From 632c54beaf67e68a1eeeec22274466157003b779 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 5 Apr 2017 16:02:22 +0000 Subject: [PATCH] - first prroperties on lfsx proved - component "conversion" completed - some typos fixed --- .../lambdadelta/basic_2/conversion/cpc.ma | 25 ++++--- .../lambdadelta/basic_2/conversion/cpc_cpc.ma | 6 +- .../basic_2/etc/lfpx/lfpx_fqus.etc | 66 +++++++++++++++++ .../relations/{pconv_4.ma => pconv_5.ma} | 4 +- .../lambdadelta/basic_2/relocation/lexs.ma | 13 ++++ .../{lfsx_fqus.ma => lfsx_fqup.ma} | 2 +- .../basic_2/rt_computation/lfsx_lfsx.ma | 47 +++++------- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpx_lfdeq.ma | 74 ++----------------- .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 37 ++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 +- .../matita/contribs/lambdadelta/partial.txt | 1 + 12 files changed, 167 insertions(+), 118 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpx/lfpx_fqus.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{pconv_4.ma => pconv_5.ma} (92%) rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lfsx_fqus.ma => lfsx_fqup.ma} (97%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma index 1268d8887..156374e3f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma @@ -12,29 +12,30 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/pconv_4.ma". -include "basic_2/reduction/cpr.ma". +include "basic_2/notation/relations/pconv_5.ma". +include "basic_2/rt_transition/cpm.ma". -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************) +(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) -definition cpc: relation4 genv lenv term term ≝ - λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 ∨ ⦃G, L⦄ ⊢ T2 ➡ T1. +definition cpc: sh → relation4 genv lenv term term ≝ + λh,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 ∨ ⦃G, L⦄ ⊢ T2 ➡[h] T1. interpretation - "context-sensitive parallel conversion (term)" - 'PConv G L T1 T2 = (cpc G L T1 T2). + "context-sensitive parallel r-conversion (term)" + 'PConv h G L T1 T2 = (cpc h G L T1 T2). (* Basic properties *********************************************************) -lemma cpc_refl: ∀G,L. reflexive … (cpc G L). +lemma cpc_refl: ∀h,G,L. reflexive … (cpc h G L). /2 width=1 by or_intror/ qed. -lemma cpc_sym: ∀G,L. symmetric … (cpc L G). -#G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/ +lemma cpc_sym: ∀h,G,L. symmetric … (cpc h L G). +#h #G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/ qed-. (* Basic forward lemmas *****************************************************) -lemma cpc_fwd_cpr: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ➡ T & ⦃G, L⦄ ⊢ T2 ➡ T. -#G #L #T1 #T2 * /2 width=3 by ex2_intro/ +lemma cpc_fwd_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[h] T & ⦃G, L⦄ ⊢ T2 ➡[h] T. +#h #G #L #T1 #T2 * /2 width=3 by ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma index 14518aaab..92ce08e18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma @@ -14,10 +14,10 @@ include "basic_2/conversion/cpc.ma". -(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************) +(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) (* Main properties **********************************************************) -theorem cpc_conf: ∀G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T. +theorem cpc_conf: ∀h,G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌[h] T1 → ⦃G, L⦄ ⊢ T0 ⬌[h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌[h] T & ⦃G, L⦄ ⊢ T2 ⬌[h] T. /3 width=3 by cpc_sym, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpx/lfpx_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpx/lfpx_fqus.etc new file mode 100644 index 000000000..c67ddb150 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpx/lfpx_fqus.etc @@ -0,0 +1,66 @@ +(* +(* Properties with supclosure ***********************************************) + +lemma lpx_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 + #K0 #V0 #H1KL1 #_ #H destruct + elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // + #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct + /2 width=4 by fqu_lref_O, ex3_intro/ +| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (drop_O1_le (Ⓕ) (k+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpx_drop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpx_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpx_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma index a7563d0c0..4c9e62514 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌ break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌ [ break term 46 h ] break term 46 T2 )" non associative with precedence 45 - for @{ 'PConv $G $L $T1 $T2 }. + for @{ 'PConv $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 9c009bbf2..b002e073a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -242,3 +242,16 @@ lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) → #g2 #H #H2 destruct /3 width=5 by lexs_next/ ] qed-. + +lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + ∀f,L1,L2. L1 ⦻*[R1, RP, f] L2 → ∀g. f ⊆ g → + ∃∃L. L1 ⦻*[R1, RP, g] L & L ⦻*[R2, cfull, f] L2. +#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 +[ /2 width=3 by lexs_atom, ex2_intro/ ] +#f #I #L1 #L2 #V1 #V2 #_ #HV12 #IH #y #H +[ elim (sle_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct + elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, ex2_intro/ +| elim (sle_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct + elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma index 789453aa9..10bcdd59c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/lfdeq_fqus.ma". +include "basic_2/static/lfdeq_fqup.ma". include "basic_2/rt_computation/lfsx.ma". (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index 5ea3071b0..7ca826d11 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -18,9 +18,6 @@ include "basic_2/rt_computation/lfsx.ma". (* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) -axiom pippo: ∀h,o,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L & L ≡[h, o, V] L2. - (* Advanced properties ******************************************************) lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → @@ -33,37 +30,29 @@ qed-. (* Advanced forward lemmas **************************************************) -(* Basic_2A1: was: lsx_fwd_bind_sn *) -lemma lfsx_fwd_bind_sn: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ → +(* Basic_2A1: includes: lsx_fwd_bind_sn lsx_fwd_flat_sn *) +(* Basic_2A1: was: lsx_fwd_pair_sn *) +lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄. -#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L -#L1 #_ #IHL1 @lfsx_intro -#L2 #H #HnL12 elim (pippo … o p I … T H) -H -/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_sn/ -qed-. -(* -lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L. -#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L #L1 #_ #IHL1 @lfsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/ +#L2 #H #HnL12 elim (lfpx_pair_sn_split … o I … T H) -H +/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/ qed-. -lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, T, l] L. -#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L -#L1 #_ #IHL1 @lfsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/ -qed-. -lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L. -#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/ +(* Basic_2A1: was: lsx_fwd_flat_dx *) +lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +#h #o #I #G #L #V #T #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #H #HnL12 elim (lfpx_flat_dx_split … o I … V … H) -H +/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_flat_dx/ qed-. -(* Basic inversion lemmas ***************************************************) +(* Advanced inversion lemmas ************************************************) -lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L. -/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-. -*) \ No newline at end of file +(* Basic_2A1: was: lsx_inv_flat *) +lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. +/3 width=3 by lfsx_fwd_pair_sn, lfsx_fwd_flat_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 4269b54d2..610a54f77 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -2,4 +2,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.m lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -lfsx.ma lfsx_fqup.ma +lfsx.ma lfsx_fqup.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 7af823975..020bd81c5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -22,6 +22,14 @@ include "basic_2/rt_transition/lfpx.ma". (**) (* should be in lfpx_frees.ma *) (* Properties with degree-based equivalence for local environments **********) +lemma lfpx_pair_sn_split: ∀h,o,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≡[h, o, V] L2. +/3 width=5 by lfpx_frees_conf, lfxs_pair_sn_split/ qed-. + +lemma lfpx_flat_dx_split: ∀h,o,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≡[h, o, T] L2. +/3 width=5 by lfpx_frees_conf, lfxs_flat_dx_split/ qed-. + lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). #h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ [ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02 @@ -146,69 +154,3 @@ lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → elim (lfpx_lfdeq_conf … o … HLK2 L1) /3 width=3 by lfdeq_sym, ex2_intro/ qed-. -(* -(* Properties with supclosure ***********************************************) - -lemma lpx_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 - #K0 #V0 #H1KL1 #_ #H destruct - elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (drop_inv_O2 … H) -H #H destruct - /2 width=4 by fqu_lref_O, ex3_intro/ -| * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpx_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (drop_O1_le (Ⓕ) (k+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpx_drop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpx_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpx_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpx_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 56ce31016..3b94bdb61 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -19,6 +19,43 @@ include "basic_2/static/lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) +(* Advanced properties ******************************************************) + +lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lexs_frees_confluent … R1 cfull → + ∀L1,L2,V. L1 ⦻*[R1, V] L2 → ∀I,T. + ∃∃L. L1 ⦻*[R1, ②{I}V.T] L & L ⦻*[R2, V] L2. +#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T +[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg + elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy +| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg + elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy +] +lapply(frees_mono … H … Hf) -H #H1 +lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy +lapply (sor_inv_sle_sn … Hy) -y2 #Hfg +elim (lexs_sle_split … HR1 HR2 … HL12 … Hfg) -HL12 #L #HL1 #HL2 +lapply (sle_lexs_trans … HL1 … Hfg) // #H +elim (HR … Hf … H) -HR -Hf -H +/4 width=7 by sle_lexs_trans, ex2_intro/ +qed-. + +lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lexs_frees_confluent … R1 cfull → + ∀L1,L2,T. L1 ⦻*[R1, T] L2 → ∀I,V. + ∃∃L. L1 ⦻*[R1, ⓕ{I}V.T] L & L ⦻*[R2, T] L2. +#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V +elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg +elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy +lapply(frees_mono … H … Hf) -H #H2 +lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy +lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +elim (lexs_sle_split … HR1 HR2 … HL12 … Hfg) -HL12 #L #HL1 #HL2 +lapply (sle_lexs_trans … HL1 … Hfg) // #H +elim (HR … Hf … H) -HR -Hf -H +/4 width=7 by sle_lexs_trans, ex2_intro/ +qed-. + (* Main properties **********************************************************) theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T. 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 68759e53b..0ac1d94d2 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 @@ -62,15 +62,15 @@ table { ] } ] +*) class "blue" [ { "conversion" * } { - [ { "context-sensitive conversion" * } { - [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ] + [ { "context-sensitive r-conversion" * } { + [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] } ] } ] -*) class "sky" [ { "rt-computation" * } { (* @@ -124,7 +124,7 @@ table { ] class "cyan" [ { "rt-transition" * } { - [ { "parallel rst-transition" * } { + [ { "uncounted rst-transition" * } { [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 4f87c5f77..909355c60 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -6,4 +6,5 @@ basic_2/s_computation basic_2/static basic_2/i_static basic_2/rt_transition +basic_2/conversion apps_2/examples/ex_cpr_omega.ma -- 2.39.2