From 331cbed42a29b3b9f5fb11d127534f3c62c86797 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 18 Jun 2011 14:29:50 +0000
Subject: [PATCH] - xoa: more existential types - ground: more arithmetics -
 lift: more nasic inversion lemmas and some renaming

---
 matita/matita/lib/lambda-delta/ground.ma      | 10 +++
 .../lambda-delta/substitution/lift_defs.ma    | 61 ++++++++++++++-----
 .../lambda-delta/substitution/lift_main.ma    | 44 ++++++-------
 matita/matita/lib/lambda-delta/xoa_defs.ma    | 10 ++-
 .../matita/lib/lambda-delta/xoa_notation.ma   |  4 ++
 5 files changed, 85 insertions(+), 44 deletions(-)

diff --git a/matita/matita/lib/lambda-delta/ground.ma b/matita/matita/lib/lambda-delta/ground.ma
index f4279588b..87d8d9baf 100644
--- a/matita/matita/lib/lambda-delta/ground.ma
+++ b/matita/matita/lib/lambda-delta/ground.ma
@@ -30,10 +30,20 @@ lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
 >(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/
+qed.
+
 lemma lt_false: ∀n. n < n → False.
 #n #H lapply (lt_to_not_eq … H) -H #H elim H -H /2/
 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_false … H)
+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/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
index 86e1b7511..1f9be7fe2 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
@@ -29,12 +29,27 @@ interpretation "relocation" 'RLift T1 d e T2 = (lift T1 d e T2).
 
 (* The basic properties *****************************************************)
 
-lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d,e] #(i - e) ≡ #i.
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i.
 #d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
 qed.
 
+lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T.
+#T elim T -T
+[ //
+| #i #d elim (lt_or_ge i d) /2/
+| #I elim I -I /2/
+]
+qed.
+
 (* The basic inversion lemmas ***********************************************)
 
+lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
+#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/
+qed.
+
+lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
+/2/ qed.
+
 lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
 #d #e #T1 #T2 #H elim H -H d e T1 T2 //
 [ #i #d #e #_ #k #H destruct
@@ -44,8 +59,7 @@ lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k 
 qed.
 
 lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
-#d #e #T2 #k #H lapply (lift_inv_sort1_aux … H) /2/
-qed.
+/2 width=5/ qed.
 
 lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
                           (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
@@ -60,7 +74,18 @@ qed.
 
 lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
                       (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
-#d #e #T2 #i #H lapply (lift_inv_lref1_aux … H) /2/
+/2/ qed.
+
+lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i.
+#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
+#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
+elim (lt_false … Hdd)
+qed.
+
+lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e).
+#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
+#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
+elim (lt_false … Hdd)
 qed.
 
 lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
@@ -79,8 +104,7 @@ qed.
 lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕓{I} V1. U1 ≡ T2 →
                       ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
                                T2 = 𝕓{I} V2. U2.
-#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_bind1_aux … H) /2/
-qed.
+/2/ qed.
 
 lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
@@ -98,8 +122,7 @@ qed.
 lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ↑[d,e] 𝕗{I} V1. U1 ≡ T2 →
                       ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
                                T2 = 𝕗{I} V2. U2.
-#d #e #T2 #I #V1 #U1 #H lapply (lift_inv_flat1_aux … H) /2/
-qed.
+/2/ qed.
 
 lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
 #d #e #T1 #T2 #H elim H -H d e T1 T2 //
@@ -110,8 +133,7 @@ lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k 
 qed.
 
 lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
-#d #e #T1 #k #H lapply (lift_inv_sort2_aux … H) /2/
-qed.
+/2 width=5/ qed.
 
 lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
                           (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
@@ -126,7 +148,18 @@ qed.
 
 lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
                       (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-#d #e #T1 #i #H lapply (lift_inv_lref2_aux … H) /2/
+/2/ qed.
+
+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)
+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)
 qed.
 
 lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
@@ -145,8 +178,7 @@ qed.
 lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕓{I} V2. U2 →
                       ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
                                T1 = 𝕓{I} V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_bind2_aux … H) /2/
-qed.
+/2/ qed.
 
 lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
                           ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
@@ -164,5 +196,4 @@ qed.
 lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ↑[d,e] T1 ≡  𝕗{I} V2. U2 →
                       ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
                                T1 = 𝕗{I} V1. U1.
-#d #e #T1 #I #V2 #U2 #H lapply (lift_inv_flat2_aux … H) /2/
-qed.
+/2/ qed.
diff --git a/matita/matita/lib/lambda-delta/substitution/lift_main.ma b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
index 2f588c1a6..ba74cf7b2 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_main.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_main.ma
@@ -18,21 +18,18 @@ include "lambda-delta/substitution/lift_defs.ma".
 
 (* the main properies *******************************************************)
 
-theorem lift_conf_rev: ∀d1,e1,T1,T. ↑[d1,e1] T1 ≡ T →
-                       ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
-                       d1 ≤ d2 →
-                       ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
+theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                     ∀d2,e2,T2. ↑[d2 + e1, e2] T2 ≡ T →
+                     d1 ≤ d2 →
+                     ∃∃T0. ↑[d1, e1] T0 ≡ T2 & ↑[d2, e2] T0 ≡ T1.
 #d1 #e1 #T1 #T #H elim H -H d1 e1 T1 T
 [ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
   lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct -T2 /3/
 | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
-  [ -Hid2 /4/
-  | elim (lt_false d1 ?)
-    @(le_to_lt_to_lt … Hd12) -Hd12 @(le_to_lt_to_lt … Hid1) -Hid1 /2/
-  ]
+  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+  lapply (lift_inv_lref2_lt … Hi ?) -Hi /3/
 | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
-  lapply (lift_inv_lref2 … Hi) -Hi * * #Hid2 #H destruct -T2
+  elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct -T2
   [ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
   | -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
     @(ex2_1_intro … #(i - e2))
@@ -70,33 +67,26 @@ theorem lift_free: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
 ]
 qed.
 
-theorem lift_trans: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
-                    ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
-                    d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
+theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
+                       ∀d2,e2,T2. ↑[d2, e2] T ≡ T2 →
+                       d1 ≤ d2 → d2 ≤ d1 + e1 → ↑[d1, e1 + e2] T1 ≡ T2.
 #d1 #e1 #T1 #T #H elim H -d1 e1 T1 T
 [ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
   >(lift_inv_sort1 … HT2) -HT2 //
 | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #Hd12 #_
-  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
-  [ -Hd12 Hid2 /2/
-  | lapply (le_to_lt_to_lt … d1 Hid2 ?) // -Hid1 Hid2 #Hd21
-    lapply (le_to_lt_to_lt … d1 Hd12 ?) // -Hd12 Hd21 #Hd11
-    elim (lt_false … Hd11)
-  ]
+  lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+  lapply (lift_inv_lref1_lt … HT2 Hid2) /2/
 | #i #d1 #e1 #Hid1 #d2 #e2 #T2 #HT2 #_ #Hd21
-  lapply (lift_inv_lref1 … HT2) -HT2 * * #Hid2 #H destruct -T2
-  [ lapply (lt_to_le_to_lt … (d1+e1) Hid2 ?) // -Hid2 Hd21 #H
-    lapply (lt_plus_to_lt_l … H) -H #H
-    lapply (le_to_lt_to_lt … d1 Hid1 ?) // -Hid1 H #Hd11
-    elim (lt_false … Hd11)
-  | -Hd21 Hid2 /2/
+  lapply (lift_inv_lref1_ge … HT2 ?) -HT2
+  [ @(transitive_le … Hd21 ?) -Hd21 /2/
+  | -Hd21 /2/
   ]
 | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  lapply (lift_inv_bind1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
   lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
   lapply (IHT12 … HT20 ? ?) /2/
 | #I #V1 #V2 #T1 #T2 #d1 #e1 #_ #_ #IHV12 #IHT12 #d2 #e2 #X #HX #Hd12 #Hd21
-  lapply (lift_inv_flat1 … HX) -HX * #V0 #T0 #HV20 #HT20 #HX destruct -X;
+  elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct -X;
   lapply (IHV12 … HV20 ? ?) // -IHV12 HV20 #HV10
   lapply (IHT12 … HT20 ? ?) /2/
 ]
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index e36373e3c..022c06607 100644
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -17,13 +17,19 @@
 include "basics/pts.ma".
 
 inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
-   | ex2_1_intro: ∀x0. (P0 x0)→(P1 x0)→(ex2_1 ? ? ?)
+   | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ?
 .
 
 interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
 
+inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
+   | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+
 inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
-   | ex3_2_intro: ∀x0,x1. (P0 x0 x1)→(P1 x0 x1)→(P2 x0 x1)→(ex3_2 ? ? ? ? ?)
+   | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2).
diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index 1af6c7fab..c16d28585 100644
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -18,6 +18,10 @@ notation "hvbox(∃∃ ident x0 . term 19 P0 & term 19 P1)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) }.
 
+notation "hvbox(∃∃ ident x0 , ident x1 . term 19 P0 & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) }.
+
 notation "hvbox(∃∃ ident x0 , ident x1 . term 19 P0 & term 19 P1 & term 19 P2)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) (λ${ident x0},${ident x1}.$P2) }.
-- 
2.39.2