From d83fa3d6e3604bcc596840219f3998d795630d66 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 19 Jul 2011 20:39:43 +0000
Subject: [PATCH] first main property of drop closed

---
 matita/matita/lib/lambda-delta/ground.ma         | 16 ++++++++++++++++
 .../lib/lambda-delta/substitution/drop_defs.ma   | 13 +++++++++++++
 .../lib/lambda-delta/substitution/drop_main.ma   | 15 +++++++++++++--
 3 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index 23b028eb2..ac8147dfc 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -48,6 +48,22 @@ 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.
 
diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
index 3a827c3a0..79af8f90d 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
@@ -26,6 +26,19 @@ interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
 
 (* the basic inversion lemmas ***********************************************)
 
+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.
+#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)
+]
+qed.
+
+lemma drop_inv_drop1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e →
+                                   ↑[0, e - 1] L2 ≡ K.
+/2 width=5/ 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 dc6f00d40..67a1df4c1 100644
--- a/matita/matita/lib/lambda-delta/substitution/drop_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_main.ma
@@ -18,10 +18,21 @@ include "lambda-delta/substitution/drop_defs.ma".
 
 (* the main properties ******************************************************)
 
-axiom drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
+lemma drop_conf_ge: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
                     ∀e2,L2. ↑[0, e2] L2 ≡ L → d1 + e1 ≤ e2 →
                     ↑[0, e2 - e1] L2 ≡ L1.
-      
+#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
+[ //
+| #L #K #I #V #e #_ #IHLK #e2 #L2 #H #He2
+  lapply (drop_inv_drop1 … H ?) -H /2/ #HL2
+  <minus_plus_comm /3/
+| #L #K #I #V1 #V2 #d #e #_ #_ #IHLK #e2 #L2 #H #Hdee2
+  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/ ]
+]
+qed.
 
 axiom drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
                     ∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L →
-- 
2.39.2