--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+include "basics/list2.ma".
+
+ninductive T : Type ≝
+ | Sort: nat → T
+ | Rel: nat → T
+ | App: T → T → T
+ | Lambda: T → T → T (* type, body *)
+ | Prod: T → T → T (* type, body *)
+.
+
+nlet rec lift_aux t k p ≝
+ match t with
+ [ Sort n ⇒ Sort n
+ | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
+ | 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)
+ ].
+
+ndefinition lift ≝ λt.λp.lift_aux t 0 p.
+
+nlet rec subst_aux t k a ≝
+ match t with
+ [ Sort n ⇒ Sort n
+ | Rel n ⇒ if_then_else T (leb (S n) k) (Rel 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)
+ ].
+
+ndefinition subst ≝ λa.λt.subst_aux t 0 a.
+
+(*** properties of lift and subst ***)
+nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
+#t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k);
+nnormalize;//;nqed.
+
+nlemma lift_0: ∀t:T. lift t 0 = t.
+#t; nelim t; nnormalize; //; nqed.
+
+nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
+//; nqed.
+
+nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
+//; nqed.
+
+nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
+#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
+
+(*
+nlemma lift_lift_aux: ∀t.∀i,j,k,k1. k ≤ k1 → k1 ≤ k+j →
+lift_aux (lift_aux t k j) k1 i = lift_aux t k (j+i).
+#t; nelim t; nnormalize; //; #n; #i;#j; #k; #k1; #lel; #ler;
+napply (leb_elim (S n) k); #Hnk;nnormalize;
+ ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
+ ##|nrewrite > (lt_to_leb_false (S n+j) k ?);
+ nnormalize;//;napply (lt_to_le_to_lt ? (S n));
+ ##[napply not_le_to_lt;/2/;
+ ##|(* lento /2/; *) napply le_S_S;/1/;
+ ##]
+nqed. *)
+
+nlemma lift_lift_aux: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
+#t; nelim t; nnormalize; //; #n; #i;#j; #k;
+napply (leb_elim (S n) k); #Hnk;nnormalize;
+ ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
+ ##|nrewrite > (lt_to_leb_false (S n+j) k ?);
+ nnormalize;//; napply (lt_to_le_to_lt ? (S n));
+ ##[napply not_le_to_lt;//;
+ ##|napply le_S_S;//;
+ ##]
+nqed.
+
+nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
+#t; nelim t; nnormalize; //; #n; #i;#j; #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+j) (j+k) ?);
+ nnormalize;//; napply le_S_S; napplyS monotonic_le_plus_r;
+ /3/;
+ ##]
+nqed.
+
+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.
+
+(*************************** substl *****************************)
+
+nlet rec substl (G:list T) (N:T) : list T ≝
+ match G with
+ [ nil ⇒ nil T
+ | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
+ ].
+
+
+(*****************************************************************)
+
+naxiom A: nat → nat → Prop.
+naxiom R: nat → nat → nat → Prop.
+naxiom conv: T → T → Prop.
+
+ninductive TJ: list T → T → T → Prop ≝
+ | ax : ∀i,j. A i j → TJ [] (Sort i) (Sort j)
+ | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 1)
+ | weak: ∀G.∀A,B,C.∀i.
+ TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1)
+ | prod: ∀G.∀A,B.∀i,j,k. R i j k →
+ TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
+ | app: ∀G.∀F,A,B,a.
+ TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B a)
+ | abs: ∀G.∀A,B,b.∀i.
+ TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
+ | conv: ∀G.∀A,B,C.∀i. conv B C →
+ TJ G A B → TJ G B (Sort i) → TJ G A C.
+
+ninverter TJ_inv2 for TJ (%?%) : Prop.
+
+(**** definitions ****)
+
+ninductive Glegal (G: list T) : Prop ≝
+glegalk : ∀A,B.TJ G A B → Glegal G.
+
+ninductive Gterm (G: list T) (A:T) : Prop ≝
+ | is_term: ∀B.TJ G A B → Gterm G A
+ | is_type: ∀B.TJ G B A → Gterm G A.
+
+ninductive Gtype (G: list T) (A:T) : Prop ≝
+gtypek: ∀i.TJ G A (Sort i) → Gtype G A.
+
+ninductive Gelement (G:list T) (A:T) : Prop ≝
+gelementk: ∀B.TJ G A B → Gtype G B → Gelement G A.
+
+ninductive Tlegal (A:T) : Prop ≝
+tlegalk: ∀G. Gterm G A → Tlegal A.
+
+(*
+ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
+
+ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
+
+ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
+
+ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
+
+ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
+*)
+
+(*
+ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
+subst C A
+#G; #i; #j; #axij; #Gleg; ncases Gleg;
+#A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
+*)
+
+ntheorem start_lemma1: ∀G.∀i,j.
+A i j → Glegal G → TJ G (Sort i) (Sort j).
+#G; #i; #j; #axij; #Gleg; ncases Gleg;
+#A; #B; #tjAB; nelim tjAB; /2/;
+(* bello *) nqed.
+
+ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
+TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S i)).
+#G; #A; #C; #n; #i; #p; #tjC; #tjn;
+ napplyS (weak G (Rel n));//. (* bello *)
+ (*
+ nrewrite > (plus_n_O i);
+ nrewrite > (plus_n_Sm i O);
+ nrewrite < (lift_lift A 1 i);
+ nrewrite > (plus_n_O n); nrewrite > (plus_n_Sm n O);
+ applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
+nqed.
+
+ntheorem start_lemma2: ∀G.
+Glegal G → ∀n. n < length T G → TJ G (Rel n) (lift (nth n T G (Rel O)) (S n)).
+#G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
+ ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
+ napply (absurd … abs); //;
+ ##|#G; #A; #i; #tjA; #Hind; #m; ncases m; /2/;
+ #p; #Hle; napply start_rel; //; napply Hind;
+ napply le_S_S_to_le; napply Hle;
+ ##|#G; #A; #B; #C; #i; #tjAB; #tjC; #Hind1; #_; #m; ncases m;
+ /2/; #p; #Hle; napply start_rel; //;
+ napply Hind1; napply le_S_S_to_le; napply Hle;
+ ##]
+nqed.
+
+(*
+nlet rec TJm G D on D : Prop ≝
+ match D with
+ [ nil ⇒ True
+ | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
+ ].
+
+nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
+#G; #D; #A; *; //; nqed.
+
+ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
+ ∀G. Glegal G → TJm G D → TJ G A B.
+#D; #A; #B; #tjAB; nelim tjAB;
+ ##[/2/;
+ ##|/2/;
+ ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
+ #tjGcons;
+ napply weak;
+*)
+(*
+ntheorem substitution_tj:
+∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
+ TJ G (subst N M) (subst N B).
+#G;#A;#B;#N;#M;#tjM;
+ napply (TJ_inv2 (A::G) M B);
+ ##[nnormalize; /3/;
+ ##|#G; #A; #N; #tjA; #Hind; #Heq;
+ ndestruct;//;
+ ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
+ ndestruct;//;
+ ##|nnormalize; #E; #A; #B; #i; #j; #k;
+ #Ax; #tjA; #tjB; #Hind1; #_;
+ #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
+ ##[/2/;
+ ##|nnormalize; napplyS weak;
+
+*)
+
+ntheorem substitution_tj:
+∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A →
+ TJ ((substl D N)@G) (subst_aux M (length ? D) N) (subst_aux B (length ? D) N).
+#E; #A; #B; #M; #tjMB; nelim tjMB;
+ ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D;
+ ##[nnormalize; #isnil; ndestruct;
+ ##|#P; #L; nnormalize; #isnil; ndestruct;
+ ##]
+ ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D;
+ ##[#N; #Heq; #tjN;
+ nrewrite > (delift (lift N O) A1 O O O ??); //;
+ nnormalize in Heq; ndestruct;/2/;
+ ##|#H; #L; #N1; #Heq; nnormalize in Heq;
+ #tjN1; nnormalize; ndestruct;
+ (* porcherie *)
+ ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
+ nrewrite > Heq;
+ nrewrite < (lift_subst_aux_k N1 H (length T L) O);
+ nrewrite < (plus_n_O (length T L));
+ napply start;/2/;
+ ##]
+ ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
+ #G1; #D; #N; ncases D; nnormalize;
+ ##[#Heq; ndestruct; #tjN; //;
+ ##|#H; #L; #Heq;
+ #tjN1; ndestruct;
+ (* porcherie *)
+ ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
+ nrewrite > Heq;
+ nrewrite < (lift_subst_aux_k N P (length T L) O);
+ nrewrite < (lift_subst_aux_k N Q (length T L) O);
+ nrewrite < (plus_n_O (length T L));
+ napply weak;/2/;
+ ##]
+ ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
+ #G1; #D; #N; #Heq; #tjN;
+ napply (prod … Ax);
+ ##[/2/;
+ ##|
+ ##]
+ ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
+ #G1; #D; #N; #Heq; #tjN; nnormalize;
+ ncheck app.
+
+
+
+
+ntheorem substitution_tj:
+∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A →
+∀k.length ? D = k →
+ TJ ((substl D N)@G) (subst_aux M k N) (subst_aux B k N).
+#E; #A; #B; #M; #tjMB; nelim tjMB;
+ ##[nnormalize; (* /3/; *)
+ ##|#G; #A1; #i; #tjA; #Hind;
+ #G1; #D; ncases D;
+ ##[#N; #Heq; #tjN; #k; nnormalize in ⊢ (% → ?); #kO;
+ nrewrite < kO;
+ nrewrite > (delift (lift N O) A1 O O O ??); //;
+ nnormalize in Heq; ndestruct;/2/;
+ ##|#H; #L; #N1; #Heq; nnormalize in Heq;
+ #tjN1; #k; #len; nnormalize in len;
+ nrewrite < len;
+ nnormalize; ndestruct;
+ (* porcherie *)
+ ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
+ nrewrite > Heq;
+ nrewrite < (lift_subst_aux_k N1 H (length T L) O);
+ nrewrite < (plus_n_O (length T L));
+ napply (start (substl L N1@G1) (subst_aux H (length T L) N1) i ?).
+ napply Hind;//;
+ ##]
+
+
+
+
+
+
+
+
projects / helm.git / commitdiff