X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Fsubst.ma;h=4f61ef5282fdcf6da367948d7c264526e7ebf87f;hb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;hp=85bef55e155fa0e4a01a83de2fcaeff28d56fc47;hpb=6bbf27282bad84e066bb952e41dbc8f72b31de6c;p=helm.git

diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index 85bef55e1..4f61ef528 100644
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -9,35 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/nat.ma".
-
-inductive T : Type[0] ≝
-  | Sort: nat → T
-  | Rel: nat → T 
-  | App: T → T → T 
-  | Lambda: T → T → T (* type, body *)
-  | Prod: T → T → T (* type, body *)
-  | D: T →T
-.
-
-let 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 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)
-    | D n ⇒ D (lift n k p)
-    ].
-
-(* 
-ndefinition lift ≝ λt.λp.lift_aux t 0 p.
-
-notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift O $M}.
-notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
-*)
-(* interpretation "Lift" 'Lift n M = (lift M n). *)
-interpretation "Lift" 'Lift n k M = (lift M k n).
+include "lambda/lift.ma".
 
 let rec subst t k a ≝ 
   match t with 
@@ -55,52 +27,10 @@ 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 $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 ***)
-
-lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
-#t (elim t) normalize // #n #k cases (leb (S n) k) normalize // 
-qed.
-
-(* nlemma lift_0: ∀t:T. lift t 0 = t.
-#t; nelim t; nnormalize; //; nqed. *)
-
-lemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
-// qed.
-
-lemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
-// qed.
-
-lemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
-#i (change with (lift (Rel i) 0 1 = Rel (1 + i))) //
-qed.
-
-lemma 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 (elim t) normalize // #n #h #k
-@(leb_elim (S n) k) #Hnk normalize
-  [>(le_to_leb_true (S n) (j+k) ?) normalize /2/
-  |>(lt_to_leb_false (S n+i) (j+k) ?)
-     normalize // @le_S_S >(commutative_plus j k)
-     @le_plus // @not_lt_to_le /2/
-  ]
-qed.
+interpretation "Subst" 'Subst1 M k N = (subst M k N).
 
-lemma lift_lift1: ∀t.∀i,j,k. 
-  lift(lift t k j) k i = lift t k (j+i).
-/2/ qed.
-
-lemma lift_lift2: ∀t.∀i,j,k. 
-  lift (lift t k j) (j+k) i = lift t k (j+i).
-/2/ qed.
-
-(*
-nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
-nnormalize; //; nqed. *)
+(*** properties of subst ***)
 
 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
 #A #B (elim B) normalize /2/ #n #k
@@ -167,6 +97,54 @@ lemma lift_subst_ijk: ∀A,B.∀i,j,k.
   ]
 qed. 
 
+lemma lift_subst_up: ∀M,N,n,i,j.
+  lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)].
+#M (elim M) 
+  [//
+  |#p #N #n #i #j (cases (true_or_false (leb p i)))
+    [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi)))
+      [#ltpi >(subst_rel1 … ltpi) 
+       (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij
+       >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?); 
+        [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //]
+      |#eqpi >eqpi >subst_rel2 >lift_rel_lt;
+        [>subst_rel2 >(plus_n_O (i+j)) 
+         applyS lift_lift_up 
+        |@(le_to_lt_to_lt ? (i+j)) //
+        ]
+      ]
+    |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip
+     (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp
+     >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1))))
+      [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt
+       >lift_rel_lt; 
+        [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //]
+      |#Hfalse >lift_rel_ge; 
+        [>lift_rel_ge; 
+          [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //]
+          |@not_lt_to_le @(leb_false_to_not_le … Hfalse)
+          ]
+        |@le_plus_to_minus_r @not_lt_to_le 
+         @(leb_false_to_not_le … Hfalse)
+        ]
+      ]
+    ]
+  |#P #Q #HindP #HindQ #N #n #i #j normalize 
+   @eq_f2; [@HindP |@HindQ ]
+  |#P #Q #HindP #HindQ #N #n #i #j normalize 
+   @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+   <associative_plus @HindQ]
+  |#P #Q #HindP #HindQ #N #n #i #j normalize 
+   @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
+   <associative_plus @HindQ]
+  |#P #HindP #N #n #i #j normalize 
+   @eq_f @HindP
+  ]
+qed.
+
+lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
+// qed.
+
 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
   (lift B i (S k)) [j ≝ A] = lift B i k.
 #A #B (elim B) normalize /2/
@@ -228,7 +206,7 @@ lemma subst_lemma: ∀A,B,C.∀k,i.
   ] 
 qed.
 
-  
-
-
-
+lemma subst_lemma_comm: ∀A,B,C.∀k,i.
+  (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
+#A #B #C #k #i >commutative_plus >subst_lemma //
+qed.