From a6602de6db0993a67c5b23aedb3c8fe1d484855f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 30 May 2011 18:34:47 +0000
Subject: [PATCH] basics: some additions lambda: some additions + split of lift
 and subst

---
 matita/matita/lib/basics/list.ma            |  33 +++++
 matita/matita/lib/basics/logic.ma           |   4 +
 matita/matita/lib/lambda/degree.ma          |  38 +++++-
 matita/matita/lib/lambda/lambda_notation.ma |   4 +
 matita/matita/lib/lambda/lift.ma            | 134 ++++++++++++++++++++
 matita/matita/lib/lambda/subst.ma           |  98 +-------------
 6 files changed, 214 insertions(+), 97 deletions(-)
 create mode 100644 matita/matita/lib/lambda/lift.ma

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 798f57629..21dd7e3d1 100644
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -129,6 +129,10 @@ let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝
     [O ⇒ hd A l d
     |S m ⇒ nth m A (tail A l) d].
 
+lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
+#A #a #i elim i normalize //
+qed.
+
 (**************************** fold *******************************)
 
 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
@@ -183,3 +187,32 @@ theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
   [>nill //|#a #tl #Hind <assoc //]
 qed.
 
+(********************** lhd and ltl ******************************)
+
+let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
+   [ O   ⇒ nil …
+   | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
+   ].
+
+let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
+   [ O   ⇒ l
+   | S n ⇒ ltl A (tail … l) n
+   ].
+
+lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
+#A #n elim n //
+qed.
+
+lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
+#A #n elim n normalize //
+qed.
+
+lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
+#A #n elim n -n //
+#n #IHn #l elim l normalize //
+qed.
+
+lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
+#A #n elim n -n /2/
+#n #IHn * normalize /2/
+qed.
diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 32124c2fb..6723cf2cc 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -55,6 +55,10 @@ theorem eq_f2: ∀A,B,C.∀f:A→B→C.
 ∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2.
 #A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. 
 
+lemma eq_f3: ∀A,B,C,D.∀f:A→B→C->D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
 (* hint to genereric equality 
 definition eq_equality: equality ≝
  mk_equality eq refl rewrite_l rewrite_r.
diff --git a/matita/matita/lib/lambda/degree.ma b/matita/matita/lib/lambda/degree.ma
index bfe0fe3e9..1fa4ee7ec 100644
--- a/matita/matita/lib/lambda/degree.ma
+++ b/matita/matita/lib/lambda/degree.ma
@@ -119,6 +119,42 @@ interpretation "degree assignment (type context)" 'IInt1 G L = (Deg L G).
 
 interpretation "degree assignment (type context)" 'IInt G = (Deg (nil ?) G).
 
-lemma Deg_append: ∀L,G,H. ║H @ G║_[L] = ║H║_[║G║_[L]].
+lemma Deg_cons: ∀L,F,t. let H ≝ Deg L F in
+                ║t :: F║_[L] = ║t║_[H] - 1 :: H.
+// qed.
+
+lemma ltl_Deg: ∀L,G. ltl … (║G║_[L]) (|G|) = L.
+#L #G elim G normalize //
+qed.
+
+lemma Deg_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║_[║G║_[L]].
 #L #G #H elim H normalize //
 qed.
+
+interpretation "degree assignment (type context)" 'IIntS1 G L = (lhd ? (Deg L G) (length ? G)).
+
+lemma length_DegHd: ∀L,G. |║G║*_[L]| = |G|.
+#L #G elim G normalize //
+qed.
+
+lemma Deg_decomp: ∀L,G. ║G║*_[L] @ L = ║G║_[L].
+// qed.
+
+lemma append_Deg: ∀L,G,H. ║H @ G║_[L] = ║H║*_[║G║_[L]] @ ║G║_[L].
+// qed.
+
+lemma DegHd_Lift: ∀L,Lp,p. p = |Lp| → 
+                  ∀G. ║Lift G p║*_[Lp @ L] = ║G║*_[L].
+#L #Lp #p #HLp #G elim G //
+#t #G #IH normalize >IH <Deg_decomp /4/
+qed.
+
+lemma Deg_lift_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
+                      ∀t,k,Gk. k = |Gk| →
+                      ║lift t[k≝v] k 1 :: Lift Gk 1 @ [w] @ G║ =
+                      ║t :: Lift Gk 1 @ [w] @ G║.
+#v #w #G #Hvw #t #k #Gk #HGk
+>Deg_cons >Deg_cons in ⊢ (???%)
+>append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
+>deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
+qed.
diff --git a/matita/matita/lib/lambda/lambda_notation.ma b/matita/matita/lib/lambda/lambda_notation.ma
index e8ca08046..4f2f4f1dc 100644
--- a/matita/matita/lib/lambda/lambda_notation.ma
+++ b/matita/matita/lib/lambda/lambda_notation.ma
@@ -69,6 +69,10 @@ notation "hvbox(║T║ break _ [E1 break , E2])"
    non associative with precedence 50
    for @{'IInt2 $T $E1 $E2}.
 
+notation "hvbox(║T║ * break _ [E])"
+   non associative with precedence 50
+   for @{'IIntS1 $T $E}.
+
 notation "hvbox(〚T〛)"
    non associative with precedence 50
    for @{'EInt $T}.
diff --git a/matita/matita/lib/lambda/lift.ma b/matita/matita/lib/lambda/lift.ma
new file mode 100644
index 000000000..27d3d192e
--- /dev/null
+++ b/matita/matita/lib/lambda/lift.ma
@@ -0,0 +1,134 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "lambda/terms.ma".
+
+(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
+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). 
+
+(*** properties of lift ***)
+
+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_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i.
+#n #k #i #ltik change with 
+(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel i)
+>(le_to_leb_true … ltik) //
+qed.
+
+lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n).
+#n #k #i #leki change with 
+(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel (i+n))
+>lt_to_leb_false // @le_S_S // 
+qed.
+
+lemma lift_lift: ∀t.∀m,j.j ≤ m  → ∀n,k. 
+  lift (lift t k m) (j+k) n = lift t k (m+n).
+#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.
+
+lemma lift_lift_up: ∀n,m,t,k,i.
+  lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m.
+#n #m #N (elim N)
+  [1,3,4,5,6: normalize //
+  |#p #k #i @(leb_elim i p);
+    [#leip >lift_rel_ge // @(leb_elim (k+i) p);
+      [#lekip >lift_rel_ge; 
+        [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) //
+        |>associative_plus >commutative_plus @monotonic_le_plus_l // 
+        ]
+      |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki
+       >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //] 
+       >lift_rel_lt // >lift_rel_ge // 
+      ]
+    |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi 
+     >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
+     >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] 
+     >lift_rel_lt //
+    ]
+  ]
+qed.
+
+lemma lift_lift_up_sym: ∀n,m,t,k,i.
+  lift (lift t i m) (m+i+k) n = lift (lift t (i+k) n) i m.
+// qed.
+
+lemma lift_lift_up_01: ∀t,k,p. (lift (lift t k p) 0 1 = lift (lift t 0 1) (k+1) p).
+#t #k #p <(lift_lift_up_sym ? ? ? ? 0) //
+qed.
+
+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. *)
+
+(********************* context lifting ********************)
+
+let rec Lift G p ≝ match G with
+   [ nil      ⇒ nil …
+   | cons t F ⇒ cons … (lift t (|F|) p) (Lift F p)
+   ].
+
+interpretation "Lift (context)" 'Lift p G = (Lift G p).
+
+lemma Lift_cons: ∀k,Gk. k = |Gk| → 
+                 ∀p,t. Lift (t::Gk) p = lift t k p :: Lift Gk p.
+#k #Gk #H >H //
+qed.
+
+lemma Lift_length: ∀p,G. |Lift G p| = |G|.
+#p #G elim G -G; normalize //
+qed. 
diff --git a/matita/matita/lib/lambda/subst.ma b/matita/matita/lib/lambda/subst.ma
index ac0480224..4258f6a7c 100644
--- a/matita/matita/lib/lambda/subst.ma
+++ b/matita/matita/lib/lambda/subst.ma
@@ -9,27 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/terms.ma".
-
-(* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
-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 
@@ -50,81 +30,7 @@ notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
 (* interpretation "Subst" 'Subst N M = (subst N M). *)
 interpretation "Subst" 'Subst1 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_rel_lt : ∀n,k,i. i < k → lift (Rel i) k n = Rel i.
-#n #k #i #ltik change with 
-(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel i)
->(le_to_leb_true … ltik) //
-qed.
-
-lemma lift_rel_ge : ∀n,k,i. k ≤ i → lift (Rel i) k n = Rel (i+n).
-#n #k #i #leki change with 
-(if_then_else ? (leb (S i) k) (Rel i) (Rel (i+n)) = Rel (i+n))
->lt_to_leb_false // @le_S_S // 
-qed.
-
-lemma lift_lift: ∀t.∀m,j.j ≤ m  → ∀n,k. 
-  lift (lift t k m) (j+k) n = lift t k (m+n).
-#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.
-
-lemma lift_lift_up: ∀n,m,t,k,i.
-  lift (lift t i m) (m+k+i) n = lift (lift t (k+i) n) i m.
-#n #m #N (elim N)
-  [1,3,4,5,6: normalize //
-  |#p #k #i @(leb_elim i p);
-    [#leip >lift_rel_ge // @(leb_elim (k+i) p);
-      [#lekip >lift_rel_ge; 
-        [>lift_rel_ge // >lift_rel_ge // @(transitive_le … leip) //
-        |>associative_plus >commutative_plus @monotonic_le_plus_l // 
-        ]
-      |#lefalse (cut (p < k+i)) [@not_le_to_lt //] #ltpki
-       >lift_rel_lt; [|>associative_plus >commutative_plus @monotonic_lt_plus_r //] 
-       >lift_rel_lt // >lift_rel_ge // 
-      ]
-    |#lefalse (cut (p < i)) [@not_le_to_lt //] #ltpi 
-     >lift_rel_lt // >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //]
-     >lift_rel_lt; [|@(lt_to_le_to_lt … ltpi) //] 
-     >lift_rel_lt //
-    ]
-  ]
-qed.
-
-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
-- 
2.39.2