From 8a5391064ec6e84333444453f836ef9cb91fee7b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 26 Nov 2012 20:27:40 +0000
Subject: [PATCH] we started the theory of delifting substitution ...

---
 matita/matita/contribs/lambda/dsubst.ma | 85 +++++++++++++++++++++++++
 matita/matita/lib/arithmetics/nat.ma    | 15 +++--
 matita/matita/predefined_virtuals.ml    |  2 +-
 3 files changed, 96 insertions(+), 6 deletions(-)
 create mode 100644 matita/matita/contribs/lambda/dsubst.ma

diff --git a/matita/matita/contribs/lambda/dsubst.ma b/matita/matita/contribs/lambda/dsubst.ma
new file mode 100644
index 000000000..4d686ef37
--- /dev/null
+++ b/matita/matita/contribs/lambda/dsubst.ma
@@ -0,0 +1,85 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lift.ma".
+
+(* DELIFTING SUBSTITUTION ***************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec dsubst C d M on M ≝ match M with
+[ VRef i   ⇒ tri … i d (#i) (↑[i] C) (#(i-1))
+| Abst A   ⇒ 𝛌. (dsubst C (d+1) A)
+| Appl B A ⇒ @ (dsubst C d B). (dsubst C d A)
+].
+
+interpretation "delifting substitution"
+   'DSubst C d M = (dsubst C d M).
+
+(* Note: the notation with "/" does not work *)
+notation "hvbox( [ d ⬐ break C ] break term 55 M )"
+   non associative with precedence 55
+   for @{ 'DSubst $C $d $M }.
+
+notation > "hvbox( [ ⬐ C ] break term 55 M )"
+   non associative with precedence 55
+   for @{ 'DSubst $C 0 $M }.
+
+lemma dsubst_vref_lt: ∀i,d,C. i < d → [ d ⬐ C ] #i = #i.
+normalize /2 width=1/
+qed.
+
+lemma dsubst_vref_eq: ∀d,C. [ d ⬐ C ] #d = ↑[d]C.
+normalize //
+qed.
+
+lemma dsubst_vref_gt: ∀i,d,C. d < i → [ d ⬐ C ] #i = #(i-1).
+normalize /2 width=1/
+qed.
+
+theorem dsubst_lift_le: ∀h,C,M,d1,d2. d2 ≤ d1 →
+                        [ d2 ⬐ ↑[d1 - d2, h] C ] ↑[d1 + 1, h] M = ↑[d1, h] [ d2 ⬐ C ] M.
+#h #C #M elim M -M
+[ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
+  [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+    >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
+  | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
+  | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+    [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
+    | lapply (ltn_to_ltO … Hid2) #Hi
+      >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+    ]
+  ]
+| normalize #A #IHA #d1 #d2 #Hd21
+  lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd21
+  >IHB -IHB // >IHA -IHA //
+]
+qed.
+ 
+theorem dsubst_lift_be: ∀h,C,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+                        [ d2 ⬐ C ] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #C #M elim M -M
+[ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+  [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+    >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
+  | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+    >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
+    >dsubst_vref_gt // /2 width=1/
+  ]
+| normalize #A #IHA #d1 #d2 #Hd12 #Hd21
+  >IHA -IHA // /2 width=1/
+| normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
+  >IHB -IHB // >IHA -IHA //
+]
+qed.
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 06266a4b0..edb99b8c0 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -645,6 +645,14 @@ theorem monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 @lt_plus_to_minus_r <plus_minus_m_m //
 qed.
 
+(* More compound conclusion *************************************************)
+
+lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
+* /2 width=1/ #x * /2 width=1/ #y normalize #H 
+lapply (minus_le x y) <H -H #H
+elim (not_le_Sn_n x) #H0 elim (H0 ?) //
+qed-.
+
 (* Still more equalities ****************************************************)
 
 theorem eq_minus_O: ∀n,m:nat.
@@ -688,11 +696,8 @@ qed.
 lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
 /2 width=1/ qed.
 
-lemma discr_minus_x_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
-* /2 width=1/ #x * /2 width=1/ #y normalize #H 
-lapply (minus_le x y) <H -H #H
-elim (not_le_Sn_n x) #H0 elim (H0 ?) //
-qed-.
+lemma minus_plus_plus_l: ∀x,y,h. (x + h) - (y + h) = x - y.
+// qed.
 
 (* Stilll more atomic conclusion ********************************************)
 
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index e351b7250..0dbc5b75e 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1515,7 +1515,7 @@ let predefined_classes = [
  ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ;
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; ];
- ["_" ; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "⬐"; "⎽"; "⎼"; "⎻"; "⎺"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];
-- 
2.39.2