From: Andrea Asperti Date: Tue, 23 Mar 2010 17:50:12 +0000 (+0000) Subject: One more case. X-Git-Tag: make_still_working~2977 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=10e8d3c7da0978dd482e703004ced1138fdea8c0;p=helm.git One more case. From: asperti --- diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma index 9a53cc00f..d7fbe0440 100644 --- a/helm/software/matita/nlibrary/PTS/gpts.ma +++ b/helm/software/matita/nlibrary/PTS/gpts.ma @@ -177,92 +177,8 @@ ntheorem substitution_tj: 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; - 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/; + #tjN1; nnormalize; ndestruct; + napplyS start; /2/; ##] ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2; #G1; #D; #N; ncases D; nnormalize; @@ -279,21 +195,28 @@ ntheorem substitution_tj: ##[/2/; ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1; nrewrite < Heq1; - napply (Hind2 ? (P::D));//; + napply (Hind2 ? (P::D));nnormalize;//; ##] ##|#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) ?). + nrewrite > (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?)); +(* + napplyS (app (substl D N@G1) (subst P (length T D) N) A (subst R (length T D) N) (subst 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/; + ##|#G; #P; #Q; #R; #i; #tjR; #tjProd; #Hind1; #Hind2; + #G1; #D; #N; #Heq; #tjN; nnormalize; + 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; //##] + ##|##] ##| + diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma index a37074b4d..5282e86ba 100644 --- a/helm/software/matita/nlibrary/PTS/subst.ma +++ b/helm/software/matita/nlibrary/PTS/subst.ma @@ -178,7 +178,7 @@ ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → subst (lift B i (S k)) j A = (lift 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; + 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; @@ -211,7 +211,7 @@ nlemma subst_lemma: ∀A,B,C.∀k,i. ##[nrewrite > eqni; nrewrite > (le_to_leb_true i (k+i) ?); //; nrewrite > (subst_rel2 …); nnormalize; - napply symmetric_eq; + napply sym_eq; napplyS (lift_subst_ijk C B i k O); ##|napply (leb_elim (S (n-1)) (k+i)); #nk; ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);