]> matita.cs.unibo.it Git - helm.git/commitdiff
Keeping only lift_aux e subst_aux (renamed to lift and subst).
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 23 Mar 2010 07:32:33 +0000 (07:32 +0000)
From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

helm/software/matita/nlibrary/PTS/gpts.ma
helm/software/matita/nlibrary/PTS/subst.ma

index d43efef3f1064eaae0a7447ae5836b97b3d37158..9a53cc00f4d771aad41d00ceca43d5e6a87d4460 100644 (file)
@@ -19,17 +19,18 @@ 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.
-*)
+/2/; nqed.*)
 
 (****************************************************************)
 
@@ -37,20 +38,15 @@ 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.
-
-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 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 →
@@ -105,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 *)
  (*
@@ -117,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)) (S n).
 #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
   ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
      napply (absurd … abs); //; 
@@ -178,12 +174,94 @@ 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;
+       #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;
@@ -199,49 +277,25 @@ ntheorem substitution_tj:
      #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;//;
-    ##]
-       
-
-
 
 
 
index 7ca2fdc03f059c0df5b292fdc3f204567f9e3143..a37074b4d306a60b85f7909bcecc2637b7849d82 100644 (file)
@@ -22,61 +22,64 @@ ninductive T : Type ≝
   | Prod: T → T → T (* type, body *)
 .
 
-nlet rec lift_aux t k p ≝
+nlet rec lift t k p ≝
   match t with 
     [ Sort n ⇒ Sort n
     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
-    | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
-    | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
-    | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
+    | App m n ⇒ App (lift m k p) (lift n k p)
+    | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
+    | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
     ].
 
-ndefinition lift ≝ λt.λp.lift_aux t 0 p.
+(* 
+ndefinition lift ≝ λt.λp.lift_aux t 0 p.*)
 
-notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift $n $M}.
-notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift_aux $n $k $M}.
+notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift O $M}.
+notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift $n $k $M}.
 
-interpretation "Lift" 'Lift n M = (lift M n).
-interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n).
+(* interpretation "Lift" 'Lift n M = (lift M n). *)
+interpretation "Lift" 'Lift n k M = (lift M k n).
 
-nlet rec subst_aux t k a ≝ 
+nlet rec subst t k a ≝ 
   match t with 
     [ Sort n ⇒ Sort n
     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
-        (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
-    | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
-    | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
-    | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
+        (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
+    | App m n ⇒ App (subst m k a) (subst n k a)
+    | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
+    | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
     ].
 
+(* meglio non definire 
 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
-
 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
-notation "M [ k ← N]" non associative with precedence 90 for @{'Subst_aux $M $k $N}.
+*)
+
+notation "M [ k ← N]" non associative with precedence 90 for @{'Subst $M $k $N}.
 
-interpretation "Subst" 'Subst N M = (subst N M).
-interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N).
+(* interpretation "Subst" 'Subst N M = (subst N M). *)
+interpretation "Subst" 'Subst M k N = (subst M k N).
 
 (*** properties of lift and subst ***)
 
-nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
+nlemma lift_0: ∀t:T.∀k. lift t k 0 = t.
 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k); 
 nnormalize;//;nqed.
 
-nlemma lift_0: ∀t:T. lift t 0 = t.
-#t; nelim t; nnormalize; //; nqed.
+(* nlemma lift_0: ∀t:T. lift t 0 = t.
+#t; nelim t; nnormalize; //; nqed. *)
 
-nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
+nlemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
 //; nqed.
 
-nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
+nlemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
 //; nqed.
 
-nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
-#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
+nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
+#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
 
-nlemma lift_lift_aux: ∀t.∀i,j.j ≤ i  → ∀h,k. 
-lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
+nlemma lift_lift: ∀t.∀i,j.j ≤ i  → ∀h,k. 
+  lift (lift t k i) (j+k) h = lift t k (i+h).
 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
 napply (leb_elim (S n) k); #Hnk;nnormalize;
   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
@@ -86,17 +89,19 @@ napply (leb_elim (S n) k); #Hnk;nnormalize;
   ##]
 nqed.
 
-nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
+nlemma lift_lift1: ∀t.∀i,j,k. 
+  lift(lift t k j) k i = lift t k (j+i).
 #t;/3/; nqed.
 
-nlemma lift_lift_aux2: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
+nlemma lift_lift2: ∀t.∀i,j,k. 
+  lift (lift t k j) (j+k) i = lift t k (j+i).
 #t; /2/; nqed.
 
+(*
 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
-nnormalize; //; nqed.
+nnormalize; //; nqed. *)
 
-nlemma subst_lift_aux_k: ∀A,B.∀k. 
-  subst_aux (lift_aux B k 1) k A = B.
+nlemma subst_lift_k: ∀A,B.∀k. subst (lift B k 1) k A = B.
 #A; #B; nelim B; nnormalize; /2/; #n; #k;
 napply (leb_elim (S n) k); nnormalize; #Hnk;
   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
@@ -108,39 +113,38 @@ napply (leb_elim (S n) k); nnormalize; #Hnk;
   ##]
 nqed.
 
+(*
 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
-nnormalize; //; nqed.
-
-nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
-//; nqed.
+nnormalize; //; nqed. *)
 
-nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
+nlemma subst_sort: ∀A.∀n,k. subst (Sort n) k A = Sort n.
 //; nqed.
 
-nlemma subst_rel: ∀A.subst A (Rel O) = A.
+nlemma subst_rel: ∀A.subst (Rel 0) 0 A = A.
 nnormalize; //; nqed.
 
 nlemma subst_rel1: ∀A.∀k,i. i < k → 
-  subst_aux (Rel i) k A = Rel i.
+  subst (Rel i) k A = Rel i.
 #A; #k; #i; nnormalize; #ltik;
 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
 
-nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
+nlemma subst_rel2: ∀A.∀k. 
+  subst (Rel k) k A = lift A 0 k.
 #A; #k; nnormalize; 
 nrewrite > (lt_to_leb_false (S k) k ?); //; 
 nrewrite > (eq_to_eqb_true … (refl …)); //;
 nqed.
 
 nlemma subst_rel3: ∀A.∀k,i. k < i → 
-  subst_aux (Rel i) k A = Rel (i-1).
+  subst (Rel i) k A = Rel (i-1).
 #A; #k; #i; nnormalize; #ltik;
 nrewrite > (lt_to_leb_false (S i) k ?); /2/; 
 nrewrite > (not_eq_to_eqb_false i k ?); //;
 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
 nqed.
 
-nlemma lift_subst_aux_ijk: ∀A,B.∀i,j,k.
-  lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
+nlemma lift_subst_ijk: ∀A,B.∀i,j,k.
+  lift (subst B (j+k) A) k i = subst (lift B k i) (j+k+i) A.
 #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
   ##[nelim (leb (S n) k);
@@ -151,7 +155,7 @@ napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
     ##[nrewrite > (lt_to_leb_false (S n) k ?);
        ##[ncut (j+k+i = n+i);##[//;##] #Heq;
           nrewrite > Heq; nrewrite > (subst_rel2 A ?);
-          nnormalize; napplyS lift_lift_aux;//;
+          nnormalize; napplyS lift_lift;//;
        ##|/2/;
        ##]
     ##|ncut (j + k < n);
@@ -171,7 +175,7 @@ napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
 nqed. 
 
 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
-  subst_aux (lift_aux B i (S k)) j A = (lift_aux B 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;
@@ -194,8 +198,8 @@ nqed.
 (********************* substitution lemma ***********************)    
 
 nlemma subst_lemma: ∀A,B,C.∀k,i. 
-  subst_aux (subst_aux A i B) (k+i) C = 
-    subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
+  subst (subst A i B) (k+i) C = 
+    subst (subst A (S (k+i)) C) i (subst B k C).
 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
 #n; #i; napply (leb_elim (S n) i); #Hle;
   ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
@@ -208,7 +212,7 @@ nlemma subst_lemma: ∀A,B,C.∀k,i.
        nrewrite > (le_to_leb_true i (k+i) ?); //;
        nrewrite > (subst_rel2 …); nnormalize; 
        napply symmetric_eq; 
-       napplyS (lift_subst_aux_ijk C B i k O);
+       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);
          nrewrite > (le_to_leb_true n (k+i) ?);