Library PTSATR.ut_term
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.
Module Type ut_term_mod (X: term_sig).
Import X.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.
Module Type ut_term_mod (X: term_sig).
Import X.
Term syntax:
Inductive Term : Set:=
| Var : Vars → Term
| Sort : Sorts → Term
| App : Term → Term → Term
| Pi : Term → Term → Term
| La :Term → Term → Term
.
Notation "x · y" := (App x y) (at level 15, left associativity) : UT_scope.
Notation "! s" := (Sort s) (at level 1) : UT_scope.
Notation "# v" := (Var v) (at level 1) : UT_scope.
Notation "'Π' ( U ) , V " := (Pi U V) (at level 20, U, V at level 30) : UT_scope.
Notation "'λ' [ U ] , v " := (La U v) (at level 20, U , v at level 30) : UT_scope.
Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity).
Delimit Scope UT_scope with UT.
Open Scope UT_scope.
| Var : Vars → Term
| Sort : Sorts → Term
| App : Term → Term → Term
| Pi : Term → Term → Term
| La :Term → Term → Term
.
Notation "x · y" := (App x y) (at level 15, left associativity) : UT_scope.
Notation "! s" := (Sort s) (at level 1) : UT_scope.
Notation "# v" := (Var v) (at level 1) : UT_scope.
Notation "'Π' ( U ) , V " := (Pi U V) (at level 20, U, V at level 30) : UT_scope.
Notation "'λ' [ U ] , v " := (La U v) (at level 20, U , v at level 30) : UT_scope.
Reserved Notation " t ↑ x # n " (at level 5, x at level 0, left associativity).
Delimit Scope UT_scope with UT.
Open Scope UT_scope.
In order to deal with variable bindings and captures, we need a lift
function to deal with free and bounded variables.
M ↑ n # m recursivly add n to all variables that are
above m in M.
Fixpoint lift_rec (n:nat) (k:nat) (T:Term) {struct T} := match T with
| # x ⇒ if le_gt_dec k x then Var (n+x) else Var x
| ! s ⇒ Sort s
| M · N ⇒ App (M ↑ n # k) (N ↑ n # k)
| Π ( A ), B ⇒ Π (A ↑ n # k), (B ↑ n # (S k))
| λ [ A ], M ⇒ λ [A ↑ n # k], (M ↑ n # (S k))
end
where "t ↑ n # k" := (lift_rec n k t) : UT_scope.
Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity) : UT_scope.
| # x ⇒ if le_gt_dec k x then Var (n+x) else Var x
| ! s ⇒ Sort s
| M · N ⇒ App (M ↑ n # k) (N ↑ n # k)
| Π ( A ), B ⇒ Π (A ↑ n # k), (B ↑ n # (S k))
| λ [ A ], M ⇒ λ [A ↑ n # k], (M ↑ n # (S k))
end
where "t ↑ n # k" := (lift_rec n k t) : UT_scope.
Notation " t ↑ n " := (lift_rec n 0 t) (at level 5, n at level 0, left associativity) : UT_scope.
Some basic properties of the lift function. That is everything we will
ever need to handle de Bruijn indexes
Lemma inv_lift : ∀ M N n m , M ↑ n # m = N ↑ n # m → M = N.
intros M; induction M; destruct N; intros;
simpl in *; try (discriminate || intuition); (try (destruct (le_gt_dec m v) ; discriminate)).
destruct (le_gt_dec m v); destruct (le_gt_dec m v0) ; injection H; intros; subst; intuition.
apply plus_reg_l in H0; rewrite H0; trivial.
elim (lt_irrefl m). apply le_lt_trans with v. trivial. induction n; intuition.
elim (lt_irrefl v0). apply lt_le_trans with m. induction n; intuition. trivial.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n m H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
injection H; intros; rewrite (IHM1 N1 n m H1); rewrite (IHM2 N2 n (S m) H0); reflexivity.
Qed.
Lemma lift_rec0 : ∀ M n, M ↑ 0 # n = M.
induction M; intros; simpl.
destruct (le_gt_dec n v); reflexivity.
reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
rewrite IHM1; rewrite IHM2; reflexivity.
Qed.
Lemma lift0 : ∀ M, M ↑ 0 = M .
intros; apply lift_rec0.
Qed.
Lemma liftP1 : ∀ M i j k, (M ↑ j # i) ↑ k # (j+i) = M ↑ (j+k) # i.
intros M; induction M; intros;simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec (j+i) (j+v)); simpl.
rewrite plus_assoc. replace (k+j) with (j+k) by (apply plus_comm). trivial.
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with i; intuition.
simpl; destruct (le_gt_dec (j+i)); intuition.
elim (lt_irrefl v).
apply lt_le_trans with i; intuition. induction j; intuition.
reflexivity.
rewrite IHM1;rewrite IHM2;reflexivity.
rewrite IHM1; rewrite <-IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
rewrite IHM1; rewrite <- IHM2 ;replace (j+S i) with (S(j+i)) by intuition; reflexivity.
Qed.
Lemma liftP2: ∀ M i j k n, i ≤ n →
(M ↑ j # i) ↑ k # (j+n) = (M ↑ k # n) ↑ j # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (le_gt_dec n v).
simpl.
destruct le_gt_dec. destruct le_gt_dec.
rewrite 2! plus_assoc. replace (k+j) with (j+k) by (apply plus_comm). trivial.
elim (lt_irrefl v). apply lt_le_trans with i. induction k; intuition. trivial.
apply plus_gt_reg_l in g. elim (lt_irrefl v).
apply lt_le_trans with n; intuition.
simpl.
destruct le_gt_dec. apply plus_le_reg_l in l0. elim (lt_irrefl v).
apply lt_le_trans with n; intuition. destruct le_gt_dec. trivial.
elim (lt_irrefl v). apply lt_le_trans with i; intuition.
simpl. destruct le_gt_dec. elim (lt_irrefl n). apply lt_le_trans with i.
apply le_lt_trans with v; intuition. trivial. elim (lt_irrefl v).
apply lt_le_trans with n. apply lt_le_trans with i; intuition. trivial.
simpl. destruct le_gt_dec. elim (lt_irrefl v). apply lt_le_trans with n.
intuition. induction j; intuition. destruct le_gt_dec. elim (lt_irrefl i).
apply le_lt_trans with v; intuition. trivial.
trivial.
rewrite IHM1; intuition; rewrite IHM2; intuition; reflexivity.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n)); intuition.
rewrite IHM1; intuition.
replace (S(j+n)) with (j+S n) by intuition.
rewrite (IHM2 (S i) j k (S n) ); intuition.
Qed.
Lemma liftP3 : ∀ M i k j n , i ≤ k → k ≤ (i+n) →
(M ↑ n # i) ↑ j # k = M ↑ (j+n) # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); simpl.
destruct (le_gt_dec k (n+v)); intuition.
elim (lt_irrefl (i+n)). apply lt_le_trans with k.
apply le_lt_trans with (n+v). rewrite plus_comm. intuition. intuition. trivial.
destruct (le_gt_dec k v); intuition. elim (lt_irrefl k).
apply lt_le_trans with i. apply le_lt_trans with v. trivial. intuition. trivial.
reflexivity.
rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition;rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite IHM2; intuition. change (S i + n) with (S (i+n)). intuition.
Qed.
Lemma lift_lift : ∀ M n m, (M ↑ m) ↑ n = M↑ (n+m).
intros.
apply liftP3; intuition.
Qed.
We will consider the usual implicit substitution without variable capture
(this is where the lift operator comes in handy).
M [ n ← N ] replace the variable n in M by the term N.
Reserved Notation "t [ x ← u ]" (at level 5, x at level 0, left associativity).
Fixpoint subst_rec U T n {struct T} :=
match T with
| # x ⇒ match (lt_eq_lt_dec x n) with
| inleft (left _) ⇒ # x
| inleft (right _) ⇒ U ↑ n
| inright _ ⇒ # (x - 1)
end
| ! s ⇒ ! s
| M · N ⇒ (M [ n ← U ]) · ( N [ n ← U ])
| Π ( A ), B ⇒ Π ( A [ n ← U ] ), (B [ S n ← U ])
| λ [ A ], M ⇒ λ [ A [ n ← U ] ], (M [ S n ← U ])
end
where " t [ n ← w ] " := (subst_rec w t n) : UT_scope.
Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5) : UT_scope.
Fixpoint subst_rec U T n {struct T} :=
match T with
| # x ⇒ match (lt_eq_lt_dec x n) with
| inleft (left _) ⇒ # x
| inleft (right _) ⇒ U ↑ n
| inright _ ⇒ # (x - 1)
end
| ! s ⇒ ! s
| M · N ⇒ (M [ n ← U ]) · ( N [ n ← U ])
| Π ( A ), B ⇒ Π ( A [ n ← U ] ), (B [ S n ← U ])
| λ [ A ], M ⇒ λ [ A [ n ← U ] ], (M [ S n ← U ])
end
where " t [ n ← w ] " := (subst_rec w t n) : UT_scope.
Notation " t [ ← w ] " := (subst_rec w t 0) (at level 5) : UT_scope.
Some basic properties of the substitution function. Again, we will only need
a few functions to deal with indexes.
Lemma substP1: ∀ M N i j k ,
( M [ j ← N] ) ↑ k # (j+i) = (M ↑ k # (S (j+i))) [ j ← (N ↑ k # i ) ].
intros M; induction M; intros.
simpl (#v [j ← N] ↑ 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) as [[] | ].
destruct (le_gt_dec (S (j+i)) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition.
apply le_trans with (S (j+i)); intuition.
simpl.
destruct (le_gt_dec (j+i) v).
elim (lt_irrefl v). apply lt_le_trans with j; intuition. apply le_trans with (j+i); intuition.
destruct (lt_eq_lt_dec v j) as [[] | ]. trivial.
subst. elim (lt_irrefl j);trivial.
elim (lt_irrefl j); apply lt_trans with v; trivial.
destruct (le_gt_dec (S(j+i)) v). subst.
elim (lt_irrefl j). apply lt_le_trans with (S (j+i)). intuition. trivial.
simpl. destruct (lt_eq_lt_dec v j) as [[] | ].
subst. elim (lt_irrefl j); trivial.
apply liftP2; intuition.
subst. elim (lt_irrefl j); trivial.
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) as [[] | ].
elim (lt_irrefl j). apply lt_le_trans with v. trivial. induction k; intuition.
subst. elim (lt_irrefl v). apply lt_le_trans with (S(k+v+i)). intuition. trivial.
destruct v. apply lt_n_O in l; elim l. rewrite <- 2! pred_of_minus. replace (k+ S v) with (S (k+v)) by intuition.
simpl. trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). destruct v. apply lt_n_O in l; elim l.
rewrite <- pred_of_minus in g. simpl in g. intuition. trivial.
simpl.
destruct (le_gt_dec (j+i) (v-1)). destruct (lt_eq_lt_dec v j) as [[] | ].
elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial.
elim (lt_irrefl v). apply lt_le_trans with (S (j+i)). intuition.
destruct v. apply lt_n_O in l; elim l. rewrite <- pred_of_minus in l0. simpl in l0. intuition.
destruct (lt_eq_lt_dec) as [[] | ]. elim (lt_irrefl j); apply lt_trans with v; trivial.
subst. elim (lt_irrefl j); trivial. trivial.
simpl; trivial.
simpl; rewrite IHM1; intuition; rewrite IHM2; intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with (S((S j)+i)) by intuition.
rewrite <- (IHM2 N i (S j) k ); intuition.
simpl; rewrite IHM1; intuition.
replace (S(S(j+i))) with ((S ((S j)+i))) by intuition.
rewrite <- (IHM2 N i (S j) k ); intuition.
Qed.
Lemma substP2: ∀ M N i j n, i ≤ n →
(M ↑ j # i ) [ j+n ← N ] = ( M [ n ← N]) ↑ j # i .
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v); destruct (lt_eq_lt_dec v n) as [[] | ].
simpl.
destruct (le_gt_dec i v). destruct (lt_eq_lt_dec (j+v) (j+n)) as [[] | ].
reflexivity.
apply plus_reg_l in e. subst. elim (lt_irrefl n); trivial.
apply plus_lt_reg_l in l2. elim (lt_asym v n); trivial.
elim (lt_irrefl i). apply le_lt_trans with v; intuition. subst.
simpl.
destruct (lt_eq_lt_dec (j+n) (j+n)) as [[] | ].
apply lt_irrefl in l0; elim l0.
symmetry.
apply liftP3; intuition.
apply lt_irrefl in l0; elim l0.
simpl.
destruct (le_gt_dec i (v-1)). destruct (lt_eq_lt_dec (j+v) (j+n))as [[] | ].
apply plus_lt_reg_l in l2. elim (lt_asym v n ); trivial.
apply plus_reg_l in e; subst. elim (lt_irrefl n); trivial.
destruct v. apply lt_n_O in l0; elim l0. rewrite <- 2! pred_of_minus. replace (j+ S v) with (S (j+v)) by intuition.
simpl. trivial.
unfold gt in g. unfold lt in g. rewrite <- pred_of_minus in g.
rewrite <- (S_pred v n l0) in g.
elim (lt_irrefl n). apply lt_le_trans with v; trivial. apply le_trans with i; trivial.
simpl.
destruct (le_gt_dec i v). elim (lt_irrefl i). apply le_lt_trans with v; trivial.
destruct (lt_eq_lt_dec v (j+n)) as [[] | ]. reflexivity.
subst. elim (lt_irrefl n). apply le_lt_trans with (j+n); intuition.
elim (lt_irrefl n). apply lt_trans with v. apply le_lt_trans with (j+n); intuition. trivial.
simpl. subst.
elim (lt_irrefl n). apply lt_le_trans with i; intuition.
simpl. elim (lt_irrefl n). apply lt_le_trans with v; intuition.
apply le_trans with i; intuition.
trivial.
rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
reflexivity.
rewrite IHM1; intuition;
rewrite <- (IHM2 N (S i) j (S n)); intuition.
replace (S(j+n)) with (j+(S n)) by intuition.
reflexivity.
Qed.
Lemma substP3: ∀ M N i k n, i ≤ k → k ≤ i+n →
(M↑ (S n) # i) [ k← N] = M ↑ n # i.
intro M; induction M; intros; simpl.
destruct (le_gt_dec i v).
unfold subst_rec.
destruct (lt_eq_lt_dec (S(n+v)) k) as [[] | ].
elim (lt_irrefl (i+n)). apply lt_le_trans with k; intuition.
apply le_lt_trans with (v+n). intuition. rewrite plus_comm; intuition.
subst. replace (i+n) with (n+i) in H0 by (apply plus_comm) . replace (S (n+v)) with (n + S v) in H0 by intuition.
apply plus_le_reg_l in H0. elim (lt_irrefl i). apply le_lt_trans with v; intuition.
simpl. rewrite <- minus_n_O. trivial.
simpl. destruct (lt_eq_lt_dec v k) as [[] | ].
reflexivity. subst. elim (lt_irrefl i). apply le_lt_trans with k; intuition.
elim (lt_irrefl k). apply lt_trans with v; trivial. apply lt_le_trans with i; intuition.
reflexivity.
rewrite IHM1; intuition;rewrite IHM2; intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
rewrite IHM1; intuition; rewrite <- (IHM2 N (S i) (S k) n); intuition.
change (S i + n) with (S (i+n)). intuition.
Qed.
Lemma substP4: ∀ M N P i j,
(M [ i← N]) [i+j ← P] = (M [S(i+j) ← P]) [i← N[j← P]].
intro M; induction M; intros; simpl.
destruct (lt_eq_lt_dec v i) as [[] | ] ; destruct (lt_eq_lt_dec v (S(i+j))) as [[] | ].
simpl.
destruct (lt_eq_lt_dec v (i+j)) as [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
trivial.
subst. apply lt_irrefl in l; elim l. elim ( lt_asym v i); trivial.
subst. rewrite plus_comm in l. elim (lt_irrefl i). induction j; simpl in *; intuition.
elim (lt_irrefl i). apply le_lt_trans with v;intuition. rewrite plus_comm in l1; intuition. induction j; simpl in *; intuition.
subst. elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition.
elim (lt_irrefl i). apply lt_trans with (S (i+j)); intuition. apply lt_trans with v; trivial.
simpl. subst. destruct (lt_eq_lt_dec i i) as [[] | ].
elim (lt_irrefl i); trivial. apply substP2; intuition.
elim (lt_irrefl i); trivial.
subst. rewrite plus_comm in e0. apply succ_plus_discr in e0. elim e0.
subst. elim (lt_irrefl i). apply le_lt_trans with (i+j); intuition.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ]. destruct (lt_eq_lt_dec v i) as [[] | ].
elim (lt_asym v i); trivial. subst. elim (lt_irrefl i); trivial.
trivial. rewrite <- e in l0. rewrite <- pred_of_minus in l0.
rewrite <- (S_pred v i l) in l0. elim (lt_irrefl v); trivial.
apply lt_n_S in l1. elim (lt_irrefl v).
apply lt_trans with (S(i+j)); trivial.
rewrite <- pred_of_minus in l1. rewrite <- (S_pred v i l) in l1. trivial.
subst. simpl. rewrite <- minus_n_O.
destruct (lt_eq_lt_dec (i+j) (i+j)) as [[] | ].
elim (lt_irrefl (i+j)) ; trivial.
symmetry. apply substP3; intuition.
elim (lt_irrefl (i+j)) ; trivial.
simpl.
destruct (lt_eq_lt_dec (v-1) (i+j)) as [[] | ].
elim (lt_irrefl v). apply lt_trans with (S (i+j)) ;trivial.
apply lt_n_S in l1. rewrite <- pred_of_minus in l1. rewrite <- (S_pred v i l) in l1. trivial.
apply eq_S in e. rewrite <- pred_of_minus in e. rewrite <- (S_pred v i l) in e.
subst. elim (lt_irrefl (S(i+j))); trivial.
destruct (lt_eq_lt_dec (v-1) i) as [[] | ].
elim (lt_irrefl v). apply le_lt_trans with i; trivial. destruct v. apply lt_n_O in l; elim l.
rewrite <- pred_of_minus in l2. simpl in l2. trivial.
destruct v. elim (lt_n_O i); trivial. rewrite <- pred_of_minus in e. simpl in e. subst.
rewrite <- pred_of_minus in l1. simpl in l1. elim (lt_irrefl i).
apply le_lt_trans with (i+j); intuition.
trivial.
trivial.
rewrite IHM1; rewrite IHM2; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+ j)) by intuition;
rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
rewrite IHM1; replace (S(S(i+j))) with (S((S i)+j)) by intuition;
rewrite <- (IHM2 N P (S i)); replace (S(i+j)) with ((S i)+ j) by intuition; intuition.
Qed.
Lemma subst_travers :
∀ M N P n, (M [← N]) [n ← P] = (M [n+1 ← P])[← N[n← P]].
intros.
rewrite plus_comm. change n with (O+n). apply substP4.
Qed.
Tool function usefull when eta-conversion is used, but this is not the case
here.
Lemma expand_term_with_subst : ∀ M n, (M ↑ 1 # (S n)) [ n ← #0 ] = M.
induction M; intros.
unfold lift_rec.
destruct (le_gt_dec (S n) v). unfold subst_rec.
destruct (lt_eq_lt_dec (1+v) n) as [[] | ].
apply le_not_lt in l. elim l. intuition.
elim (lt_irrefl v). apply lt_le_trans with (S (S v)). intuition. subst; trivial.
change (1+v) with (S v). destruct v; simpl; trivial.
simpl.
destruct (lt_eq_lt_dec v n) as [[] | ].
trivial.
simpl; subst; trivial.
rewrite <- plus_n_O. trivial.
elim (lt_irrefl n). apply lt_le_trans with v; intuition.
simpl; trivial.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
Qed.
End ut_term_mod.
induction M; intros.
unfold lift_rec.
destruct (le_gt_dec (S n) v). unfold subst_rec.
destruct (lt_eq_lt_dec (1+v) n) as [[] | ].
apply le_not_lt in l. elim l. intuition.
elim (lt_irrefl v). apply lt_le_trans with (S (S v)). intuition. subst; trivial.
change (1+v) with (S v). destruct v; simpl; trivial.
simpl.
destruct (lt_eq_lt_dec v n) as [[] | ].
trivial.
simpl; subst; trivial.
rewrite <- plus_n_O. trivial.
elim (lt_irrefl n). apply lt_le_trans with v; intuition.
simpl; trivial.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
simpl. rewrite IHM1. rewrite IHM2. reflexivity.
Qed.
End ut_term_mod.