From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 20 Jul 2011 20:11:07 +0000 (+0000)
Subject: two more main properties of drop closed
X-Git-Tag: make_still_working~2356
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d6cfac2387447f5682591e19cdbfeb82a15b851;p=helm.git

two more main properties of drop closed
---

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index ac8147dfc..b8c67bbcc 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -19,19 +19,33 @@ include "lambda-delta/notation.ma".
 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 // qed.
 
+lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
+// qed.
+
 lemma minus_le: ∀m,n. m - n ≤ m.
 /2/ qed.
 
 lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
 /2/ qed.
 
+lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
+/2/ qed.
+
+lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
+/2/ qed.
+
 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
 #n #m #p #lepm @plus_to_minus <associative_plus
 >(commutative_plus p) <plus_minus_m_m //
 qed.
 
-lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /3/
+lemma minus_le_minus_minus_comm: ∀m,p,n. 
+                                 p ≤ m → m - p ≤ n → n + p - m = n - (m - p).
+#m elim m -m
+[ #p #n #H >(le_O_to_eq_O … H) -H //
+| #m #IHm #p elim p -p //
+  #p #_ #n #Hpm <plus_n_Sm @IHm /2/
+]
 qed.
 
 lemma lt_refl_false: ∀n. n < n → False.
@@ -42,36 +56,29 @@ lemma lt_zero_false: ∀n. n < 0 → False.
 #n #H elim (lt_to_not_le … H) -H /2/
 qed.
 
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /3/
+qed.
+
 lemma plus_lt_false: ∀m,n. m + n < m → False.
 #m #n #H1 lapply (le_plus_n_r n m) #H2
 lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
 elim (lt_refl_false … H)
 qed.
 
-lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2/ qed.
-
 lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
 #n #m <plus_n_Sm #H destruct
 qed. 
 
-lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
-// qed.
-
 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
 /3/ qed.
 
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2/ qed.
-
 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
 /2/ qed.
 
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-/3/ qed.
-
-lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
-/3/ qed.
+lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
+#m #n #H >minus_plus <minus_minus //
+qed.
 
 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 /2/ qed.
@@ -79,9 +86,12 @@ lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
 /2/ qed.
 
-lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
-#m #n #H >minus_plus <minus_minus //
-qed.
-
 lemma arith7: ∀i,d. i ≤ d → d - i + i = d.
 /2/ qed.
+
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+/3/ qed.
+
+lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
+/3/ qed.
+
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
index 79af8f90d..623467dd5 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
@@ -24,21 +24,51 @@ inductive drop: lenv → nat → nat → lenv → Prop ≝
 
 interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
 
-(* the basic inversion lemmas ***********************************************)
+(* Basic properties *********************************************************) 
 
-lemma drop_inv_drop1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → 0 < e → d = 0 →
-                          ∀K,I,V. L1 = K. 𝕓{I} V → ↑[d, e - 1] L2 ≡ K.
+lemma drop_drop_lt: ∀L1,L2,I,V,e. 
+                    ↑[0, e - 1] L2 ≡ L1 → 0 < e → ↑[0, e] L2 ≡ L1. 𝕓{I} V.
+#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 → L1 = L2.
 #d #e #L2 #L1 #H elim H -H d e L2 L1
-[ #L #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #HL12 #_ #_ #_ #K #J #W #H destruct -L1 I V //
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #_ #H elim (plus_S_eq_O_false … H)
+[ //
+| #L1 #L2 #I #V #e #_ #_ #_ #H
+  elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H
+  elim (plus_S_eq_O_false … H)
 ]
 qed.
 
-lemma drop_inv_drop1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e →
-                                   ↑[0, e - 1] L2 ≡ K.
+lemma drop_inv_refl: ∀L2,L1. ↑[0, 0] L2 ≡ L1 → L1 = L2.
 /2 width=5/ qed.
 
+lemma drop_inv_O1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 →
+                       ∀K,I,V. L1 = K. 𝕓{I} V → 
+                       (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+                       (0 < e ∧ ↑[d, e - 1] L2 ≡ K).
+#d #e #L2 #L1 #H elim H -H d e L2 L1
+[ /3/
+| #L1 #L2 #I #V #e #HL12 #_ #_ #K #J #W #H destruct -L1 I V /3/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H elim (plus_S_eq_O_false … H)
+]
+qed.
+
+lemma drop_inv_O1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V →
+                   (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+                   (0 < e ∧ ↑[0, e - 1] L2 ≡ K).
+/2/ qed.
+
+lemma drop_inv_drop1: ∀e,L2,K,I,V.
+                      ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e → ↑[0, e - 1] L2 ≡ K.
+#e #L2 #K #I #V #H #He
+elim (drop_inv_O1 … H) -H * // #H destruct -e;
+elim (lt_refl_false … He)
+qed.
+
 lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
                           ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
                           ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 &
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_main.ma b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
index 67a1df4c1..72d980e9b 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
@@ -30,19 +30,48 @@ lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
   lapply (transitive_le 1 … Hdee2) // #He2
   lapply (drop_inv_drop1 … H ?) -H // -He2 #HL2
   lapply (transitive_le (1+e) … Hdee2) // #Hee2
-  >(plus_minus_m_m (e2-e) 1 ?) [ @drop_drop >minus_minus_comm /3/ | /2/ ]
+  @drop_drop_lt >minus_minus_comm /3/ (**) (* explicit constructor *)
 ]
 qed.
 
-axiom drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
+lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
                     ∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L →
                     e2 < d1 → let d ≝ d1 - e2 - 1 in
                     ∃∃K1,V1. ↑[0, e2] K1. 𝕓{I} V1 ≡ L1 & 
                              ↑[d, e1] K1 ≡ K2 & ↑[d,e1] V1 ≡ V2.
+#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
+[ #L0 #e2 #K2 #I #V2 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #V #e #_ #_ #e2 #K2 #J #V2 #_ #H
+  elim (lt_zero_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d
+  elim (drop_inv_O1 … H) -H *
+  [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/
+  | -HL12 -HV12 #He #HLK
+    elim (IHL12 … HLK ?) -IHL12 HLK [ <minus_minus /3 width=5/ | /2/ ] (**) (* a bit slow *)
+  ]
+]
+qed.
 
-axiom drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
+lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
                      ∀e2,L2. ↑[0, e2] L2 ≡ L → e2 ≤ d1 →
                      ∃∃L0. ↑[0, e2] L0 ≡ L1 & ↑[d1 - e2, e1] L2 ≡ L0.
+#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
+[ #L #e2 #L2 #HL2 #H
+  lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/
+| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
+  lapply (le_O_to_eq_O … H) -H #H destruct -e2;
+  elim (IHL12 … HL2 ?) -IHL12 HL2 // #L0 #H #HL0
+  lapply (drop_inv_refl … H) -H #H destruct -L1 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+  elim (drop_inv_O1 … H) -H *
+  [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/
+  | -HL12 HV12 #He2 #HL2
+    elim (IHL12 … HL2 ?) -IHL12 HL2 L2
+    [ <minus_le_minus_minus_comm /3/ | /2/ ]
+  ]
+]
+qed.
 
 axiom drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 →
                      ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 ≤ e2 → ↑[0, e1 + e2] L2 ≡ L1.