]> matita.cs.unibo.it Git - helm.git/commitdiff
Splitted gpts in two files.
authorAndrea Asperti <andrea.asperti@unibo.it>
Wed, 17 Mar 2010 11:51:01 +0000 (11:51 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Wed, 17 Mar 2010 11:51:01 +0000 (11:51 +0000)
helm/software/matita/nlibrary/PTS/gpts.ma
helm/software/matita/nlibrary/PTS/subst.ma [new file with mode: 0644]

index bf149812dff02552e64dca5120802446df2158d4..c6aeb1bd49c942deadbaea10fbfa49fe94de208a 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
-include "basics/list2.ma".
-
-ninductive T : Type ≝
-  | Sort: nat → T
-  | Rel: nat → T 
-  | App: T → T → T 
-  | Lambda: T → T → T (* type, body *)
-  | Prod: T → T → T (* type, body *)
-.
-
-nlet rec lift_aux 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)
-    ].
-
-ndefinition lift ≝ λt.λp.lift_aux t 0 p.
-
-nlet rec subst_aux 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)
-    ].
-
-ndefinition subst ≝ λa.λt.subst_aux t 0 a.
-
-(*** properties of lift and subst ***)
-nlemma lift_aux_0: ∀t:T.∀k. lift_aux 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_sort: ∀i,k. lift (Sort i) k = Sort i.
-//; nqed.
-
-nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
-//; 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,k,k1. k ≤ k1 → k1 ≤ k+j → 
-lift_aux (lift_aux t k j) k1 i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; #k1; #lel; #ler; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
-  ##|nrewrite > (lt_to_leb_false (S n+j) k ?); 
-     nnormalize;//;napply (lt_to_le_to_lt ? (S n));
-      ##[napply not_le_to_lt;/2/;
-      ##|(* lento /2/; *) napply le_S_S;/1/;
-  ##]
-nqed. *)
-
-nlemma lift_lift_aux: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
-  ##|nrewrite > (lt_to_leb_false (S n+j) k ?); 
-     nnormalize;//; napply (lt_to_le_to_lt ? (S n));
-      ##[napply not_le_to_lt;//;
-      ##|napply le_S_S;//;
-  ##]
-nqed.
-
-nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
-  ##|nrewrite > (lt_to_leb_false (S n+j) (j+k) ?); 
-     nnormalize;//; napply le_S_S; napplyS monotonic_le_plus_r;
-     /3/;
-  ##]
-nqed.
-
-nlemma lift_lift_aux2: ∀t.∀i,j.j ≤ i  → ∀h,k. 
-lift_aux (lift_aux t k i) (j+k) h = lift_aux 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/;
-  ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); 
-     nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
-     napply le_plus;//;napply not_lt_to_le;/2/;
-  ##]
-nqed.
-
-nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
-nnormalize; //;
-nqed.
-
-nlemma subst_lift_aux_k: ∀A,B.∀k. 
-  subst_aux (lift_aux 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;//;
-  ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
-      ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
-         nnormalize;/2/; napply (not_to_not … Hnk);//;
-      ##|napply le_S; napplyS (not_le_to_lt (S n) k 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.
-
-nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
-//; nqed.
-
-nlemma subst_rel: ∀A.subst A (Rel O) = A.
-nnormalize; //; nqed.
-
-nlemma subst_rel1: ∀A.∀k,i. i < k → 
-  subst_aux (Rel i) k A = Rel i.
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
+include "PTS/subst.ma".
 
-nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A 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).
-#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.
-
-(* versione con plus 
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
-  lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
-  ##[nelim (leb (S n) k); 
-    ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/;
-    ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/;
-    ##]
-  ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
-    ##[nrewrite > (lt_to_leb_false (S n) k ?);
-       ##[ncut (j+k+1 = n+1);##[//;##] #Heq;
-          nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
-          napplyS lift_lift_aux2 (* bello *);//;
-       ##|/2/;
-       ##]
-    ##|ncut (j + k < n);
-      ##[napply not_eq_to_le_to_lt;
-        ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
-      ##|#ltjkn;
-         ncut (O < n); ##[/2/; ##] #posn;
-         ncut (k ≤ n); ##[/2/; ##] #lekn;
-         nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
-          ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
-             nrewrite > (subst_rel3 A (j+k+1) (n+1) ?);
-              ##[nrewrite < (plus_minus_m_m … posn);//;
-              ##|napplyS monotonic_lt_plus_l; //;
-              ##]
-          ##|napply le_S_S; 
-             napply (not_eq_to_le_to_le_minus … lekn);
-             /2/; (* come fa? *)
-          ##]
-     ##]
-  ##]
-nqed. *)
-
-naxiom lift_subst_aux_kij: ∀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_aux_k: ∀A,B.∀j,k.
-  lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
-  ##[nelim (leb (S n) k); 
-    ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/;
-    ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/;
-    ##]
-  ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
-    ##[nrewrite > (lt_to_leb_false (S n) k ?);
-       ##[ncut (S(j+k) = n+1);##[//;##] #Heq;
-          nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
-          napplyS lift_lift_aux2 (* bello *);//;
-       ##|/2/;
-       ##]
-    ##|ncut (j + k < n);
-      ##[napply not_eq_to_le_to_lt;
-        ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
-      ##|#ltjkn;
-         ncut (O < n); ##[/2/; ##] #posn;
-         ncut (k ≤ n); ##[/2/; ##] #lekn;
-         nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
-          ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
-             nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?);
-              ##[nrewrite < (plus_minus_m_m … posn);//;
-              ##|ncut (S n = n +1); /2/;
-              ##]
-          ##|napply le_S_S;  (* /3/;*)
-             napply (not_eq_to_le_to_le_minus … lekn);
-             /3/; (* come fa? *)
-          ##]
-     ##]
-  ##]
-nqed. 
-
-(*
-nlemma lift_subst_aux_k: ∀A,B.∀k. 
-  lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A.
-#A; #B; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) k); nnormalize; #Hnk;
-  ##[nrewrite > (le_to_leb_true ?? Hnk);
-     nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/;
-  ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?);
-    ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n);
-       napply not_lt_to_le; napply Hnk; ##]      
-    napply (eqb_elim n k);#eqnk;
-      ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/;
-         nnormalize; nrewrite < eqnk; //; (* strano *)
-      ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/;
-         nnormalize; 
-         ncut (O < n);
-          ##[napply not_le_to_lt;#len;
-             napply eqnk; napply le_to_le_to_eq;
-              ##[napply transitive_le; //;
-              ##|napply not_lt_to_le; /2/;
-              ##] 
-          ##|#posn;
-             nrewrite > (lt_to_leb_false (S (n - 1)) k ?);
-             ##[nnormalize;
-                (* nrewrite < (minus_plus_m_m n 1); *)
-                nrewrite < (plus_minus_m_m n 1 ?);//;
-             ##|napply le_S_S; napply not_eq_to_le_to_le_minus;
-                ##[/2/;
-                ##|napply (not_lt_to_le … Hnk);
-                ##]
-             ##]
-          ##]
-       ##]
-  ##]
-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).
-#A; #B; nelim B; nnormalize; /2/;
-   ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
-      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;
-      ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
-      ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
-        ##[nnormalize; 
-           nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
-           nnormalize; /2/; napply (not_to_not …len);
-           #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
-           nnormalize; //; 
-        ##|napply le_S_S; napply (transitive_le … ltjk);
-           napply le_plus;//; napply not_lt_to_le; /2/;
-        ##]
-    ##]
-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).
-#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
-#n; #i; napply (leb_elim (S n) i); #Hle;
-  ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
-     ncut (n ≤ k+i); ##[/2/##] #len;
-     nrewrite > (subst_rel1 C (k+i) n ltn);
-     nrewrite > (le_to_leb_true n (k+i) len);
-     nrewrite > (subst_rel1 … Hle);//;
-  ##|napply (eqb_elim n i); #eqni;
-    ##[nrewrite > eqni; 
-       nrewrite > (le_to_leb_true i (k+i) ?); //;
-       nrewrite > (subst_rel2 …); nnormalize; 
-       napply symmetric_eq; 
-       napplyS (lift_subst_aux_kij 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) ?);
-        ##[nrewrite > (subst_rel3 ? i n ?);//;
-           napply not_eq_to_le_to_lt;
-            ##[/2/;
-            ##|napply not_lt_to_le;/2/;
-            ##]
-        ##|napply (transitive_le … nk);//;
-        ##]
-      ##|ncut (i < n);
-        ##[napply not_eq_to_le_to_lt; ##[/2/]
-           napply (not_lt_to_le … Hle);##]
-         #ltin; ncut (O < n); ##[/2/;##] #posn;
-         napply (eqb_elim (n-1) (k+i)); #H
-         ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
-            nrewrite > (lt_to_leb_false n (k+i) ?);
-            ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); 
-              ##[nnormalize;
-              ##|nrewrite < H; napplyS plus_minus_m_m;//;
-              ##]
-            ##|nrewrite < H; napply (lt_O_n_elim … posn);
-               #m; nnormalize;//;
-            ##]
-         ##|ncut (k+i < n-1);
-            ##[napply not_eq_to_le_to_lt;
-              ##[napply symmetric_not_eq; napply H;
-              ##|napply (not_lt_to_le … nk);
-              ##]
-            ##]
-            #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
-            ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
-              ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
-                 nrewrite > (subst_rel3 ? i (n-1) ?);//;
-                 napply (le_to_lt_to_lt … Hlt);//;
-              ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
-              ##]
-            ##|napply (transitive_lt … Hlt);
-               napply (lt_O_n_elim … posn);
-               #m; nnormalize;//;
-            ##]
-          ##]
-          nrewrite <H;
-          ncut (∃m:nat. S m = n);
-          ##[napply (lt_O_n_elim … posn); #m;@ m;//;
-            ##|*; #m; #Hm; nrewrite < Hm;
-               nrewrite > (delift ???????);nnormalize;/2/;
-          ##]
-nqed.
-  
 (*************************** substl *****************************)
 
 nlet rec substl (G:list T) (N:T) : list T ≝  
@@ -362,15 +22,17 @@ nlet rec substl (G:list T) (N:T) : list T ≝
     | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
     ].
     
-
-(*****************************************************************)
+(****************************************************************)
 
 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 [] (Sort i) (Sort j)
+  | 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)
   | weak: ∀G.∀A,B,C.∀i.
      TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1)
@@ -382,23 +44,26 @@ ninductive TJ: list T → T → T → Prop ≝
      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 →
      TJ G A B → TJ G B (Sort i) → TJ G A C.
-ninverter TJ_inv2 for TJ (%?%) : Prop.
+     
+notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+interpretation "type judgement" 'TJ G A B = (TJ G A B).
+
+(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
 
 (**** definitions ****)
 
 ninductive Glegal (G: list T) : Prop ≝
-glegalk : ∀A,B.TJ G A B → Glegal G.
+glegalk : ∀A,B. G ⊢ A : B → Glegal G.
 
 ninductive Gterm (G: list T) (A:T) : Prop ≝
-  | is_term: ∀B.TJ G A B → Gterm G A
-  | is_type: ∀B.TJ G B A → Gterm G A.
+  | is_term: ∀B.G ⊢ A:B → Gterm G A
+  | is_type: ∀B.G ⊢ B:A → Gterm G A.
 
 ninductive Gtype (G: list T) (A:T) : Prop ≝ 
-gtypek: ∀i.TJ G A (Sort i) → Gtype G A.
+gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
 
 ninductive Gelement (G:list T) (A:T) : Prop ≝
-gelementk: ∀B.TJ G A B → Gtype G B → Gelement G A.
+gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
 
 ninductive Tlegal (A:T) : Prop ≝ 
 tlegalk: ∀G. Gterm G A → Tlegal A.
@@ -423,13 +88,13 @@ subst C A
 *)
 
 ntheorem start_lemma1: ∀G.∀i,j. 
-A i j → Glegal G → TJ G (Sort i) (Sort j).
+A i j → Glegal G → G ⊢ Sort i: Sort j.
 #G; #i; #j; #axij; #Gleg; ncases Gleg; 
 #A; #B; #tjAB; nelim tjAB; /2/;
 (* bello *) nqed.
 
 ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
-TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S i)).
+G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i).
 #G; #A; #C; #n; #i; #p; #tjC; #tjn;
  napplyS (weak G (Rel n));//. (* bello *)
  (*
@@ -441,7 +106,7 @@ TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S
 nqed.
   
 ntheorem start_lemma2: ∀G.
-Glegal G → ∀n. n < length T G → TJ 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); //; 
@@ -493,8 +158,8 @@ ntheorem substitution_tj:
 *)
 
 ntheorem substitution_tj: 
-∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A → 
-  TJ ((substl D N)@G) (subst_aux M (length ? D) N) (subst_aux B (length ? D) N).
+∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A → 
+  ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N].
 #E; #A; #B; #M; #tjMB; nelim tjMB; 
   ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D; 
       ##[nnormalize; #isnil; ndestruct;
@@ -506,31 +171,26 @@ ntheorem substitution_tj:
        nnormalize in Heq; ndestruct;/2/;
     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
        #tjN1; 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;/2/;
+       (* napplyS start non va *)
+       ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
+       napplyS start;/2/; 
     ##]
   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
      #G1; #D; #N; ncases D; nnormalize;
     ##[#Heq; ndestruct; #tjN; //;
     ##|#H; #L; #Heq;
        #tjN1; ndestruct;
-       (* porcherie *)
-       ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
-       nrewrite > Heq;
-       nrewrite < (lift_subst_aux_k N P (length T L) O);
-       nrewrite < (lift_subst_aux_k N Q (length T L) O);
-       nrewrite < (plus_n_O (length T L));
-       napply weak;/2/;
+       (* napplyS weak non va *)
+       ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq;
+       napplyS weak; /2/;
     ##]
   ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
-     #G1; #D; #N; #Heq; #tjN;
+     #G1; #D; #N; #Heq; #tjN; nnormalize;
      napply (prod … Ax); 
     ##[/2/;
-    ##|
+    ##|(* metas not found *)
+       napplyS (Hind2 G1 (P::D) N );
+       nnormalize;
     ##]
   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
      #G1; #D; #N; #Heq; #tjN; nnormalize;
diff --git a/helm/software/matita/nlibrary/PTS/subst.ma b/helm/software/matita/nlibrary/PTS/subst.ma
new file mode 100644 (file)
index 0000000..7ca2fdc
--- /dev/null
@@ -0,0 +1,264 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basics/list2.ma".
+
+ninductive T : Type ≝
+  | Sort: nat → T
+  | Rel: nat → T 
+  | App: T → T → T 
+  | Lambda: T → T → T (* type, body *)
+  | Prod: T → T → T (* type, body *)
+.
+
+nlet rec lift_aux 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)
+    ].
+
+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}.
+
+interpretation "Lift" 'Lift n M = (lift M n).
+interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n).
+
+nlet rec subst_aux 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)
+    ].
+
+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}.
+
+interpretation "Subst" 'Subst N M = (subst N M).
+interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N).
+
+(*** properties of lift and subst ***)
+
+nlemma lift_aux_0: ∀t:T.∀k. lift_aux 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_sort: ∀i,k. lift (Sort i) k = Sort i.
+//; nqed.
+
+nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
+//; 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).
+#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/;
+  ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); 
+     nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
+     napply le_plus;//;napply not_lt_to_le;/2/;
+  ##]
+nqed.
+
+nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux 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).
+#t; /2/; nqed.
+
+nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
+nnormalize; //; nqed.
+
+nlemma subst_lift_aux_k: ∀A,B.∀k. 
+  subst_aux (lift_aux 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;//;
+  ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
+      ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
+         nnormalize;/2/; napply (not_to_not … Hnk);//;
+      ##|napply le_S; napplyS (not_le_to_lt (S n) k 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.
+
+nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
+//; nqed.
+
+nlemma subst_rel: ∀A.subst A (Rel O) = A.
+nnormalize; //; nqed.
+
+nlemma subst_rel1: ∀A.∀k,i. i < k → 
+  subst_aux (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.
+#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).
+#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.
+#A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
+napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
+  ##[nelim (leb (S n) k);
+    ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/;
+    ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/;
+    ##]
+  ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
+    ##[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;//;
+       ##|/2/;
+       ##]
+    ##|ncut (j + k < n);
+      ##[napply not_eq_to_le_to_lt;
+        ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
+      ##|#ltjkn;
+         ncut (O < n); ##[/2/; ##] #posn;
+         ncut (k ≤ n); ##[/2/; ##] #lekn;
+         nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
+          ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
+             nrewrite > (subst_rel3 A (j+k+i) (n+i) ?);
+              ##[/3/; ##|/2/; ##]
+          ##|napply le_S_S;/3/;  (* /3/;*)
+          ##]
+     ##]
+  ##]
+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).
+#A; #B; nelim B; nnormalize; /2/;
+   ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
+      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;
+      ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
+      ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
+        ##[nnormalize; 
+           nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
+           nnormalize; /2/; napply (not_to_not …len);
+           #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
+           nnormalize; //; 
+        ##|napply le_S_S; napply (transitive_le … ltjk);
+           napply le_plus;//; napply not_lt_to_le; /2/;
+        ##]
+    ##]
+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).
+#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
+#n; #i; napply (leb_elim (S n) i); #Hle;
+  ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
+     ncut (n ≤ k+i); ##[/2/##] #len;
+     nrewrite > (subst_rel1 C (k+i) n ltn);
+     nrewrite > (le_to_leb_true n (k+i) len);
+     nrewrite > (subst_rel1 … Hle);//;
+  ##|napply (eqb_elim n i); #eqni;
+    ##[nrewrite > eqni; 
+       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);
+    ##|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) ?);
+        ##[nrewrite > (subst_rel3 ? i n ?);//;
+           napply not_eq_to_le_to_lt;
+            ##[/2/;
+            ##|napply not_lt_to_le;/2/;
+            ##]
+        ##|napply (transitive_le … nk);//;
+        ##]
+      ##|ncut (i < n);
+        ##[napply not_eq_to_le_to_lt; ##[/2/]
+           napply (not_lt_to_le … Hle);##]
+         #ltin; ncut (O < n); ##[/2/;##] #posn;
+         napply (eqb_elim (n-1) (k+i)); #H
+         ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
+            nrewrite > (lt_to_leb_false n (k+i) ?);
+            ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); 
+              ##[nnormalize;
+              ##|nrewrite < H; napplyS plus_minus_m_m;//;
+              ##]
+            ##|nrewrite < H; napply (lt_O_n_elim … posn);
+               #m; nnormalize;//;
+            ##]
+         ##|ncut (k+i < n-1);
+            ##[napply not_eq_to_le_to_lt;
+              ##[napply symmetric_not_eq; napply H;
+              ##|napply (not_lt_to_le … nk);
+              ##]
+            ##]
+            #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
+            ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
+              ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
+                 nrewrite > (subst_rel3 ? i (n-1) ?);//;
+                 napply (le_to_lt_to_lt … Hlt);//;
+              ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
+              ##]
+            ##|napply (transitive_lt … Hlt);
+               napply (lt_O_n_elim … posn);
+               #m; nnormalize;//;
+            ##]
+          ##]
+          nrewrite <H;
+          ncut (∃m:nat. S m = n);
+          ##[napply (lt_O_n_elim … posn); #m;@ m;//;
+            ##|*; #m; #Hm; nrewrite < Hm;
+               nrewrite > (delift ???????);nnormalize;/2/;
+          ##]
+nqed.
+  
+
+
+