(* *)
(**************************************************************************)
-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)
- ].
+include "PTS/subst.ma".
-ndefinition lift ≝ λt.λp.lift_aux t 0 p.
+(*************************** substl *****************************)
-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)
+nlet rec substl (G:list T) (N:T) : list T ≝
+ match G with
+ [ nil ⇒ nil T
+ | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
].
-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.
+nlemma substl_cons: ∀A,N.∀G.
+substl (A::G) N = (subst_aux A (length T G) N)::(substl G 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))
- ].
-
+(*
+nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
+/2/; nqed.*)
-(*****************************************************************)
+(****************************************************************)
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)
+ | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
+ | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 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)
+ TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 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)
+ TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 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.
+
+notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+interpretation "type judgement" 'TJ G A B = (TJ G A B).
+
+(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
(**** definitions ****)
ninductive Glegal (G: list T) : Prop ≝
-glegalk : ∀A,B.TJ G A B → Glegal G.
+glegalk : ∀A,B. 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.
+ | is_term: ∀B.G ⊢ A:B → Gterm G A
+ | is_type: ∀B.G ⊢ B:A → Gterm G A.
ninductive Gtype (G: list T) (A:T) : Prop ≝
-gtypek: ∀i.TJ G A (Sort i) → Gtype G A.
+gtypek: ∀i.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.
+gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
ninductive Tlegal (A:T) : Prop ≝
tlegalk: ∀G. Gterm G A → Tlegal A.
*)
ntheorem start_lemma1: ∀G.∀i,j.
-A i j → Glegal G → TJ G (Sort i) (Sort j).
+A i j → Glegal G → 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 ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
#G; #A; #C; #n; #i; #p; #tjC; #tjn;
napplyS (weak G (Rel n));//. (* bello *)
(*
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)).
+Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
#G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
napply (absurd … abs); //;
*)
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. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A →
+ ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N].
#E; #A; #B; #M; #tjMB; nelim tjMB;
##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D;
##[nnormalize; #isnil; ndestruct;
##]
##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D;
##[#N; #Heq; #tjN;
- nrewrite > (delift (lift N O) A1 O O O ??); //;
+ nrewrite > (delift (lift N O 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/;
+ #tjN1; nnormalize; ndestruct;
+ napplyS 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/;
+ (* napplyS weak non va *)
+ ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq;
+ napplyS weak; /2/;
##]
##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
- #G1; #D; #N; #Heq; #tjN;
+ #G1; #D; #N; #Heq; #tjN; nnormalize;
napply (prod … Ax);
##[/2/;
- ##|
+ ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
+ nrewrite < Heq1;
+ napply (Hind2 ? (P::D));nnormalize;//;
##]
##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
+ #G1; #D; #N; #Heq; #tjN; nnormalize in Hind1 ⊢ %;
+ nrewrite > (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?));
+ nrewrite > (subst_lemma R S N ? 0);
+ napplyS app; /2/;
+ ##|#G; #P; #Q; #R; #i; #tjR; #tjProd; #Hind1; #Hind2;
#G1; #D; #N; #Heq; #tjN; nnormalize;
- ncheck app.
-
+ napplyS abs;
+ ##[nnormalize in Hind2; /2/;
+ ##|(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
+ ngeneralize in match (Hind1 G1 (P::D) N ? tjN);
+ ##[#H; nnormalize in H; napplyS H;##|nnormalize; //##]
+ ##|##]
+ ##|
+
-
-
-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 / blobdiff