updating the structures for sorts

[helm.git] / helm / software / matita / nlibrary / PTS / gpts.ma

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index c6aeb1bd49c942deadbaea10fbfa49fe94de208a..9af90225239158d425d63dd8cd90d8b2fbc2b1a7 100644 (file)
--- a/helm/software/matita/nlibrary/PTS/gpts.ma
+++ b/helm/software/matita/nlibrary/PTS/gpts.ma
@@ -19,27 +19,34 @@ include "PTS/subst.ma".
 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.*)
+
 (****************************************************************)
 
 naxiom A: nat → nat → Prop.
 naxiom R: nat → nat → nat → Prop.
 naxiom conv: T → T → Prop.
 
-nlemma mah: ∀A,i. lift A i = lift_aux A 0 i.
-//; nqed.
-
 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 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 →
@@ -94,7 +101,7 @@ A i j → Glegal G → G ⊢ Sort i: Sort j.
 (* 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 *)
  (*
@@ -106,7 +113,7 @@ G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i)
 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); //; 
@@ -167,13 +174,11 @@ ntheorem substitution_tj:
       ##]
   ##|#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;
-       (* napplyS start non va *)
-       ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
-       napplyS start;/2/; 
+       #tjN1; nnormalize; ndestruct;             
+       napplyS start; /2/;
     ##]
   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
      #G1; #D; #N; ncases D; nnormalize;
@@ -188,44 +193,27 @@ ntheorem substitution_tj:
      #G1; #D; #N; #Heq; #tjN; nnormalize;
      napply (prod … Ax); 
     ##[/2/;
-    ##|(* metas not found *)
-       napplyS (Hind2 G1 (P::D) N );
-       nnormalize;
+    ##|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;//;
-    ##]
-       
-
-
+