-nlemma lift_lift_aux2: ∀t.∀i,j.j ≤ i → ∀h,k.
-lift_aux (lift_aux t k i) (j+k) h = lift_aux 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/;
- ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?);
- nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
- napply le_plus;//;napply not_lt_to_le;/2/;
- ##]
-nqed.
-
-nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
-nnormalize; //;
-nqed.
-
-nlemma subst_lift_aux_k: ∀A,B.∀k.
- subst_aux (lift_aux B k 1) k A = B.
-#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 ?);
- nnormalize;/2/; napply (not_to_not … Hnk);//;
- ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
- ##]
- ##]
-nqed.
-
-nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
-nnormalize; //; nqed.
-
-nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
-//; nqed.
-
-nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
-//; nqed.
-
-nlemma subst_rel: ∀A.subst A (Rel O) = A.
-nnormalize; //; nqed.
-
-nlemma subst_rel1: ∀A.∀k,i. i < k →
- subst_aux (Rel i) k A = Rel i.
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
-
-nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A 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 →
- subst_aux (Rel i) k A = Rel (i-1).
-#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.
-
-(* versione con plus
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
- lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
- ##[nelim (leb (S n) k);
- ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/;
- ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/;
- ##]
- ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
- ##[nrewrite > (lt_to_leb_false (S n) k ?);
- ##[ncut (j+k+1 = n+1);##[//;##] #Heq;
- nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
- napplyS lift_lift_aux2 (* bello *);//;
- ##|/2/;
- ##]
- ##|ncut (j + k < n);
- ##[napply not_eq_to_le_to_lt;
- ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
- ##|#ltjkn;
- ncut (O < n); ##[/2/; ##] #posn;
- ncut (k ≤ n); ##[/2/; ##] #lekn;
- nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
- ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
- nrewrite > (subst_rel3 A (j+k+1) (n+1) ?);
- ##[nrewrite < (plus_minus_m_m … posn);//;
- ##|napplyS monotonic_lt_plus_l; //;
- ##]
- ##|napply le_S_S;
- napply (not_eq_to_le_to_le_minus … lekn);
- /2/; (* come fa? *)
- ##]
- ##]
- ##]
-nqed. *)
-
-naxiom lift_subst_aux_kij: ∀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_aux_k: ∀A,B.∀j,k.
- lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
- ##[nelim (leb (S n) k);
- ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/;
- ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/;
- ##]
- ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
- ##[nrewrite > (lt_to_leb_false (S n) k ?);
- ##[ncut (S(j+k) = n+1);##[//;##] #Heq;
- nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
- napplyS lift_lift_aux2 (* bello *);//;
- ##|/2/;
- ##]
- ##|ncut (j + k < n);
- ##[napply not_eq_to_le_to_lt;
- ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
- ##|#ltjkn;
- ncut (O < n); ##[/2/; ##] #posn;
- ncut (k ≤ n); ##[/2/; ##] #lekn;
- nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
- ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
- nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?);
- ##[nrewrite < (plus_minus_m_m … posn);//;
- ##|ncut (S n = n +1); /2/;
- ##]
- ##|napply le_S_S; (* /3/;*)
- napply (not_eq_to_le_to_le_minus … lekn);
- /3/; (* come fa? *)
- ##]
- ##]
- ##]
-nqed.
-
-(*
-nlemma lift_subst_aux_k: ∀A,B.∀k.
- lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A.
-#A; #B; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) k); nnormalize; #Hnk;
- ##[nrewrite > (le_to_leb_true ?? Hnk);
- nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/;
- ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?);
- ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n);
- napply not_lt_to_le; napply Hnk; ##]
- napply (eqb_elim n k);#eqnk;
- ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/;
- nnormalize; nrewrite < eqnk; //; (* strano *)
- ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/;
- nnormalize;
- ncut (O < n);
- ##[napply not_le_to_lt;#len;
- napply eqnk; napply le_to_le_to_eq;
- ##[napply transitive_le; //;
- ##|napply not_lt_to_le; /2/;
- ##]
- ##|#posn;
- nrewrite > (lt_to_leb_false (S (n - 1)) k ?);
- ##[nnormalize;
- (* nrewrite < (minus_plus_m_m n 1); *)
- nrewrite < (plus_minus_m_m n 1 ?);//;
- ##|napply le_S_S; napply not_eq_to_le_to_le_minus;
- ##[/2/;
- ##|napply (not_lt_to_le … Hnk);
- ##]
- ##]
- ##]
- ##]
- ##]
-nqed.
-*)
-
-ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
- subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k).
-#A; #B; nelim B; nnormalize; /2/;
- ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
- napply eq_f2;/2/; napply Hind2;
- napplyS (monotonic_le_plus_l 1);//
- ##|#n; #i; #j; #k; #leij; #ltjk;
- napply (leb_elim (S n) i); nnormalize; #len;
- ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
- ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
- ##[nnormalize;
- nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
- nnormalize; /2/; napply (not_to_not …len);
- #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
- nnormalize; //;
- ##|napply le_S_S; napply (transitive_le … ltjk);
- napply le_plus;//; napply not_lt_to_le; /2/;
- ##]
- ##]
-nqed.
-
-(********************* substitution lemma ***********************)
-nlemma subst_lemma: ∀A,B,C.∀k,i.
- subst_aux (subst_aux A i B) (k+i) C =
- subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
-#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
-#n; #i; napply (leb_elim (S n) i); #Hle;
- ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
- ncut (n ≤ k+i); ##[/2/##] #len;
- nrewrite > (subst_rel1 C (k+i) n ltn);
- nrewrite > (le_to_leb_true n (k+i) len);
- nrewrite > (subst_rel1 … Hle);//;
- ##|napply (eqb_elim n i); #eqni;
- ##[nrewrite > eqni;
- nrewrite > (le_to_leb_true i (k+i) ?); //;
- nrewrite > (subst_rel2 …); nnormalize;
- napply symmetric_eq;
- napplyS (lift_subst_aux_kij C B i k O);
- ##|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) ?);
- ##[nrewrite > (subst_rel3 ? i n ?);//;
- napply not_eq_to_le_to_lt;
- ##[/2/;
- ##|napply not_lt_to_le;/2/;
- ##]
- ##|napply (transitive_le … nk);//;
- ##]
- ##|ncut (i < n);
- ##[napply not_eq_to_le_to_lt; ##[/2/]
- napply (not_lt_to_le … Hle);##]
- #ltin; ncut (O < n); ##[/2/;##] #posn;
- napply (eqb_elim (n-1) (k+i)); #H
- ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
- nrewrite > (lt_to_leb_false n (k+i) ?);
- ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?);
- ##[nnormalize;
- ##|nrewrite < H; napplyS plus_minus_m_m;//;
- ##]
- ##|nrewrite < H; napply (lt_O_n_elim … posn);
- #m; nnormalize;//;
- ##]
- ##|ncut (k+i < n-1);
- ##[napply not_eq_to_le_to_lt;
- ##[napply symmetric_not_eq; napply H;
- ##|napply (not_lt_to_le … nk);
- ##]
- ##]
- #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
- ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
- ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
- nrewrite > (subst_rel3 ? i (n-1) ?);//;
- napply (le_to_lt_to_lt … Hlt);//;
- ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
- ##]
- ##|napply (transitive_lt … Hlt);
- napply (lt_O_n_elim … posn);
- #m; nnormalize;//;
- ##]
- ##]
- nrewrite <H;
- ncut (∃m:nat. S m = n);
- ##[napply (lt_O_n_elim … posn); #m;@ m;//;
- ##|*; #m; #Hm; nrewrite < Hm;
- nrewrite > (delift ???????);nnormalize;/2/;
- ##]
-nqed.
-