From ed76333464d49a3cd55ca2adb05b0afdbc8486bd Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 12 Mar 2010 12:25:43 +0000 Subject: [PATCH 1/1] First version of PTS --- helm/software/matita/nlibrary/PTS/gpts.ma | 573 ++++++++++++++++++++++ 1 file changed, 573 insertions(+) create mode 100644 helm/software/matita/nlibrary/PTS/gpts.ma diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma new file mode 100644 index 000000000..bf149812d --- /dev/null +++ b/helm/software/matita/nlibrary/PTS/gpts.ma @@ -0,0 +1,573 @@ +(**************************************************************************) +(* ___ *) +(* ||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 (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;//; + ##] + + + + + + + + -- 2.39.2