From ab0d181f9a89f461a9c280f42a949a2dc2abe44c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 28 Nov 2013 16:02:03 +0000 Subject: [PATCH] definition of equivalence for local environments, based on natural numbers with infinity --- .../lambdadelta/basic_2/grammar/leq.ma | 72 +++++++++++++++++++ .../lambdadelta/basic_2/grammar/lpx_sn.ma | 15 ++-- .../lambdadelta/basic_2/grammar/term.ma | 21 +++--- .../basic_2/notation/relations/iso_4.ma | 19 +++++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 17 +++-- .../lambdadelta/ground_2/ynat/ynat_succ.ma | 16 +++++ 6 files changed, 140 insertions(+), 20 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma 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 index 000000000..32924d1c2 --- /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 eb8f210dc..6001f40fa 100644 --- 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 5b62fa940..77725446a 100644 --- 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 index 000000000..8a3617c1b --- /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 3eec66de3..8bc1e8538 100644 --- 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 707556f30..c244b9cae 100644 --- 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-. -- 2.39.2