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))
+ | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
].
(*
nlemma substl_cons: ∀A,N.∀G.
substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
//; nqed.
+*)
+(*
nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
-/2/; nqed.
-*)
+/2/; nqed.*)
(****************************************************************)
naxiom R: nat → nat → nat → Prop.
naxiom conv: T → T → Prop.
-nlemma mah: ∀A,i. lift A i = lift_aux A 0 i.
-//; nqed.
-
-ncheck subst.
-
ninductive TJ: list T → T → T → Prop ≝
| 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 1)
+ | 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 a B)
+ 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 →
(* bello *) nqed.
ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
-G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (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 < |G| → 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); //;
##]
##|#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;
+ #tjN1; nnormalize; ndestruct;
+ ncheck( let clause_829:
+ ∀x1947: ?.
+ ∀x1948: ?.
+ ∀x1949: ?.
+ ∀x1950: ?.
+ ∀x1951: ?.
+ eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
+ (subst (lift x1947 x1949 x1951) (plus x1948 (plus x1949 x1951))
+ x1950)
+ ≝ λx1947:?.
+ λx1948:?.
+ λx1949:?.
+ λx1950:?.
+ λx1951:?.
+ rewrite_l nat (plus (plus x1948 x1949) x1951)
+ (λx:nat.
+ eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
+ (subst (lift x1947 x1949 x1951) x x1950))
+ (lift_subst_ijk x1950 x1947 x1951 x1948 x1949)
+ (plus x1948 (plus x1949 x1951))
+ (associative_plus x1948 x1949 x1951) in
+ let clause_60: ∀x156: ?. eq nat (S x156) (plus x156 (S O))
+ ≝ λx156:?.
+ rewrite_r nat (plus x156 O) (λx:nat. eq nat (S x) (plus x156 (S O)))
+ (plus_n_Sm x156 O) x156 (plus_n_O x156) in
+ let clause_996 :
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (S O)) ?))
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
+ ≝ rewrite_l nat (S (length T L))
+ (λx:nat.
+ eq Type
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) x N1))
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (refl Type
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (plus (length T L) (S O)) (clause_60 (length T L)) in
+ let clause_995:
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
+ ≝ rewrite_l nat (S O)
+ (λx:nat.
+ eq Type
+ (TJ (cons T (subst ? ? ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? x) ?))
+ (TJ
+ (cons T (subst H (length T L) N1)
+ (append T (substl L N1) G1)) (Rel O)
+ (subst (lift H O (S O)) (S (length T L)) N1))) clause_996
+ (plus O (S O)) (plus_O_n (S O)) in
+ rewrite_r T
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)
+ (λx:T.
+ eq Type
+ (TJ (cons T (subst ? (plus ? O) ?) ?) (Rel O) x)
+ (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ (rewrite_l nat ?
+ (λx:nat.
+ eq Type
+ (TJ (cons T (subst ? x ?) ?) (Rel O)
+ (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
+ (TJ
+ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
+ (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
+ clause_995 (plus ? O) (plus_n_O ?))
+ (lift (subst ? (plus ? O) ?) O (S O))
+ (clause_829 ? ? O ? (S O))
+).
+ napplyS start;
+ (* napplyS start; *)
(* napplyS start non va *)
ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
+ ncheck start.
napplyS start;/2/;
##]
##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
#G1; #D; #N; #Heq; #tjN; nnormalize;
napply (prod … Ax);
##[/2/;
- ##|ncheck (Hind2 G1 (P::D) N ? tjN).
- ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
- nrewrite < Heq1;
+ ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
+ nrewrite < Heq1;
napply (Hind2 ? (P::D));//;
##]
##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
#G1; #D; #N; #Heq; #tjN; nnormalize;
+ ncheck (
+ (subst (subst_aux S (length T D) N)
+ (subst_aux R (length T D) N))
+ ).
+ napplyS (app (substl D N@G1) (subst_aux P (length T D) N) A (subst_aux R (length T D) N) (subst_aux S (length T D) N) ?).
nlapply (subst_lemma R S N (length ? D) 0); #sl;
nrewrite < (plus_n_O ?) in sl; #sl;
nrewrite > sl;
+ nauto demod;
napply app; nnormalize in Hind1;/2/;
##|
-
-
-
-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