One more case.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index 9a53cc00f4d771aad41d00ceca43d5e6a87d4460..d7fbe04403dc33f349268ab6ceb4186c3e395ba1 100644 (file)
--- 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 a37074b4d306a60b85f7909bcecc2637b7849d82..5282e86baa5465c7e14e4eccaadd99dcf80b1eb6 100644 (file)
--- 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);