From: Andrea Asperti Date: Wed, 17 Mar 2010 14:58:51 +0000 (+0000) Subject: qualche caso del lemma 5.2.11 X-Git-Tag: make_still_working~3000 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c8ec2f3e2aaa71efa702f86bacc95e393778a56f;p=helm.git qualche caso del lemma 5.2.11 --- diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma index c6aeb1bd4..d43efef3f 100644 --- a/helm/software/matita/nlibrary/PTS/gpts.ma +++ b/helm/software/matita/nlibrary/PTS/gpts.ma @@ -21,7 +21,16 @@ nlet rec substl (G:list T) (N:T) : list T ≝ [ nil ⇒ nil T | cons A D ⇒ ((subst_aux 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. +*) + (****************************************************************) naxiom A: nat → nat → Prop. @@ -31,6 +40,8 @@ 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) @@ -39,7 +50,7 @@ ninductive TJ: list T → T → T → Prop ≝ | 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 a B) | 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 → @@ -188,13 +199,18 @@ ntheorem substitution_tj: #G1; #D; #N; #Heq; #tjN; nnormalize; napply (prod … Ax); ##[/2/; - ##|(* metas not found *) - napplyS (Hind2 G1 (P::D) N ); - nnormalize; + ##|ncheck (Hind2 G1 (P::D) N ? tjN). + 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 app. + nlapply (subst_lemma R S N (length ? D) 0); #sl; + nrewrite < (plus_n_O ?) in sl; #sl; + nrewrite > sl; + napply app; nnormalize in Hind1;/2/; + ##|