From 075441b55fa8a6fa693a1c96ed60ab4d87c42a2d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 19 Sep 2016 15:37:58 +0000 Subject: [PATCH] some improvements towards the confluence of lfpr ... --- .../basic_2/etc_new/droppreds_3.etc | 19 +++ .../lambdadelta/basic_2/etc_new/frees_etc.etc | 136 ++++++++++++++++++ .../lambdadelta/basic_2/etc_new/lfpr_main.etc | 80 +++++++++++ .../lambdadelta/basic_2/etc_new/lfxs_main.etc | 25 ++++ .../lambdadelta/basic_2/etc_new/ltls.etc | 47 ++++++ .../basic_2/relocation/lexs_lexs.ma | 41 +++--- .../lambdadelta/basic_2/rt_transition/lfpr.ma | 32 ++++- .../basic_2/rt_transition/lfpr_lfpr.ma | 12 +- .../lambdadelta/basic_2/rt_transition/lfpx.ma | 28 ++++ .../lambdadelta/basic_2/static/lfxs.ma | 74 +++++++++- 10 files changed, 455 insertions(+), 39 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/lfpr_main.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/lfxs_main.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/ltls.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc new file mode 100644 index 000000000..b21fe5117 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/droppreds_3.etc @@ -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( ⫱ * [ term 46 L , break term 46 K ] term 46 f )" + non associative with precedence 46 + for @{ 'DropPreds $L $K $f }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc new file mode 100644 index 000000000..3fcd30d9b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/frees_etc.etc @@ -0,0 +1,136 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops_weight.ma". +include "basic_2/s_computation/fqup_weight.ma". +include "basic_2/s_computation/fqus_fqup.ma". +include "basic_2/static/frees.ma". + +corec lemma sle_refl: ∀f. f ⊆ f. +#f cases (pn_split f) * #g #H +[ @(sle_push … H H) | @(sle_next … H H) ] -H // +qed. + +lemma sle_inv_tl1: ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ⫯f2. +#f1 elim (pn_split f1) * #g #H destruct +/2 width=5 by sle_next, sle_weak/ +qed-. + +axiom sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≡ f → + ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≡ ⫱*[n]f. + +axiom sor_sle1: ∀f1,f2,f. f1 ⋓ f2 ≡ f → + ∀g. g ⊆ f1 → g ⊆ f. + +axiom sor_sle2: ∀f1,f2,f. f1 ⋓ f2 ≡ f → + ∀g. g ⊆ f2 → g ⊆ f. + +lemma fqus_inv_refl_atom3: ∀I,G,L,X. ⦃G, L, ⓪{I}⦄ ⊐* ⦃G, L, X⦄ → ⓪{I} = X. +#I #G #L #X #H elim (fqus_inv_fqup … H) -H [2: * // ] +#H lapply (fqup_fwd_fw … H) -H +#H elim (lt_le_false … H) -H /2 width=1 by monotonic_le_plus_r/ +qed-. + +axiom drops_T_isuni_inv_refl: ∀n,L. ⬇*[n] L ≡ L → n = 0. + +axiom fqus_split_fqu: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + (∧∧ G1 = G2 & L1 = L2 & T1 = T2) ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊐ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊐* ⦃G2, L2, T2⦄. + +axiom fqus_inv_atom1: ∀I,G1,G2,L2,T2. ⦃G1, ⋆, ⓪{I}⦄ ⊐* ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & ⋆ = L2 & ⓪{I} = T2. + +axiom fqus_inv_sort1: ∀G1,G2,L1,L2,T2,s. ⦃G1, L1, ⋆s⦄ ⊐* ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 = L2 & ⋆s = T2. + +axiom fqus_inv_zero1: ∀I,G1,G2,L1,L2,V1,T2. ⦃G1, L1.ⓑ{I}V1, #0⦄ ⊐* ⦃G2, L2, T2⦄ → + (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #0 = T2) ∨ ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄. + +axiom fqus_inv_lref1: ∀I,G1,G2,L1,L2,V1,T2,i. ⦃G1, L1.ⓑ{I}V1, #⫯i⦄ ⊐* ⦃G2, L2, T2⦄ → + (∧∧ G1 = G2 & L1.ⓑ{I}V1 = L2 & #(⫯i) = T2) ∨ ⦃G1, L1, #i⦄ ⊐* ⦃G2, L2, T2⦄. + +axiom fqus_inv_gref1: ∀G1,G2,L1,L2,T2,l. ⦃G1, L1, §l⦄ ⊐* ⦃G2, L2, T2⦄ → + ∧∧ G1 = G2 & L1 = L2 & §l = T2. + +axiom fqus_inv_bind1: ∀p,I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓑ{p,I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓑ{p,I}V1.T1 = T2 + | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ + | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐* ⦃G2, L2, T2⦄. + +axiom fqus_inv_flat1: ∀I,G1,G2,L1,L2,V1,T1,T2. ⦃G1, L1, ⓕ{I}V1.T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∨∨ ∧∧ G1 = G2 & L1 = L2 & ⓕ{I}V1.T1 = T2 + | ⦃G1, L1, V1⦄ ⊐* ⦃G2, L2, T2⦄ + | ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄. + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +lemma frees_drops_sle: ∀f1,G,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → + ∀L2,T2. ⦃G, L1, T1⦄ ⊐* ⦃G, L2, T2⦄ → + ∀I,n. ⬇*[n] L1 ≡ L2.ⓑ{I}T2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ ⫱*[⫯n] f1. +#f1 #G #L1 #T1 #H elim H -f1 -L1 -T1 +[ #f1 #J #Hf1 #L2 #T2 #H12 #I #n #HL12 + elim (fqus_inv_atom1 … H12) -H12 #H1 #H2 #H3 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // +| #f1 #J #L1 #V1 #s #_ #_ #L2 #T2 #H12 #I #n #HL12 + elim (fqus_inv_sort1 … H12) -H12 #H1 #H2 #H3 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // +| #f1 #J #L1 #V1 #Hf1 #IH #L2 #T2 #H12 + elim (fqus_inv_zero1 … H12) -H12 [ * | #H12 #I * ] + [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // + | -IH -H12 #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // + #H destruct /3 width=3 by sle_refl, ex2_intro/ + | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12 + #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ + ] +| #f1 #J #L1 #V1 #i #Hf1 #IH #L2 #T2 #H12 + elim (fqus_inv_lref1 … H12) -H12 [ * | #H12 #I * ] + [ -IH -Hf1 #H1 #H2 #H3 #I #n #HL12 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // + | -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // + #H destruct <(fqus_inv_refl_atom3 … H12) -H12 /2 width=3 by sle_refl, ex2_intro/ + | -Hf1 #I #HL12 lapply (drops_inv_drop1 … HL12) -HL12 + #HL12 elim (IH … H12 … HL12) -IH -H12 -HL12 /3 width=3 by ex2_intro/ + ] +| #f1 #J #L1 #V1 #l #_ #_ #L2 #T2 #H12 #I #n #HL12 + elim (fqus_inv_gref1 … H12) -H12 #H1 #H2 #H3 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // +| #f1V #f1T #f1 #p #J #L1 #V #T #_ #_ #Hf1 #IHV #IHT #L2 #T2 #H12 #I #n #HL12 + elim (fqus_inv_bind1 … H12) -H12 [ * |*: #H12 ] + [ -IHV -IHT -Hf1 #H1 #H2 #H3 destruct + lapply (drops_fwd_lw … HL12) -HL12 #HL12 + elim (lt_le_false … HL12) -HL12 // + | -IHT elim (IHV … H12 … HL12) -IHV -H12 -HL12 + /4 width=6 by sor_tls, sor_sle1, ex2_intro/ + | -IHV elim (IHT … H12 I (⫯n)) -IHT -H12 /2 width=1 by drops_drop/ -HL12 + tls_S >S_pred // +qed-. + +definition ltls (f): lenv → lenv → rtmap ≝ λL,K. ⫱*[|L|-|K|] f. + +interpretation "ltls (rtmap)" 'DropPreds L K f = (ltls f L K). + +lemma ltls_refl: ∀f,L1,L2. |L1| ≤ |L2| → ⫱*[L1, L2] f = f. +#f #L1 #L2 #HL12 whd in ⊢ (??%?); >(eq_minus_O … HL12) -HL12 // +qed. + +lemma ltls_pair2: ∀f,I,L1,L2,V. |L2| < |L1| → ⫱⫱*[L1, L2.ⓑ{I}V] f = ⫱*[L1, L2] f. +#f #I #L1 #L2 #V #HL12 whd in ⊢ (??(?%)%); minus_Sn_m // +qed. + +lemma ltls_pair1_next: ∀f,I,L1,L2,V. |L2| ≤ |L1| → ⫱*[L1.ⓑ{I}V, L2] ⫯f = ⫱*[L1, L2] f. +#f #I #L1 #L2 #V #HL12 whd in ⊢ (??%%); >minus_Sn_m // +qed. + +lemma ltls_sle_pair: ∀f1,f2,L1,L2. ⫱*[L2, L1] f2 ⊆ ⫱*[L1, L2] f1 → + ∀I,V1. ⫱*[L2, L1.ⓑ{I}V1] f2 ⊆ ⫱*[L1.ⓑ{I}V1, L2] ⫯f1. +#f1 #f2 #L1 #L2 elim (lt_or_ge (|L1|) (|L2|)) +[ #HL12 >ltls_refl in ⊢ (??%→?); /2 width=1 by lt_to_le/ + #Hf21 #I #V1 >ltls_refl in ⊢ (??%); // + <(ltls_pair2 … I … V1 HL12) in Hf21; -HL12 /2 width=1 by sle_inv_tl1/ +| #HL21 >ltls_refl // #Hf21 #I #V1 >ltls_refl /2 width=1 by le_S/ + >ltls_pair1_next // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma index 7966fdd7c..7e7c3debc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -14,7 +14,6 @@ include "ground_2/relocation/rtmap_sand.ma". include "ground_2/relocation/rtmap_sor.ma". -include "basic_2/grammar/lenv_weight.ma". include "basic_2/relocation/lexs.ma". (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****) @@ -43,25 +42,27 @@ theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP → /2 width=9 by lexs_trans_gen/ qed-. (* Basic_2A1: includes: lpx_sn_conf *) -theorem lexs_conf: ∀RN1,RP1,RN2,RP2. - lexs_confluent RN1 RN2 RN1 RP1 RN2 RP2 → - lexs_confluent RP1 RP2 RN1 RP1 RN2 RP2 → - ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f). -#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0 generalize in match f; -f -@(f_ind … lw … L0) -L0 #x #IH * -[ #_ #f #X1 #H1 #X2 #H2 -x - >(lexs_inv_atom1 … H1) -X1 - >(lexs_inv_atom1 … H2) -X2 /2 width=3 by lexs_atom, ex2_intro/ -| #L0 #I #V0 #Hx #f elim (pn_split f) * - #g #H #X1 #H1 #X2 #H2 destruct - [ elim (lexs_inv_push1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2 - elim (HRP … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_push, ex2_intro/ - | elim (lexs_inv_next1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lexs_inv_next1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2 - elim (HRN … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_next, ex2_intro/ +theorem lexs_conf (RN1) (RP1) (RN2) (RP2): lexs_confluent RN1 RN2 RN1 RP1 RN2 RP2 → + lexs_confluent RP1 RP2 RN1 RP1 RN2 RP2 → + ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f). +#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0 +generalize in match f; -f elim L0 -L0 +[ #f #L1 #HL01 #L2 #HL02 -HRN -HRP + lapply (lexs_inv_atom1 … HL01) -HL01 #H destruct + lapply (lexs_inv_atom1 … HL02) -HL02 #H destruct + /2 width=3 by ex2_intro/ +| #K0 #I #V0 #IH #f #L1 #HL01 #L2 #HL02 + elim (pn_split f) * #g #H destruct + [ elim (lexs_inv_push1 … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct + elim (lexs_inv_push1 … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct + elim (IH … HK01 … HK02) -IH #K #HK1 #HK2 + elim (HRP … HV01 … HV02 … HK01 … HK02) -HRP -HRN -K0 -V0 + /3 width=5 by lexs_push, ex2_intro/ + | elim (lexs_inv_next1 … HL01) -HL01 #K1 #V1 #HK01 #HV01 #H destruct + elim (lexs_inv_next1 … HL02) -HL02 #K2 #V2 #HK02 #HV02 #H destruct + elim (IH … HK01 … HK02) -IH #K #HK1 #HK2 + elim (HRN … HV01 … HV02 … HK01 … HK02) -HRN -HRP -K0 -V0 + /3 width=5 by lexs_next, ex2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma index 299b0f8c8..381233f04 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma @@ -34,8 +34,8 @@ lemma lfpr_sort: ∀h,I,G,L1,L2,V1,V2,s. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2. /2 width=1 by lfxs_sort/ qed. -lemma lfpr_zero: ∀h,I,G,L1,L2,V. - ⦃G, L1⦄ ⊢ ➡[h, V] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V. +lemma lfpr_zero: ∀h,I,G,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → + ⦃G, L1⦄ ⊢ V1 ➡[h] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V2. /2 width=1 by lfxs_zero/ qed. lemma lfpr_lref: ∀h,I,G,L1,L2,V1,V2,i. @@ -60,6 +60,12 @@ lemma lfpr_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ➡[h, ⓪{I}] Y2 → Y2 = lemma lfpr_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ➡[h, ⓪{I}] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. +lemma lfpr_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +/2 width=1 by lfxs_inv_sort/ qed-. + lemma lfpr_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ➡[h, #0] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & @@ -73,6 +79,12 @@ lemma lfpr_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] Y2 → Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_lref/ qed-. +lemma lfpr_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +/2 width=1 by lfxs_inv_gref/ qed-. + lemma lfpr_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. @@ -83,6 +95,14 @@ lemma lfpr_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 (* Advanced inversion lemmas ************************************************) +lemma lfpr_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] Y2 → + ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_sort_pair_sn/ qed-. + +lemma lfpr_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_sort_pair_dx/ qed-. + lemma lfpr_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] Y2 → ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 & Y2 = L2.ⓑ{I}V2. @@ -101,6 +121,14 @@ lemma lfpr_inv_lref_pair_dx: ∀h,I,G,Y1,L2,V2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y1 = L1.ⓑ{I}V1. /2 width=2 by lfxs_inv_lref_pair_dx/ qed-. +lemma lfpr_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, §l] Y2 → + ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_gref_pair_sn/ qed-. + +lemma lfpr_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_gref_pair_dx/ qed-. + (* Basic forward lemmas *****************************************************) lemma lfpr_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index e8955fd1e..a78a84a89 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -298,7 +298,7 @@ lapply (lifts_mono … HX … HVU) -HX #H destruct /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. -theorem cpr_conf_lfpr: ∀h,G. lfxs_confluent (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G). +theorem cpr_conf_lfpr: ∀h,G. R_confluent_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G). #h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1_drops … H1) -H1 @@ -371,13 +371,3 @@ lemma lfpr_cpr_conf_sn: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → ∀L1. #h #G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (cpr_conf_lfpr … HT01 T0 … L0 … HL01) /2 width=3 by ex2_intro/ qed-. - -(* Main properties **********************************************************) - -(* - -theorem lpr_conf: ∀G. confluent … (lpr G). -/3 width=6 by lpx_sn_conf, cpr_conf_lpr/ -qed-. - -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index c0ca76840..ad9f1e03f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -60,6 +60,12 @@ lemma lfpx_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] Y2 → Y2 = lemma lfpx_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ⬈[h, ⓪{I}] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. +lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +/2 width=1 by lfxs_inv_sort/ qed-. + lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & @@ -73,6 +79,12 @@ lemma lfpx_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] Y2 → Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_lref/ qed-. +lemma lfpx_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +/2 width=1 by lfxs_inv_gref/ qed-. + lemma lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. @@ -83,6 +95,14 @@ lemma lfpx_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 (* Advanced inversion lemmas ************************************************) +lemma lfpx_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, ⋆s] Y2 → + ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_sort_pair_sn/ qed-. + +lemma lfpx_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_sort_pair_dx/ qed-. + lemma lfpx_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #0] Y2 → ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & Y2 = L2.ⓑ{I}V2. @@ -101,6 +121,14 @@ lemma lfpx_inv_lref_pair_dx: ∀h,I,G,Y1,L2,V2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & Y1 = L1.ⓑ{I}V1. /2 width=2 by lfxs_inv_lref_pair_dx/ qed-. +lemma lfpx_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, §l] Y2 → + ∃∃L2,V2. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y2 = L2.ⓑ{I}V2. +/2 width=2 by lfxs_inv_gref_pair_sn/ qed-. + +lemma lfpx_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 & Y1 = L1.ⓑ{I}V1. +/2 width=2 by lfxs_inv_gref_pair_dx/ qed-. + (* Basic forward lemmas *****************************************************) lemma lfpx_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index 88a8bd542..dba35a74a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -26,12 +26,12 @@ definition lfxs (R) (T): relation lenv ≝ interpretation "generic extension on referred entries (local environment)" 'RelationStar R T L1 L2 = (lfxs R T L1 L2). -definition lfxs_confluent: relation4 (relation3 lenv term term) - (relation3 lenv term term) … ≝ - λR1,R2,RP1,RP2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +definition R_confluent_lfxs: relation4 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RP1,RP2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. (* Basic properties ***********************************************************) @@ -72,6 +72,10 @@ lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ qed-. +lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 → + lexs_confluent R1 R2 RP1 cfull RP2 cfull. +#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 + (* Basic inversion lemmas ***************************************************) lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. @@ -82,6 +86,19 @@ lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. #R #I #Y1 * /2 width=4 by lexs_inv_atom2/ qed-. +lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_sort … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & @@ -104,6 +121,19 @@ lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → ] qed-. +lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2 +[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ +| lapply (frees_inv_gref … H1) -H1 #Hf + elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct + /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. #R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf @@ -118,6 +148,22 @@ qed-. (* Advanced inversion lemmas ************************************************) +lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → + ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & Y2 = L2.ⓑ{I}V2. @@ -154,6 +200,22 @@ lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 ] qed-. +lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → + ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + (* Basic forward lemmas *****************************************************) lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. -- 2.39.2