From: Ferruccio Guidi Date: Fri, 17 Nov 2017 14:34:37 +0000 (+0000) Subject: - ext2_tc added X-Git-Tag: make_still_working~405 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7cf2232827c06c7e85a9bc3be005f9134d5b869d;p=helm.git - ext2_tc added - lexs_tc reconstructed - support for lex (was lpx_sn) reintroduced - fixed a bug about ceq --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc deleted file mode 100644 index cb772458b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc +++ /dev/null @@ -1,49 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on transitive_closure *****************************************) - -lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. lpx_sn (LTC … R) L1 L2 → - TC … (lpx_sn R) L1 L2. -#R #HR #L1 #L2 #H elim H -L1 -L2 -/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ -qed-. - -(* Inversion lemmas on transitive closure ***********************************) - -lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀S:relation lenv. - S (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → - S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. -#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 -[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // -| #L2 #I #V2 #IHL2 #X #H - elim (TC_lpx_sn_inv_pair2 … H) // -H -HR - #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ -] -qed-. - -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - lpx_sn (LTC … R) L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma new file mode 100644 index 000000000..8f247592c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfeq.ma". +*) +include "basic_2/static/lfxs_lfxs.ma". +include "basic_2/i_static/tc_lfxs_fqup.ma". + +include "basic_2/notation/relations/lazyeqsn_3.ma". + +definition ceq_ext: relation3 lenv bind bind ≝ + cext2 (λL,T1,T2. T1 = T2). + +definition lfeq: relation3 term lenv lenv ≝ + lfxs (λL,T1,T2. T1 = T2). + +interpretation + "syntactic equivalence on referred entries (local environment)" + 'LazyEqSn T L1 L2 = (lfeq T L1 L2). + +axiom lfeq_lfxs_trans: ∀R,L1,L,T. L1 ≡[T] L → + ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. + +axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2. +(* +#R #L #I1 #I2 * -I1 -I2 +[ /2 width=1 by ext2_unit, inj/ +| #I #V1 #V2 #HV12 +*) + + +(* +lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) → + ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → + TC … (lexs RN RP f) L1 L2. +#RN #RP #HRP #f #L1 #L2 #H elim H -f -L1 -L2 +[ /2 width=1 by lexs_atom, inj/ ] +#f #I1 #I2 #L1 #L2 #HL12 #HI12 #IH +[ @step [3: +*) + +axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP → + lexs_frees_confluent (LTC … RN) RP. +(* +#RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H +*) +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +lemma pippo: ∀R. (∀L. reflexive … (R L)) → + (lexs_frees_confluent (cext2 R) cfull) → + ∀L1,L2,T. L1 ⪤**[R, T] L2 → + ∃∃L. L1 ⪤*[LTC … R, T] L & L ≡[T] L2. +#R #H1R #H2R #L1 #L2 #T #H +@(tc_lfxs_ind_sn … H1R … H) -H -L2 +[ /4 width=5 by lfxs_refl, inj, ex2_intro/ +| #L0 #L2 #_ #HL02 * #L * #f1 #Hf1 #HL1 #HL0 + lapply (lexs_co ??? cfull … (cext2_inv_LTC R) … HL1) -HL1 // #HL1 + lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 #HL2 + elim (lexs_frees_confluent_LTC_sn … H2R … Hf1 … HL1) #f2 #Hf2 #Hf21 + lapply (lfxs_inv_frees … HL2 … Hf2) -HL2 #HL2 + elim (lexs_sle_split … ceq_ext … HL2 … Hf21) -HL2 + [ #L0 #HL0 #HL02 + |*: /2 width=1 by ext2_refl/ + ] + lapply (sle_lexs_trans … HL0 … Hf21) -Hf21 // #H + elim (H2R … Hf2 … H) -H #f0 #Hf0 #Hf02 + lapply (sle_lexs_trans … HL02 … Hf02) -f2 // #HL02 + @(ex2_intro … L0) + [ @(ex2_intro … Hf1) + | @(ex2_intro … HL02) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relation_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relation_3.ma new file mode 100644 index 000000000..251dbf3f9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relation_3.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 R ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'Relation $R $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index d469f0ac1..5e8cfaeaa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -432,10 +432,12 @@ qed-. (* Properties with context-sensitive equivalence for terms ******************) -lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq. +lemma ceq_lift_sn: d_liftable2_sn … liftsb ceq_ext. +#K #I1 #I2 #H <(ceq_ext_inv_eq … H) -I2 /2 width=3 by ex2_intro/ qed-. -lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq. +lemma ceq_inv_lift_sn: d_deliftable2_sn … liftsb ceq_ext. +#L #J1 #J2 #H <(ceq_ext_inv_eq … H) -J2 /2 width=3 by ex2_intro/ qed-. (* Note: d_deliftable2_sn cfull does not hold *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index b96a2ddcc..a1ca60e4c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -33,8 +33,9 @@ lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 → ∀b,f,I,K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} → 𝐔⦃f⦄ → ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} & K1 ≡[f1] K2. -#f2 #L1 #L2 #HL12 #b #f #I #K1 #HLK1 #Hf #f1 #Hf2 -elim (lexs_drops_trans_next … HL12 … HLK1 Hf … Hf2) -f2 -L2 -Hf +#f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2 +elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf +#I1 #K1 #HLK1 #HK12 #H <(ceq_ext_inv_eq … H) -I2 /2 width=3 by ex2_intro/ qed-. @@ -43,7 +44,7 @@ lemma lreq_drops_conf_next: ∀f2,L1,L2. L1 ≡[f2] L2 → ∀b,f,I,K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} → 𝐔⦃f⦄ → ∀f1. f ~⊚ ⫯f1 ≡ f2 → ∃∃K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} & K1 ≡[f1] K2. -#f2 #L1 #L2 #HL12 #b #f #I #K1 #HLK1 #Hf #f1 #Hf2 +#f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2 elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf /3 width=3 by lreq_sym, ex2_intro/ qed-. @@ -52,6 +53,9 @@ lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 → ∀b,f,I,L1. ⬇*[b, f] L1.ⓘ{I} ≡ K1 → ∀f2. f ~⊚ f1 ≡ ⫯f2 → ∃∃L2. ⬇*[b, f] L2.ⓘ{I} ≡ K2 & L1 ≡[f2] L2 & L1.ⓘ{I} ≡[f] L2.ⓘ{I}. -#f1 #K1 #K2 #HK12 #b #f #I #L1 #HLK1 #f2 #Hf2 +#f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1 -/2 width=6 by cfull_lift_sn, ceq_lift_sn, ex3_intro/ qed-. +/2 width=6 by cfull_lift_sn, ceq_lift_sn/ +#I2 #L2 #HLK2 #HL12 #H >(ceq_ext_inv_eq … H) -I1 +/2 width=4 by ex3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma new file mode 100644 index 000000000..72260e801 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/relations/relation_3.ma". +include "basic_2/relocation/lexs.ma". + +(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************) + +(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) +definition lex: (lenv → relation bind) → relation lenv ≝ + λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, R, f] L2. + +interpretation "generic extension (local environment)" + 'Relation R L1 L2 = (lex R L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index acfd31ed5..bd0a3af6b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -18,7 +18,6 @@ include "basic_2/syntax/lenv.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) -(* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) inductive lexs (RN,RP:relation3 lenv bind bind): rtmap → relation lenv ≝ | lexs_atom: ∀f. lexs RN RP f (⋆) (⋆) | lexs_next: ∀f,I1,I2,L1,L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma new file mode 100644 index 000000000..e68f1109d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma @@ -0,0 +1,118 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lib/star.ma". +include "basic_2/relocation/lexs.ma". + +(* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) + +(* Properties with transitive closure ***************************************) + +lemma lexs_tc_refl: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f. reflexive … (TC … (lexs RN RP f)). +/3 width=1 by lexs_refl, TC_reflexive/ qed. + +lemma lexs_tc_next_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → + ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RN L1 I1 I2 → + TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 +/3 width=3 by lexs_next, TC_strap, inj/ +qed. + +lemma lexs_tc_next_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 → + TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 +/4 width=5 by lexs_refl, lexs_next, step, inj/ +qed. + +lemma lexs_tc_push_sn: ∀RN,RP. (∀L. reflexive … (RP L)) → + ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RP L1 I1 I2 → + TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRP #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 +/3 width=3 by lexs_push, TC_strap, inj/ +qed. + +lemma lexs_tc_push_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 → + TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 +/4 width=5 by lexs_refl, lexs_push, step, inj/ +qed. + +lemma lexs_tc_inj_sn: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → L1 ⪤*[LTC … RN, RP, f] L2. +#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2 +/3 width=1 by lexs_push, lexs_next, inj/ +qed. + +lemma lexs_tc_inj_dx: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → L1 ⪤*[RN, LTC … RP, f] L2. +#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2 +/3 width=1 by lexs_push, lexs_next, inj/ +qed. + +(* Main properties with transitive closure **********************************) + +theorem lexs_tc_next: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 → + TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 +/4 width=5 by lexs_tc_next_sn, lexs_tc_refl, trans_TC/ +qed. + +theorem lexs_tc_push: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 → + TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). +#RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 +/4 width=5 by lexs_tc_push_sn, lexs_tc_refl, trans_TC/ +qed. + +(* Basic_2A1: uses: TC_lpx_sn_ind *) +theorem lexs_tc_step_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) → + ∀f,L1,L. L1 ⪤*[RN, RP, f] L → 𝐈⦃f⦄ → + ∀L2. L ⪤*[RN, LTC … RP, f] L2 → L1⪤* [RN, LTC … RP, f] L2. +#RN #RP #HRP #f #L1 #L #H elim H -f -L1 -L +[ #f #_ #Y #H -HRP >(lexs_inv_atom1 … H) -Y // ] +#f #I1 #I #L1 #L #HL1 #HI1 #IH #Hf #Y #H +[ elim (isid_inv_next … Hf) -Hf // +| lapply (isid_inv_push … Hf ??) -Hf [3: |*: // ] #Hf + elim (lexs_inv_push1 … H) -H #I2 #L2 #HL2 #HI2 #H destruct + @lexs_push [ /2 width=1 by/ ] -L2 -IH + @(TC_strap … HI1) -HI1 + @(HRP … HL1) // (**) (* auto fails *) +] +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: TC_lpx_sn_inv_lpx_sn_LTC *) +lemma lexs_tc_dx: ∀RN,RP. (∀f. 𝐈⦃f⦄ → s_rs_transitive … RP (λ_.lexs RN RP f)) → + ∀f. 𝐈⦃f⦄ → ∀L1,L2. TC … (lexs RN RP f) L1 L2 → L1 ⪤*[RN, LTC … RP, f] L2. +#RN #RP #HRP #f #Hf #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 +/3 width=3 by lexs_tc_step_dx, lexs_tc_inj_dx/ +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lexs_inv_tc_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → TC … (lexs RN RP f) L1 L2. +#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 +/2 width=1 by lexs_tc_next, lexs_tc_push_sn, lexs_atom, inj/ +qed-. + +(* Basic_2A1: uses: lpx_sn_LTC_TC_lpx_sn *) +lemma lexs_inv_tc_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → + ∀f,L1,L2. L1 ⪤*[RN, LTC … RP, f] L2 → TC … (lexs RN RP f) L1 L2. +#RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 +/2 width=1 by lexs_tc_push, lexs_tc_next_sn, lexs_atom, inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index e0b7d236c..1442fa552 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -13,13 +13,13 @@ (**************************************************************************) include "basic_2/notation/relations/lazyeqsn_3.ma". -include "basic_2/syntax/ext2.ma". +include "basic_2/syntax/lenv_ceq.ma". include "basic_2/relocation/lexs.ma". (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) (* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *) -definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq cfull. +definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq_ext cfull. interpretation "ranged equivalence (local environment)" @@ -39,11 +39,11 @@ lemma sle_lreq_trans: ∀f2,L1,L2. L1 ≡[f2] L2 → (* Basic_2A1: includes: lreq_refl *) lemma lreq_refl: ∀f. reflexive … (lreq f). -/3 width=1 by lexs_refl, ext2_refl/ qed. +/2 width=1 by lexs_refl/ qed. (* Basic_2A1: includes: lreq_sym *) lemma lreq_sym: ∀f. symmetric … (lreq f). -/3 width=1 by lexs_sym, ext2_sym/ qed-. +/3 width=2 by lexs_sym, cext2_sym/ qed-. (* Basic inversion lemmas ***************************************************) @@ -54,7 +54,9 @@ lemma lreq_inv_atom1: ∀f,Y. ⋆ ≡[f] Y → Y = ⋆. (* Basic_2A1: includes: lreq_inv_pair1 *) lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≡[⫯g] Y → ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ{J}. -#g #J #K1 #Y #H elim (lexs_inv_next1 … H) -H /2 width=3 by ex2_intro/ +#g #J #K1 #Y #H +elim (lexs_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct +<(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *) @@ -70,7 +72,9 @@ lemma lreq_inv_atom2: ∀f,X. X ≡[f] ⋆ → X = ⋆. (* Basic_2A1: includes: lreq_inv_pair2 *) lemma lreq_inv_next2: ∀g,J,X,K2. X ≡[⫯g] K2.ⓘ{J} → ∃∃K1. K1 ≡[g] K2 & X = K1.ⓘ{J}. -#g #J #X #K2 #H elim (lexs_inv_next2 … H) -H /2 width=3 by ex2_intro/ +#g #J #X #K2 #H +elim (lexs_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct +<(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *) @@ -82,7 +86,9 @@ qed-. (* Basic_2A1: includes: lreq_inv_pair *) lemma lreq_inv_next: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[⫯f] L2.ⓘ{I2} → L1 ≡[f] L2 ∧ I1 = I2. -/2 width=1 by lexs_inv_next/ qed-. +#f #I1 #I2 #L1 #L2 #H elim (lexs_inv_next … H) -H +/3 width=3 by ceq_ext_inv_eq, conj/ +qed-. (* Basic_2A1: includes: lreq_inv_succ *) lemma lreq_inv_push: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[↑f] L2.ⓘ{I2} → L1 ≡[f] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma index 42aaf3eea..ec166cb7d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/syntax/ceq_ext_ceq_ext.ma". include "basic_2/relocation/lexs_lexs.ma". (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) @@ -19,7 +20,7 @@ include "basic_2/relocation/lexs_lexs.ma". (* Main properties **********************************************************) theorem lreq_trans: ∀f. Transitive … (lreq f). -/2 width=3 by lexs_trans/ qed-. +/3 width=5 by lexs_trans, ceq_ext_trans/ qed-. theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f). /3 width=3 by lexs_canc_sn, lreq_trans, lreq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma new file mode 100644 index 000000000..440bddba4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ceq_ext_ceq_ext.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/lenv_ceq.ma". + +(* CONTEXT-DEPENDENT SYNTACTIC EQUIVALENCE FOR BINDERS **********************) + +(* Main properties **********************************************************) + +theorem ceq_ext_trans: ∀L1,I1,I. ceq_ext L1 I1 I → + ∀L2,I2. ceq_ext L2 I I2 → ∀L3. ceq_ext L3 I1 I2. +#L1 #I1 #I * -I1 -I // +#I1 #V1 #V #HV1 #L2 #Z #H elim (ext2_inv_pair_sn … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/ext2_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/ext2_tc.ma new file mode 100644 index 000000000..1fc4bd4bf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/ext2_tc.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lib/star.ma". +include "basic_2/syntax/ext2.ma". + +(* EXTENSION TO BINDERS OF A RELATION FOR TERMS *****************************) + +(* Properties with transitive closure ***************************************) + +lemma ext2_tc_pair: ∀R,I,V1,V2. TC … R V1 V2 → + TC … (ext2 R) (BPair I V1) (BPair I V2). +#R #I #V1 #V2 #H elim H -H -V2 +/3 width=3 by ext2_pair, step, inj/ +qed. + +lemma ext2_tc_inj: ∀R,I1,I2. ext2 R I1 I2 → ext2 (TC … R) I1 I2. +#R #I1 #I2 * -I1 -I2 +/3 width=1 by ext2_unit, ext2_pair, inj/ +qed. + +(* Main properties with transitive closure **********************************) + +theorem ext2_tc_step: ∀R,I1,I. ext2 (TC … R) I1 I → + ∀I2. ext2 R I I2 → ext2 (TC … R) I1 I2. +#R #I1 #I * -I1 -I +[ #I #Z #H >(ext2_inv_unit_sn … H) -Z /2 width=1 by ext2_unit/ +| #I #V1 #V #HV1 #Z #H + elim (ext2_inv_pair_sn … H) -H #V2 #HV2 #H destruct + /3 width=3 by ext2_pair, step/ +] +qed-. + +(* Advanced properties with transitive closure ******************************) + +lemma ext2_tc: ∀R,I1,I2. TC … (ext2 R) I1 I2 → ext2 (TC … R) I1 I2. +#R #I1 #I2 #H elim H -I2 +/2 width=3 by ext2_tc_step, ext2_tc_inj/ +qed. + +(* Advanced inversion lemmas with transitive closure ************************) + +lemma ext2_inv_tc: ∀R,I1,I2. ext2 (TC … R) I1 I2 → TC … (ext2 R) I1 I2. +#R #I1 #I2 * -I1 -I2 +/3 width=1 by ext2_tc_pair, ext2_unit, inj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma index 8cb745690..2822b5d4b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma @@ -52,7 +52,7 @@ interpretation "abstraction (local environment)" definition cfull: relation3 lenv bind bind ≝ λL,I1,I2. ⊤. -definition ceq: relation3 lenv bind bind ≝ λL. eq …. +definition ceq: relation3 lenv term term ≝ λL. eq …. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma new file mode 100644 index 000000000..8ae1e8148 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ceq.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/lenv_ext2.ma". + +(* EXTENSION TO BINDERS OF A CONTEXT-SENSITIVE RELATION FOR TERMS ***********) + +definition ceq_ext: lenv → relation bind ≝ + cext2 ceq. + +(* Basic properties *********************************************************) + +lemma ceq_ext_refl (L): reflexive … (ceq_ext L). +/2 width=1 by ext2_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ceq_ext_inv_eq: ∀L,I1,I2. ceq_ext L I1 I2 → I1 = I2. +#L #I1 #I2 * -I1 -I2 // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 77fe48710..4f947c2dc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -221,7 +221,7 @@ table { } ] [ { "generic entrywise extension" * } { - [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ] + [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] } ] } @@ -258,7 +258,7 @@ table { } ] [ { "binders for local environments" * } { - [ "ext2" "ext2_ext2" * ] + [ "ext2" "ext2_tc" + "ext2_ext2" * ] [ "bind" "bind_weight" * ] } ]