definition of equivalence for local environments,

based on natural numbers with infinity

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
new file mode 100644 (file)
index 0000000..32924d1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground_2/ynat/ynat_succ.ma".
+include "basic_2/notation/relations/iso_4.ma".
+include "basic_2/grammar/lenv_length.ma".
+
+(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************)
+
+inductive leq: ynat → ynat → relation lenv ≝
+| leq_atom: ∀d,e. leq d e (⋆) (⋆)
+| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| leq_pair: ∀I1,I2,L1,L2,V1,V2,e.
+            leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2)
+| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+.
+
+interpretation
+   "equivalence (local environment)"
+   'Iso d e L1 L2 = (leq d e L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma leq_refl: ∀L,d,e. L ≃[d, e] L.
+#L elim L -L /2 width=1 by/
+#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ]
+elim (ynat_cases … e) [ | * ]
+/2 width=1 by leq_zero, leq_pair/
+qed.
+
+lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize //
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
+#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H)
+qed-.
+
+lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2.
+/2 width=4 by leq_inv_O2_aux/ qed-.
+
+fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/
+[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct
+| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H
+  /3 width=1 by eq_f3/
+]
+qed-.
+
+lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2.
+/2 width=4 by leq_inv_Y1_aux/ qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
index eb8f210dc30f069db0a6c96dbebbe3c0f708aa09..6001f40fa962427299acecb860891db8a0e5ff55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma
@@ -39,7 +39,7 @@ fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. 
                            ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
 #R #L1 #L2 * -L1 -L2
 [ #J #K1 #V1 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
@@ -61,7 +61,7 @@ fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. 
                            ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
 #R #L1 #L2 * -L1 -L2
 [ #J #K2 #V2 #H destruct
-| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/
 ]
 qed-.
 
@@ -69,6 +69,13 @@ lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
                         ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
 /2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
 
+lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2.
+                       lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) →
+                       ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2.
+#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H
+#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
@@ -104,11 +111,11 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
-#R #HR #L elim L -L // /2 width=1/
+#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/
 qed-.
 
 lemma lpx_sn_append: ∀R. l_appendable_sn R →
                      ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
                      lpx_sn R (L1 @@ K1) (L2 @@ K2).
-#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+#R #HR #K1 #K2 #H elim H -K1 -K2 /3 width=1 by lpx_sn_pair/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
index 5b62fa9405e497856ec2bb5f429080d7be44b016..77725446a9ebf79e1aedd380433dd4f315bc702d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
@@ -97,12 +97,15 @@ axiom eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
 
 (* Basic inversion lemmas ***************************************************)
 
+lemma destruct_tpair_tpair: ∀I1,I2,T1,T2,V1,V2. ②{I1}T1.V1 = ②{I2}T2.V2 →
+                            ∧∧T1 = T2 & I1 = I2 & V1 = V2.
+#I1 #I2 #T1 #T2 #V1 #V2 #H destruct /2 width=1 by and3_intro/
+qed-.
+
 lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → ⊥.
 #I #T #V elim V -V
 [ #J #H destruct
-| #J #W #U #IHW #_ #H destruct
-  -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
-  /2 width=1/
+| #J #W #U #IHW #_ #H elim (destruct_tpair_tpair … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
 ]
 qed-.
 
@@ -110,9 +113,7 @@ qed-.
 lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → ⊥.
 #I #V #T elim T -T
 [ #J #H destruct
-| #J #W #U #_ #IHU #H destruct
-  -H (**) (* destruct: the destucted equality is not erased *)
-  /2 width=1/
+| #J #W #U #_ #IHU #H elim (destruct_tpair_tpair … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
 ]
 qed-.
 
@@ -120,16 +121,16 @@ lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
                              (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
                              (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
 #I #V1 #T1 #V2 #T2 #H
-elim (eq_term_dec V1 V2) /3 width=1/ #HV12 destruct
-@or_intror @conj // #HT12 destruct /2 width=1/
+elim (eq_term_dec V1 V2) /3 width=1 by or_introl/ #HV12 destruct
+@or_intror @conj // #HT12 destruct /2 width=1 by/
 qed-.
 
 lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
                              (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
                              (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
 #I #V1 #T1 #V2 #T2 #H
-elim (eq_term_dec T1 T2) /3 width=1/ #HT12 destruct
-@or_intror @conj // #HT12 destruct /2 width=1/
+elim (eq_term_dec T1 T2) /3 width=1 by or_introl/ #HT12 destruct
+@or_intror @conj // #HT12 destruct /2 width=1 by/
 qed-.
 
 (* Basic_1: removed theorems 3:

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma
new file mode 100644 (file)
index 0000000..8a3617c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )"
+   non associative with precedence 45
+   for @{ 'Iso $d $e $L1 $L2 }.

diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
index 3eec66de3398534d92270caef92376e2f959f784..8bc1e8538b38992b56fa42f75b8bcde81b53181d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl
@@ -4,17 +4,22 @@ table {
    class "grey"
    [ { "plane" * } {
         [ "files" * ]
-     }     
+     }
    ]
-   class "orange"
+   class "yellow"
    [ { "natural numbers with infinity" * } {
         [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" "ynat_le ( ?≤? )" "ynat_lt ( ?<? )" * ]
-     }     
+     }
+   ]
+   class "orange"
+   [ { "extensions to the library" * } {
+        [ "arith.ma ( ?^? )" * ]
+     }
    ]
    class "red"
-   [ { "" * } {
-        [ "" * ]
-     }     
+   [ { "generated logical decomposables" * } {
+        [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ]
+     }
    ]
 }
 

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
index 707556f301211c4015cb0c7faee3adcfa00569cc..c244b9caed637c9567846f7515f054511f3a57f4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_succ.ma
@@ -30,6 +30,14 @@ interpretation "ynat successor" 'Successor m = (ysucc m).
 lemma ypred_succ: ∀m. ⫰⫯m = m.
 * // qed.
 
+lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m. n = ⫯m.
+*
+[ * /2 width=1 by or_introl/
+  #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *)
+| @or_intror @(ex_intro … (∞)) // (**) (* explicit constructor *)
+]
+qed-.
+
 (* Inversion lemmas *********************************************************)
 
 lemma ysucc_inj: ∀m,n. ⫯m = ⫯n → m = n.
@@ -61,3 +69,11 @@ qed-.
 
 lemma ysucc_inv_Y_dx: ∀m. ⫯m = ∞ → m = ∞.
 /2 width=1 by ysucc_inv_Y_sn/ qed-.
+
+lemma ysucc_inv_O_sn: ∀m. yinj 0 = ⫯m → ⊥. (**) (* explicit coercion *)
+#m #H elim (ysucc_inv_inj_sn … H) -H
+#n #_ #H destruct
+qed-.
+
+lemma ysucc_inv_O_dx: ∀m. ⫯m = 0 → ⊥.
+/2 width=2 by ysucc_inv_O_sn/ qed-.