- slicing relation for the global environment defined (gdrop)

- two arithmetical lemmas inlined

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
index 1f750064ebd139eb0c9d472ef31dbda24c79e99e..6f3ec15131aa6e1440c25da186e5382c6f951428 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
@@ -74,8 +74,7 @@ fact lsubs_fwd_length_full1_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
 | /2 width=1/
 | /3 width=1/
 | /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H
-  elim (plus_S_eq_O_false … H)
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 
@@ -89,8 +88,7 @@ fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
 | /2 width=1/
 | /3 width=1/
 | /3 width=1/
-| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ #H
-  elim (plus_S_eq_O_false … H)
+| #L1 #L2 #_ #_ #_ #_ #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index 0ec1b1466a44e4b16b9f95094d20211773a73650..8e1d4362afddadfc86d1df58337c5d8bf2bfeee9 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -86,6 +86,10 @@ notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
    non associative with precedence 45
    for @{ 'RLift $d $e $T1 $T2 }.
 
+notation "hvbox( ↓ [ e ] break L1 ≡ break L2 )"
+   non associative with precedence 45
+   for @{ 'RDrop $e $L1 $L2 }.
+
 notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
    non associative with precedence 45
    for @{ 'RDrop $d $e $L1 $L2 }.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
new file mode 100644 (file)
index 0000000..47d75a4
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic_2/substitution/ldrop.ma".
+
+(* GLOBAL ENVIRONMENT SLICING ***********************************************)
+
+inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝
+| gdrop_lt: ∀G2. e < |G1| → ↓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2
+| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆)
+.
+
+interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2).
+
+(* basic inversion lemmas ***************************************************)
+
+fact gdrop_inv_atom2_aux: ∀G1,G2,e. ↓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e.
+#G1 #G2 #e * -G2 //
+#G2 #He #HG12 #H destruct
+lapply (ldrop_fwd_O1_length … HG12) -HG12
+>minus_le_minus_minus_comm // -He >le_plus_minus_comm // <minus_n_n
+>(commutative_plus e) normalize #H destruct
+qed.
+
+lemma gdrop_inv_atom2: ∀G1,e. ↓[e] G1 ≡ ⋆ → |G1| ≤ e.
+/2 width=3/ qed-.
+
+lemma gdrop_inv_ge: ∀G1,G2,e. ↓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
+#G1 #G2 #e * // #G2 #H1 #_ #H2
+lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He
+elim (lt_refl_false … He)
+qed-.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index 9d085fc0566f9d508f2d9a5214dea9be09bf6514..b4d3355d6bd4c38d249a9f9246b08343f37d18fe 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -28,7 +28,7 @@ inductive ldrop: nat → nat → relation lenv ≝
               ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
 .
 
-interpretation "ldropping" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
+interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -36,10 +36,8 @@ fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ //
 | //
-| #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)
+| #L1 #L2 #I #V #e #_ #_ >commutative_plus normalize #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 
@@ -69,7 +67,7 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
 [ #d #e #_ #K #I #V #H destruct
 | #L #I #V #_ #K #J #W #HX destruct /3 width=1/
 | #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
index 30296c685d2a9751b7b5971ee17aa58bbbc1cbfc..fa1dfae280dec03d5f8fc66d5a6c43e3d88af8b6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
@@ -164,7 +164,8 @@ lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
 lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i.
 #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
 #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
-elim (plus_lt_false … Hdd)
+elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
+elim (lt_refl_false … Hdd)
 qed-.
 
 (* Basic_1: was: lift_gen_lref_false *)
@@ -180,7 +181,8 @@ qed-.
 lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e).
 #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
 #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
-elim (plus_lt_false … Hdd)
+elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
+elim (lt_refl_false … Hdd)
 qed-.
 
 fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p.

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
index ccb460654269bc592b5a900514aa248b257f4620..c804efa415469e9a2ab30fa58c02f26af4d61caa 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
@@ -57,8 +57,7 @@ qed.
 
 fact ltps_inv_refl_O2_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → e = 0 → L1 = L2.
 #d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
-[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ #H
-  elim (plus_S_eq_O_false … H)
+[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
 | #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
   >(IHL12 ?) -IHL12 // >(tps_inv_refl_O2 … HV12) //
 ]
@@ -89,7 +88,7 @@ fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 
@@ -139,7 +138,7 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
 | #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
index 80e23e6956a2ea78bccda3a080348a853774207b..37fac204b70452b7cb98881b30f63b303a844633 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
@@ -29,20 +29,14 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
 /2 by plus_minus/ qed.
 
 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
- /3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
+/3 by monotonic_le_minus_l, le_to_le_to_eq/ qed.
 
 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
-#b elim b -b
-[ #c #a #H >(le_n_O_to_eq … H) -H //
-| #b #IHb #c elim c -c //
-  #c #_ #a #Hcb
-  lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
-  <plus_n_Sm normalize /2 width=1/
-]
+#b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
 qed.
 
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus /3 width=1/
+#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
 qed.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
@@ -68,11 +62,9 @@ lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
 qed-.
 
 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
-#m elim m -m
-[ * /2 width=1/
-| #m #IHm * /2 width=1/
-  #n elim (IHm n) -IHm #H 
-  [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
+#m #n elim (lt_or_ge m n) /2 width=1/
+#H elim H -m /2 width=1/
+#m #Hm * #H /2 width=1/ /3 width=1/
 qed-.
 
 lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
@@ -81,6 +73,9 @@ lemma le_inv_plus_plus_r: ∀x,y,z. x + z ≤ y + z → x ≤ y.
 lemma le_inv_plus_l: ∀x,y,z. x + y ≤ z → x ≤ z - y ∧ y ≤ z.
 /3 width=2/ qed-.
 
+lemma lt_inv_plus_l: ∀x,y,z. x + y < z → x < z ∧ y < z - x.
+/3 width=2/ qed-.
+
 lemma lt_refl_false: ∀n. n < n → False.
 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
 qed-.
@@ -89,24 +84,18 @@ lemma lt_zero_false: ∀n. n < 0 → False.
 #n #H elim (lt_to_not_le … H) -H /2 width=1/
 qed-.
 
-lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
-#n #m <plus_n_Sm #H destruct
-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 false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
 #x #y #H elim (decidable_lt x y) /2 width=1/
 #Hxy elim (H Hxy)
 qed-.
 
 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-#m1 #m2 #H elim H -m1
-[ /2 width=2/
-| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=3/
-]
-qed-.
+#m1 #m2 #H #n1 #n2 >commutative_plus
+#H elim (le_inv_plus_l … H) -H >commutative_plus <minus_le_minus_minus_comm //
+#H #_ @(transitive_le … H) /2 width=1/
+qed-. 
+
+(*
+lemma pippo: ∀x,y,z. x < z → y < z - x → x + y < z.
+/3 width=2/
+*)