Require Import Peano_dec. Require Import Compare_dec. Require Import Lt. Require Import Omega. Require Import Bool. Definition Sorts := nat. Definition Vars := nat. (* raw terms *) Inductive Term : Set:= | Var : Vars -> Term (* DeBruijn index *) | Sort : Sorts -> Term | App : Term -> Term -> Term | Pi : Term -> Term -> Term | La :Term -> Term -> Term . (* with cool notations *) Notation "x · y" := (App x y) (at level 15, left associativity). Notation "! s" := (Sort s) (at level 1). Notation "# v" := (Var v) (at level 1). Notation "'Π' ( U ) , V " := (Pi U V) (at level 20, U, V at level 30). Notation "'λ' [ U ] , v " := (La U v) (at level 20, U , v at level 30). (* decidability of eq is ok on the terms *) Theorem eq_term_dec : forall x y: Term, {x=y}+{x<>y}. decide equality. apply eq_nat_dec. apply eq_nat_dec. Qed. (* lift function, deBruijn related *) Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity). (* "lift n k c" lift the indexes above k in c by n e.g. #0 ↑ n # 42 = #0 but #43 ↑ n # 42 = #(43+n) *) Fixpoint lift_rec (n:nat) (k:nat) (c':Term) {struct c'} := match c' with | # i => if le_gt_dec k i then Var (n+i) else Var i | ! s => Sort s | u · v=> App (u ↑ n # k) (v ↑ n # k) | Π ( A ), B => Π (A ↑ n # k), (B ↑ n # (S k)) | λ [ A ], b => λ [A ↑ n # k], (b ↑ n # (S k)) end where "t ↑ n # k" := (lift_rec n k t). (* most of the time we lift everything *) Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity). (* simple rewriting lemma *) Lemma lift_rec0 : forall c n, c ↑ 0 # n = c. induction c; intros; simpl. destruct (le_gt_dec n v); reflexivity. reflexivity. rewrite IHc1; rewrite IHc2; reflexivity. rewrite IHc1; rewrite IHc2; reflexivity. rewrite IHc1; rewrite IHc2; reflexivity. Qed. Lemma lift0 : forall c, c ↑ 0 = c . intros; apply lift_rec0. Qed. (* 3 lemmas on lift / lift is all we will ever need thank to Gerard Huet for the code *) Lemma liftP1 : forall t i j k, (t ↑ j # i) ↑ k # (j+i) = t ↑ (j+k) # i. intros t; induction t; intros;simpl. destruct (le_gt_dec i v); simpl. destruct (le_gt_dec (j+i) (j+v)); simpl. replace (k+(j+v)) with (j+k+v) by omega; reflexivity. intuition. simpl; destruct (le_gt_dec (j+i)); intuition. reflexivity. rewrite IHt1;rewrite IHt2;reflexivity. rewrite IHt1; rewrite <-IHt2 ;replace (j+S i) with (S(j+i)) by omega; reflexivity. rewrite IHt1; rewrite <- IHt2 ;replace (j+S i) with (S(j+i)) by omega; reflexivity. Qed. Lemma liftP2: forall t i j k n, i <= n -> (t ↑ j # i) ↑ k # (j+n) = (t ↑ k # n) ↑ j # i. intro t; induction t; intros; simpl. destruct (le_gt_dec i v); destruct (le_gt_dec n v). simpl. destruct (le_gt_dec (j+n) (j+v)); destruct (le_gt_dec i (k+v)); intuition. simpl. destruct (le_gt_dec (j+n) (j+v)); destruct (le_gt_dec i v); intuition. simpl. destruct (le_gt_dec (j+n) v); destruct (le_gt_dec i (k+v)); intuition. simpl. destruct (le_gt_dec (j+n) v); (destruct (le_gt_dec i v)); intuition. reflexivity. rewrite IHt1; intuition; rewrite IHt2; intuition; reflexivity. rewrite IHt1; intuition. replace (S(j+n)) with (j+S n) by omega. rewrite (IHt2 (S i) j k (S n)); intuition. rewrite IHt1; intuition. replace (S(j+n)) with (j+S n) by omega. rewrite (IHt2 (S i) j k (S n) ); intuition. Qed. Lemma liftP3 : forall t i k j n , i <= k -> k <= (i+n) -> (t ↑ n # i) ↑ j # k = t ↑ (j+n) # i. intro t; induction t; intros; simpl. destruct (le_gt_dec i v); simpl. destruct (le_gt_dec k (n+v)); intuition. destruct (le_gt_dec k v); intuition. reflexivity. rewrite IHt1; intuition;rewrite IHt2; intuition. rewrite IHt1; intuition;rewrite IHt2; intuition. rewrite IHt1; intuition; rewrite IHt2; intuition. Qed. Lemma lift_lift : forall t n m, (t ↑ m) ↑ n = t↑ (n+m). intros. apply liftP3; omega. Qed. (* substitution *) (* i = index to replace t = term we are replacing k = limit between free and bound indices *) (* we substitute the deBruijn index x with the term u in the term t *) Reserved Notation "t [ x ← u ]" (at level 5, x at level 0, left associativity). Fixpoint subst_rec w t n {struct t} := match t with | # v => match (lt_eq_lt_dec v n) with | inleft (left _) => # v (* v < n *) | inleft (right _) => w ↑ n (* v = n *) | inright _ => # (v - 1) (* v > n *) end | ! s => ! s | u · v => (u [ n ← w ]) · ( v [ n ← w ]) | Π ( A ), B => Π ( A [ n ← w ] ), (B [ S n ← w ]) | λ [ A ], b => λ [ A [ n ← w ] ], (b [ S n ← w ]) end where " t [ n ← w ] " := (subst_rec w t n). Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5). (* this time, we only need 4 lemmas for subst/lift or subst/subst cases again thanks gerard *) Lemma substP1: forall t u i j k , ( t [ j ← u] ) ↑ k # (j+i) = (t ↑ k # (S (j+i))) [ j ← (u ↑ k # i ) ]. intros t; induction t; intros. simpl (#v [j ← u] ↑ k # (j+i)). change (#v ↑ k # (S (j+i))) with (if le_gt_dec (S (j+i)) v then #(k+v) else #v). destruct (lt_eq_lt_dec v j). destruct s. destruct (le_gt_dec (S (j+i)) v). elim (lt_irrefl j); intuition. simpl. destruct (le_gt_dec (j+i) v). elim (lt_irrefl j); intuition. destruct (lt_eq_lt_dec v j). destruct s. reflexivity. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. destruct (le_gt_dec (S(j+i)) v). elim (lt_irrefl j); intuition. simpl. destruct (lt_eq_lt_dec v j). destruct s. elim (lt_irrefl j); intuition. apply liftP2; intuition. elim (lt_irrefl j); intuition. destruct (le_gt_dec (S (j+i)) v). simpl. destruct (le_gt_dec (j+i) (v-1)); destruct (lt_eq_lt_dec (k+v) j). destruct s. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. replace (k+(v-1)) with (k+v-1) by omega. reflexivity. destruct s. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. simpl. destruct (le_gt_dec (j+i) (v-1)); destruct (lt_eq_lt_dec v j). destruct s. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. destruct s. elim (lt_irrefl j); intuition. elim (lt_irrefl j); intuition. reflexivity. intuition. simpl; rewrite IHt1; intuition; rewrite IHt2; intuition. simpl; rewrite IHt1; intuition. replace (S(S(j+i))) with (S((S j)+i)) by omega. rewrite <- (IHt2 u i (S j) k ); intuition. simpl; rewrite IHt1; intuition. replace (S(S(j+i))) with ((S ((S j)+i))) by omega. rewrite <- (IHt2 u i (S j) k ); intuition. Qed. Lemma substP2: forall t u i j n, i <= n -> (t ↑ j # i ) [ j+n ← u ] = ( t [ n ← u]) ↑ j # i . intro t; induction t; intros; simpl. destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v n) . destruct s. simpl. destruct (le_gt_dec i v); destruct (lt_eq_lt_dec (j+v) (j+n)). destruct s. reflexivity. elim (lt_asym v n); intuition. intuition. elim (lt_asym i v); intuition. elim (lt_asym v n); intuition. simpl. destruct (lt_eq_lt_dec (j+v) (j+n)). destruct s. elim (lt_asym v n); intuition. symmetry. apply liftP3; intuition. elim (lt_asym v n); intuition. simpl. destruct (le_gt_dec i (v-1)); destruct (lt_eq_lt_dec (j+v) (j+n)). destruct s. intuition. elim (lt_asym v n); intuition. intuition. destruct s. intuition. elim (lt_asym v n); intuition. intuition. destruct s. simpl. destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v (j+n)). destruct s. intuition. elim (lt_asym v n); intuition. intuition. destruct s. intuition. elim (lt_asym v n); intuition. intuition. simpl. destruct (lt_eq_lt_dec v (j+n)). destruct s. elim (lt_asym v n); intuition. elim (lt_asym v n); intuition. elim (lt_asym v n); intuition. simpl. destruct (le_gt_dec i (v-1)); destruct (lt_eq_lt_dec v (j+n)). destruct s. intuition. elim (lt_asym v n); intuition. intuition. destruct s. intuition. elim (lt_asym v n); intuition. intuition. intuition. rewrite IHt1; intuition;rewrite IHt2; intuition. rewrite IHt1; intuition; rewrite <- (IHt2 u (S i) j (S n)); intuition. replace (S(j+n)) with (j+(S n)) by omega. reflexivity. rewrite IHt1; intuition; rewrite <- (IHt2 u (S i) j (S n)); intuition. replace (S(j+n)) with (j+(S n)) by omega. reflexivity. Qed. Lemma substP3: forall t u i k n, i <= k -> k <= i+n -> (t↑ (S n) # i) [ k← u] = t ↑ n # i. intro t; induction t; intros; simpl. destruct (le_gt_dec i v). change (#(S (n+v)) [k ← u]) with ( match lt_eq_lt_dec (S (n+v)) k with | inleft (left _ ) => #(S(n+v)) | inleft (right _ ) => u ↑ k | inright _ => #(S(n+v)-1) end ). destruct (lt_eq_lt_dec (S(n+v)) k). destruct s. intuition. elim (lt_asym n v); intuition. intuition. simpl. destruct (lt_eq_lt_dec v k). destruct s. reflexivity. elim (lt_asym n v); intuition. intuition. reflexivity. rewrite IHt1; intuition;rewrite IHt2; intuition. rewrite IHt1; intuition; rewrite <- (IHt2 u (S i) (S k) n); intuition. rewrite IHt1; intuition; rewrite <- (IHt2 u (S i) (S k) n); intuition. Qed. Lemma substP4: forall t u w i j, (t [ i← u]) [i+j ← w] = (t [S(i+j) ← w]) [i← u[j← w]]. intro t; induction t; intros; simpl. destruct (lt_eq_lt_dec v i); destruct (lt_eq_lt_dec v (S(i+j))). destruct s; destruct s0. simpl. destruct (lt_eq_lt_dec v (i+j)); destruct (lt_eq_lt_dec v i); intuition ; (try (elim (lt_asym v i); intuition)). elim (lt_asym v i); intuition. simpl. destruct (lt_eq_lt_dec v i). destruct s; intuition. elim (lt_asym v i); intuition. apply substP2; intuition. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. destruct s. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. destruct s. simpl. destruct (lt_eq_lt_dec (v-1) (i+j)); destruct (lt_eq_lt_dec v i). destruct s; destruct s0. intuition. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. destruct s. reflexivity. elim (lt_asym v i); intuition. destruct s. intuition. elim (lt_asym v i); intuition. intuition. simpl. destruct (lt_eq_lt_dec (v-1) (i+j)). destruct s. elim (lt_asym v i); intuition. symmetry;apply substP3; intuition. elim (lt_asym v i); intuition. simpl. destruct (lt_eq_lt_dec (v-1) (i+j)) ; destruct (lt_eq_lt_dec (v-1) i). destruct s; destruct s0. reflexivity. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. elim (lt_asym v i); intuition. destruct s. intuition. elim (lt_asym v i); intuition. destruct s. intuition. elim (lt_asym v i); intuition. reflexivity. reflexivity. rewrite IHt1; rewrite IHt2; intuition. rewrite IHt1; replace (S(S(i+j))) with (S((S i)+ j)) by omega; rewrite <- (IHt2 u w (S i)); replace (S(i+j)) with ((S i)+ j) by omega; intuition. rewrite IHt1; replace (S(S(i+j))) with (S((S i)+j)) by omega; rewrite <- (IHt2 u w (S i)); replace (S(i+j)) with ((S i)+ j) by omega; intuition. Qed. Lemma subst_travers : forall M N P n, (M [← N]) [n ← P] = (M [n+1 ← P])[← N[n← P]]. intro M; induction M; intros; simpl. destruct (lt_eq_lt_dec v 0); destruct (lt_eq_lt_dec v (n+1)). destruct s; destruct s0. elim (lt_n_O v); intuition. elim (lt_n_O v); intuition. rewrite (lift0 N). simpl. destruct (lt_eq_lt_dec v 0). destruct s. elim (lt_n_O v); intuition. rewrite (lift0 (subst_rec P N n)). reflexivity. elim (lt_n_O v); intuition. rewrite e in e0. replace (n+1) with (S n) in e0. discriminate e0. omega. destruct s. elim (lt_n_O v); intuition. elim (lt_n_O (n+1)); intuition. destruct s. simpl. destruct (lt_eq_lt_dec (v-1) n); destruct (lt_eq_lt_dec v 0). destruct s; destruct s0. elim (lt_n_O v); intuition. elim (lt_irrefl 0); intuition. elim (lt_n_O v); intuition. elim (lt_irrefl 0); intuition. destruct s. intuition. elim (lt_n_O v); intuition. destruct s. elim (lt_n_O v); intuition. elim (lt_irrefl 0); intuition. intuition. simpl. destruct (lt_eq_lt_dec (v-1) n). destruct s. elim (lt_asym v (n+1)); intuition. destruct N. simpl. destruct (lt_eq_lt_dec v0 n). destruct s. simpl. replace (n+1) with (S n) by omega; symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega; symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega; symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega; symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega; symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega;symmetry; apply substP3; intuition. replace (n+1) with (S n) by omega;symmetry; apply substP3; intuition. elim (lt_irrefl (n+1)); intuition. simpl. destruct (lt_eq_lt_dec (v-1) n); destruct (lt_eq_lt_dec (v-1) 0). destruct s; destruct s0. intuition. elim (lt_n_O n); intuition. elim (lt_n_O n); intuition. elim (lt_n_O n); intuition. destruct s. elim (lt_n_O n); intuition. elim (lt_n_O n); intuition. destruct s. elim (lt_n_O n); intuition. elim (lt_n_O n); intuition. intuition. intuition. rewrite IHM1; rewrite IHM2 ; reflexivity. rewrite IHM1; change (S n) with (1+n); rewrite substP4 ;replace (n+1) with (1+n) by (apply plus_comm); reflexivity. rewrite IHM1; change (S n) with (1+n); rewrite substP4 ;replace (n+1) with (1+n) by (apply plus_comm); reflexivity. Qed.