- | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
- | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
- | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
+ | App m n ⇒ App (lift m k p) (lift n k p)
+ | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
+ | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
-notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift $n $M}.
-notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift_aux $n $k $M}.
+notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift O $M}.
+notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift $n $k $M}.
-interpretation "Lift" 'Lift n M = (lift M n).
-interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n).
+(* interpretation "Lift" 'Lift n M = (lift M n). *)
+interpretation "Lift" 'Lift n k M = (lift M k n).
- (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
- | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
- | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
- | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
+ (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
+ | App m n ⇒ App (subst m k a) (subst n k a)
+ | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
+ | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
-interpretation "Subst" 'Subst N M = (subst N M).
-interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N).
+(* interpretation "Subst" 'Subst N M = (subst N M). *)
+interpretation "Subst" 'Subst M k N = (subst M k N).
-nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
-#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
+nlemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
+#i; nchange with (lift (Rel i) 0 1 = Rel (1 + i)); //; nqed.
-nlemma lift_lift_aux: ∀t.∀i,j.j ≤ i → ∀h,k.
-lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
+nlemma lift_lift: ∀t.∀i,j.j ≤ i → ∀h,k.
+ lift (lift t k i) (j+k) h = lift t k (i+h).
#t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
napply (leb_elim (S n) k); #Hnk;nnormalize;
##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
#t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
napply (leb_elim (S n) k); #Hnk;nnormalize;
##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
-nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
+nlemma lift_lift1: ∀t.∀i,j,k.
+ lift(lift t k j) k i = lift t k (j+i).
-nlemma lift_lift_aux2: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
+nlemma lift_lift2: ∀t.∀i,j,k.
+ lift (lift t k j) (j+k) i = lift t k (j+i).
#A; #B; nelim B; nnormalize; /2/; #n; #k;
napply (leb_elim (S n) k); nnormalize; #Hnk;
##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
#A; #B; nelim B; nnormalize; /2/; #n; #k;
napply (leb_elim (S n) k); nnormalize; #Hnk;
##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
#A; #k; nnormalize;
nrewrite > (lt_to_leb_false (S k) k ?); //;
nrewrite > (eq_to_eqb_true … (refl …)); //;
nqed.
nlemma subst_rel3: ∀A.∀k,i. k < i →
#A; #k; nnormalize;
nrewrite > (lt_to_leb_false (S k) k ?); //;
nrewrite > (eq_to_eqb_true … (refl …)); //;
nqed.
nlemma subst_rel3: ∀A.∀k,i. k < i →
#A; #k; #i; nnormalize; #ltik;
nrewrite > (lt_to_leb_false (S i) k ?); /2/;
nrewrite > (not_eq_to_eqb_false i k ?); //;
napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
nqed.
#A; #k; #i; nnormalize; #ltik;
nrewrite > (lt_to_leb_false (S i) k ?); /2/;
nrewrite > (not_eq_to_eqb_false i k ?); //;
napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
nqed.
-nlemma lift_subst_aux_ijk: ∀A,B.∀i,j,k.
- lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
+nlemma lift_subst_ijk: ∀A,B.∀i,j,k.
+ lift (subst B (j+k) A) k i = subst (lift B k i) (j+k+i) A.
#A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
##[nelim (leb (S n) k);
#A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
##[nelim (leb (S n) k);
##[nrewrite > (lt_to_leb_false (S n) k ?);
##[ncut (j+k+i = n+i);##[//;##] #Heq;
nrewrite > Heq; nrewrite > (subst_rel2 A ?);
##[nrewrite > (lt_to_leb_false (S n) k ?);
##[ncut (j+k+i = n+i);##[//;##] #Heq;
nrewrite > Heq; nrewrite > (subst_rel2 A ?);
nqed.
ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
nqed.
ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
#A; #B; nelim B; nnormalize; /2/;
##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
#A; #B; nelim B; nnormalize; /2/;
##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
napplyS (monotonic_le_plus_l 1);//
##|#n; #i; #j; #k; #leij; #ltjk;
napply (leb_elim (S n) i); nnormalize; #len;
napplyS (monotonic_le_plus_l 1);//
##|#n; #i; #j; #k; #leij; #ltjk;
napply (leb_elim (S n) i); nnormalize; #len;
(********************* substitution lemma ***********************)
nlemma subst_lemma: ∀A,B,C.∀k,i.
(********************* substitution lemma ***********************)
nlemma subst_lemma: ∀A,B,C.∀k,i.
#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
#n; #i; napply (leb_elim (S n) i); #Hle;
##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
#n; #i; napply (leb_elim (S n) i); #Hle;
##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
##|napply (leb_elim (S (n-1)) (k+i)); #nk;
##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
nrewrite > (le_to_leb_true n (k+i) ?);
##|napply (leb_elim (S (n-1)) (k+i)); #nk;
##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
nrewrite > (le_to_leb_true n (k+i) ?);