From 956df16197063a88b3858e3d212d7ed0f2c5ff46 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 25 Mar 2014 19:55:08 +0000 Subject: [PATCH] - partial commit: just the components below "computation" the development of lazy pointwise extensions continues ... - we parked not-lazy pointwise extensions in etc --- .../basic_2/etc/llpx_sn/llpx_sn_tc.etc | 160 ++++++++++++++++++ .../lpx_sn/ldrop_lpx_sn.etc} | 0 .../{reduction/lpr.ma => etc/lpx_sn/lpr.etc} | 0 .../lpr_ldrop.ma => etc/lpx_sn/lpr_ldrop.etc} | 0 .../lpr_lpr.ma => etc/lpx_sn/lpr_lpr.etc} | 0 .../lambdadelta/basic_2/etc/lpx_sn/lprs.etc | 71 ++++++++ .../basic_2/etc/lpx_sn/lprs_alt.etc | 47 +++++ .../basic_2/etc/lpx_sn/lprs_ldrop.etc | 29 ++++ .../basic_2/etc/lpx_sn/lprs_lprs.etc | 31 ++++ .../{reduction/lpx.ma => etc/lpx_sn/lpx.etc} | 0 .../lpx_aaa.ma => etc/lpx_sn/lpx_aaa.etc} | 0 .../lpx_ldrop.ma => etc/lpx_sn/lpx_ldrop.etc} | 0 .../lpx_lleq.ma => etc/lpx_sn/lpx_lleq.etc} | 0 .../lpx_sn.ma => etc/lpx_sn/lpx_sn.etc} | 0 .../lpx_sn/lpx_sn_lpx_sn.etc} | 0 .../lpx_sn_tc.ma => etc/lpx_sn/lpx_sn_tc.etc} | 0 .../predsn_3.ma => etc/lpx_sn/predsn_3.etc} | 0 .../predsn_5.ma => etc/lpx_sn/predsn_5.etc} | 0 .../lpx_sn/predsnstar_3.etc} | 0 .../lpx_sn/predsnstar_5.etc} | 0 .../lpx_sn/predsnstaralt_3.etc} | 0 .../lpx_sn/predsnstaralt_5.etc} | 0 .../notation/relations/lazypredsnstar_5.ma | 19 +++ .../notation/relations/lazypredsnstar_7.ma | 19 +++ .../basic_2/reduction/cpr_llpx_sn.ma | 47 +++++ .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 3 +- .../basic_2/reduction/cpx_llpx_sn.ma | 3 +- .../lambdadelta/basic_2/reduction/fpb.ma | 10 +- .../lambdadelta/basic_2/reduction/fpb_aaa.ma | 4 +- .../basic_2/reduction/llpr_ldrop.ma | 7 +- .../basic_2/reduction/llpr_llpr.ma | 2 +- .../lambdadelta/basic_2/reduction/llpx_aaa.ma | 81 +++++++++ .../basic_2/reduction/llpx_ldrop.ma | 3 +- .../basic_2/reduction/llpx_lleq.ma | 28 +++ .../basic_2/relocation/ldrop_leq.ma | 13 +- .../basic_2/relocation/llpx_sn_llpx_sn.ma | 10 +- .../lambdadelta/ground_2/etc/lib/star.etc | 31 ++++ .../contribs/lambdadelta/ground_2/lib/star.ma | 110 ++++++------ 38 files changed, 656 insertions(+), 72 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc rename matita/matita/contribs/lambdadelta/basic_2/{relocation/ldrop_lpx_sn.ma => etc/lpx_sn/ldrop_lpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpr.ma => etc/lpx_sn/lpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpr_ldrop.ma => etc/lpx_sn/lpr_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpr_lpr.ma => etc/lpx_sn/lpr_lpr.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx.ma => etc/lpx_sn/lpx.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_aaa.ma => etc/lpx_sn/lpx_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_ldrop.ma => etc/lpx_sn/lpx_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_lleq.ma => etc/lpx_sn/lpx_lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{grammar/lpx_sn.ma => etc/lpx_sn/lpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{grammar/lpx_sn_lpx_sn.ma => etc/lpx_sn/lpx_sn_lpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{grammar/lpx_sn_tc.ma => etc/lpx_sn/lpx_sn_tc.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsn_3.ma => etc/lpx_sn/predsn_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsn_5.ma => etc/lpx_sn/predsn_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsnstar_3.ma => etc/lpx_sn/predsnstar_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsnstar_5.ma => etc/lpx_sn/predsnstar_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsnstaralt_3.ma => etc/lpx_sn/predsnstaralt_3.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predsnstaralt_5.ma => etc/lpx_sn/predsnstaralt_5.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/etc/lib/star.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc new file mode 100644 index 000000000..682b48c68 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_tc.etc @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ldrop_leq.ma". +include "basic_2/relocation/llpx_sn.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +definition TC_llpx_sn_confluent1: relation (relation3 lenv term term) ≝ λS,R. + ∀Ls,T1,T2. S Ls T1 T2 → + ∀Ld. TC … (llpx_sn R 0 T1) Ls Ld → TC … (llpx_sn R 0 T2) Ls Ld. + +lemma TC_llpx_sn_s_confluent: ∀S,R. (llpx_sn_confluent1 S R) → TC_llpx_sn_confluent1 S R. +#S #R #HSR #Ls #T1 #T2 #HT12 #Ld #H +generalize in match HT12; -HT12 +@(TC_ind_dx … Ls H) -Ls +[ /3 width=3 by inj/ +| #Ls #L #HLs #_ #IHLd #HT12 + @(TC_strap … L) /2 width=3 by/ @IHLd -IHLd + +lemma TC_llpx_sn_lref_refl: ∀R. (∀L.reflexive … (R L)) → + ∀I,L1,K1,K2,V,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V → + TC lenv (llpx_sn R 0 V) K1 K2 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V → TC … (llpx_sn R d (#i)) L1 L2. +#R #HR #I #L1 #K1 #K2 #V #d #i #Hdi #HLK1 #H @(TC_star_ind … K2 H) -K2 +[ /2 width=1 by llpx_sn_refl/ +| /4 width=9 by llpx_sn_refl, llpx_sn_lref, inj/ +| #K #K2 #_ #HV #IHK1 #L2 #HLK2 lapply (ldrop_fwd_length … HLK2) + #H elim (ldrop_O1_ex (K.ⓑ{I}V) i L2) [2: normalize in H ⊢ %; >(llpx_sn_fwd_length … HV) ] + /4 width=11 by llpx_sn_lref, step/ +] +qed-. + +lemma TC_llpx_sn_lref: ∀R. (∀L.reflexive … (R L)) → (llpx_sn_confluent1 R R) → + ∀I,K1,V1,V2,d,i. d ≤ yinj i → LTC … R K1 V1 V2 → + ∀K2. TC lenv (llpx_sn R 0 V1) K1 K2 → ∀L1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → + ∀L2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → TC … (llpx_sn R d (#i)) L1 L2. +#R #H1R #H2R #I #K1 #V1 #V2 #d #i #Hdi #H @(TC_star_ind_dx … V1 H) -V1 +[ /2 width=1 by llpx_sn_refl/ +| /2 width=7 by TC_llpx_sn_lref_refl/ +| #V1 #V #HV1 #_ #IHV2 #K2 #HK12 #L1 #HLK1 #L2 #HLK2 + lapply (ldrop_fwd_length … HLK1) + #H elim (ldrop_O1_ex (K1.ⓑ{I}V) i L1) [2: normalize in H ⊢ %; // ] -H + #L #_ #HLK @(TC_strap … L) + [ @(llpx_sn_lref … HLK1 … HLK) /2 width=1 by llpx_sn_refl/ + | @(IHV2 … HLK … HLK2) + -HLK1 -HLK2 -HLK -IHV2 -Hdi @(TC_llpx_sn_s_confluent R R … HK12) // + ] +] + + +lemma llpx_sn_LTC_TC_llpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2,T,d. llpx_sn (LTC … R) d T L1 L2 → + TC … (llpx_sn R d T) L1 L2. +#R #HR #L1 #L2 #T #d #H elim H -L1 -L2 +/3 width=3 by llpx_sn_gref, llpx_sn_free, llpx_sn_skip, llpx_sn_sort, inj/ +[ #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #_ #HV12 #IHV1 + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +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_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. s_rs_trans … 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_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_trans … 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-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc new file mode 100644 index 000000000..6e8431959 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc @@ -0,0 +1,71 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predsnstar_3.ma". +include "basic_2/grammar/lpx_sn_tc.ma". +include "basic_2/reduction/lpr.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +definition lprs: relation3 genv lenv lenv ≝ + λG. TC … (lpr G). + +interpretation "parallel computation (local environment, sn variant)" + 'PRedSnStar G L1 L2 = (lprs G L1 L2). + +(* Basic eliminators ********************************************************) + +lemma lprs_ind: ∀G,L1. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L2. +#G #L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma lprs_ind_dx: ∀G,L2. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ➡* L2 → R L1. +#G #L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2. +/2 width=1/ qed. + +lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L. +/2 width=1/ qed. + +lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2. +/2 width=3/ qed. + +lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma lprs_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡* L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +lemma lprs_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡* ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lprs_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc new file mode 100644 index 000000000..315ee8f7a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predsnstaralt_3.ma". +include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* alternative definition *) +definition lprsa: relation3 genv lenv lenv ≝ + λG. lpx_sn … (cprs G). + +interpretation "parallel computation (local environment, sn variant) alternative" + 'PRedSnStarAlt G L1 L2 = (lprsa G L1 L2). + +(* Main properties on the alternative definition ****************************) + +theorem lprsa_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2. +/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-. + +(* Main inversion lemmas on the alternative definition **********************) + +theorem lprs_inv_lprsa: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡➡* L2. +/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-. + +(* Alternative eliminators **************************************************) + +lemma lprs_ind_alt: ∀G. ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc new file mode 100644 index 000000000..f03d3f0e8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/lpr_ldrop.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Properies on local environment slicing ***********************************) + +lemma lprs_ldrop_conf: ∀G. dropable_sn (lprs G). +/3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-. + +lemma ldrop_lprs_trans: ∀G. dedropable_sn (lprs G). +/3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-. + +lemma lprs_ldrop_trans_O1: ∀G. dropable_dx (lprs G). +/3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc new file mode 100644 index 000000000..1da198d4e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc @@ -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/reduction/lpr_lpr.ma". +include "basic_2/computation/lprs.ma". + +(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) + +(* Advanced properties ******************************************************) + +lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G). +/3 width=3 by TC_strip1, lpr_conf/ qed-. + +(* Main properties **********************************************************) + +theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G). +/3 width=3 by TC_confluent2, lpr_conf/ qed-. + +theorem lprs_trans: ∀G. Transitive … (lprs G). +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma new file mode 100644 index 000000000..824933fba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.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( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break [ term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyPRedSnStar $G $L1 $L2 $T $d }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma new file mode 100644 index 000000000..f8209e2f8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.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( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡* break [ term 46 h , break term 46 g , break term 46 T , break term 46 d ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyPRedSnStar $G $L1 $L2 $h $g $T $d }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma new file mode 100644 index 000000000..ba2210f69 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma @@ -0,0 +1,47 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llpx_sn_ldrop.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma llpx_sn_cpr_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → + ∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0). +#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ // +| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ +| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // + #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) + [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/ + | /3 width=4 by llpx_sn_bind_repl_O/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index d2703ad7c..77dce4631 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -43,8 +43,7 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → ] qed-. -lemma lleq_cpx_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. +lemma lleq_cpx_conf_sn: ∀h,g,G. s_r_confluent1 … (cpx h g G) (lleq 0). /3 width=6 by llpx_sn_cpx_conf, lift_mono, ex2_intro/ qed-. lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma index 38a83a760..36a97fc62 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma @@ -21,8 +21,7 @@ include "basic_2/reduction/cpx.ma". (* Note: lemma 1000 *) lemma llpx_sn_cpx_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → - ∀h,g,G,Ls,T1,T2. ⦃G, Ls⦄ ⊢ T1 ➡[h, g] T2 → - ∀Ld. llpx_sn R 0 T1 Ls Ld → llpx_sn R 0 T2 Ls Ld. + ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0). #R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 [ // | /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 94c114260..7c65dcfa9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -13,15 +13,15 @@ (**************************************************************************) include "basic_2/notation/relations/btpred_8.ma". -include "basic_2/relocation/fquq_alt.ma". -include "basic_2/reduction/lpx.ma". +include "basic_2/relocation/fquq.ma". +include "basic_2/reduction/llpx.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpb_fquq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2 | fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2 -| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1 +| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → fpb h g G1 L1 T1 G1 L2 T1 . interpretation @@ -36,5 +36,5 @@ lemma fpb_refl: ∀h,g. tri_reflexive … (fpb h g). lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄. /3 width=1 by fpb_cpx, cpr_cpx/ qed. -lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpb_lpx, lpr_lpx/ qed. +lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +/3 width=1 by fpb_lpx, llpr_llpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma index d61a11ae0..158b6b1d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/aaa_fqus.ma". -include "basic_2/reduction/lpx_aaa.ma". +include "basic_2/reduction/llpx_aaa.ma". include "basic_2/reduction/fpb.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -23,5 +23,5 @@ include "basic_2/reduction/fpb.ma". lemma aaa_fpb_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ∀A1. ⦃G1, L1⦄ ⊢ T1 ⁝ A1 → ∃A2. ⦃G2, L2⦄ ⊢ T2 ⁝ A2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=6 by aaa_lpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ +/3 width=6 by aaa_llpx_conf, aaa_cpx_conf, aaa_fquq_conf, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma index a19534b4a..0ca90bae4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/relocation/llpx_sn_ldrop.ma". include "basic_2/relocation/fquq_alt.ma". include "basic_2/reduction/cpr_lift.ma". +include "basic_2/reduction/cpr_llpx_sn.ma". include "basic_2/reduction/llpr.ma". (* LAZY SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ************************) @@ -47,6 +47,11 @@ lemma llpr_bind_repl_O: ∀I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[T, 0] ∀J,W1,W2. ⦃G, L1⦄ ⊢ ➡[W1, 0] L2 → ⦃G, L1⦄ ⊢ W1 ➡ W2 → ⦃G, L1.ⓑ{J}W1⦄ ⊢ ➡[T, 0] L2.ⓑ{J}W2. /2 width=4 by llpx_sn_bind_repl_O/ qed-. +(* Advanced properties ******************************************************) + +lemma llpr_cpr_conf: ∀G. s_r_confluent1 … (cpr G) (llpr G 0). +/3 width=10 by llpx_sn_cpr_conf, cpr_inv_lift1, cpr_lift/ qed-. + (* Properties on context-sensitive parallel reduction for terms *************) lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma index 925765be8..4e5b9e2be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma @@ -300,7 +300,7 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=2 by ldrop_ /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. -theorem cpr_conf_llpr: ∀G. llpx_sn_confluent (cpr G) (cpr G). +theorem cpr_conf_llpr: ∀G. llpx_sn_confluent2 (cpr G) (cpr G). #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 … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma new file mode 100644 index 000000000..7c0949133 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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/aaa_lift.ma". +include "basic_2/static/lsuba_aaa.ma". +include "basic_2/reduction/llpx_ldrop.ma". + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties on atomic arity assignment for terms **************************) + +(* Note: lemma 500 *) +lemma aaa_cpx_llpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #g #L1 #k #X #H elim (cpx_inv_sort1 … H) -H // * // +| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 + elim (cpx_inv_lref1 … H) -H + [ #H destruct + elim (llpx_inv_lref_ge_sn … HL12 … HLK1) -L1 /3 width=6 by aaa_lref/ + | * #J #Y #Z #V2 #H #HV12 #HV2 + lapply (ldrop_mono … H … HLK1) -H #H destruct + elim (llpx_inv_lref_ge_sn … HL12 … HLK1) -L1 /3 width=8 by aaa_lift, ldrop_fwd_drop2/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_bind_O … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_abbr1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=4 by llpx_bind_repl_O, aaa_abbr/ + | #T2 #HT12 #HT2 #H destruct -IHV1 /3 width=8 by aaa_inv_lift, ldrop_drop/ + ] +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_bind_O … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct + /4 width=4 by llpx_bind_repl_O, aaa_abst/ +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_flat … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_appl1 … H) -H * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3 by aaa_appl/ + | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct + lapply (IHV1 … HV12 … HV1) -IHV1 -HV12 #HV2 + lapply (IHT1 (ⓛ{b}W2.U2) … HT1) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct + /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ + | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct + lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by ldrop_drop/ #HV2 + lapply (IHT1 (ⓓ{b}W2.U2) … HT1) -IHT1 /2 width=1 by cpx_bind/ -L1 #H + elim (aaa_inv_abbr … H) -H /3 width=3 by aaa_abbr, aaa_appl/ + ] +| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 + elim (llpx_inv_flat … HL12) -HL12 #HV1 #HT1 + elim (cpx_inv_cast1 … H) -H + [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by aaa_cast/ + | -IHV1 /2 width=1 by/ + | -IHT1 /2 width=1 by/ + ] +] +qed-. + +lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/2 width=7 by aaa_cpx_llpx_conf/ qed-. + +lemma aaa_llpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/2 width=7 by aaa_cpx_llpx_conf/ qed-. + +lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. + +lemma aaa_llpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. +/3 width=5 by aaa_llpx_conf, llpr_llpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma index 9b7d295d3..0b9d88b99 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma @@ -54,8 +54,7 @@ lemma llpx_fwd_bind_O_dx: ∀h,g,a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{ (* Advanced properties ******************************************************) -lemma llpx_cpx_conf: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g, T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T2, 0] L2. +lemma llpx_cpx_conf: ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx h g G 0). /3 width=10 by llpx_sn_cpx_conf, cpx_inv_lift1, cpx_lift/ qed-. (* Inversion lemmas on relocation *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma new file mode 100644 index 000000000..bc8619d66 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpx_lleq.ma". +include "basic_2/reduction/llpx.ma". + +(* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_llpx_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L.⦃G, L2⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L. +/3 width=3 by lleq_cpx_trans, lleq_llpx_sn_trans/ qed-. + +lemma lleq_llpx_conf: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L.⦃G, L1⦄ ⊢ ➡[h, g, T, d] L → ⦃G, L2⦄ ⊢ ➡[h, g, T, d] L. +/3 width=3 by lleq_cpx_trans, lleq_llpx_sn_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma index cdca16bb5..91b20e720 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -59,6 +59,17 @@ elim (leq_ldrop_trans_be … (leq_sym … HL12) … HLK1) // -L1 -Hdi -Hide /3 width=3 by leq_sym, ex2_intro/ qed-. +lemma ldrop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i → + ∃∃L2. L1 ≃[0, i] L2 & ⇩[i] L2 ≡ K2. +#K2 #i @(nat_ind_plus … i) -i +[ /3 width=3 by leq_O2, ex2_intro/ +| #i #IHi #Y #Hi elim (ldrop_O1_lt Y 0) // + #I #L1 #V #H lapply (ldrop_inv_O2 … H) -H #H destruct + normalize in Hi; elim (IHi L1) -IHi + /3 width=5 by ldrop_drop, leq_pair, injective_plus_l, ex2_intro/ +] +qed-. + lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). #R #HR #L1 #K1 #s #d #e #HLK1 #K2 #H elim H -K2 [ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 @@ -70,7 +81,7 @@ qed-. (* Inversion lemmas on equivalence ******************************************) -lemma ldrop_O_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2. +lemma ldrop_O1_inj: ∀i,L1,L2,K. ⇩[i] L1 ≡ K → ⇩[i] L2 ≡ K → L1 ≃[i, ∞] L2. #i @(nat_ind_plus … i) -i [ #L1 #L2 #K #H <(ldrop_inv_O2 … H) -K #H <(ldrop_inv_O2 … H) -L1 // | #i #IHi * [2: #L1 #I1 #V1 ] * [2,4: #L2 #I2 #V2 ] #K #HLK1 #HLK2 // diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma index 904a86c10..0df9690ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma @@ -16,9 +16,9 @@ include "basic_2/relocation/llpx_sn.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) -definition llpx_sn_confluent: relation (lenv→relation term) ≝ λR1,R2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. llpx_sn R1 0 T0 L0 L1 → ∀L2. llpx_sn R2 0 T0 L0 L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +definition llpx_sn_confluent2: relation (lenv→relation term) ≝ λR1,R2. + ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. llpx_sn R1 0 T0 L0 L1 → ∀L2. llpx_sn R2 0 T0 L0 L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. -(* Note: we miss llpx_sn_conf and derivatives: lpr_conf *) +(* Note: we miss llpx_sn_conf and derivatives: lpr_conf lprs_conf *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/etc/lib/star.etc b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/star.etc new file mode 100644 index 000000000..fb4d9c3e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/etc/lib/star.etc @@ -0,0 +1,31 @@ +lemma TC_case_sn: ∀A,R. reflexive A R → + ∀a1,a2. TC … R a1 a2 → ∃∃a. R a1 a & TC … R a a2. +#A #R #HR #a1 #a2 #H @(TC_ind_dx … a1 H) -a1 +[ /3 width=3 by inj, ex2_intro/ +| #a1 #a0 #Ha10 #Ha02 #_ /2 width=3 by ex2_intro/ (**) (* auto fails withput #_ *) +] +qed-. + +lemma TC_case_dx: ∀A,R. reflexive A R → + ∀a1,a2. TC … R a1 a2 → ∃∃a. TC … R a1 a & R a a2. +#A #R #HR #a1 #a2 #H @(TC_ind … a2 H) -a2 +[ /3 width=3 by inj, ex2_intro/ +| #a0 #a2 #Ha10 #Ha02 #_ /2 width=3 by ex2_intro/ (**) (* auto fails withput #_ *) +] +qed-. + +definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. + +definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. + +lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S. +#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] +#T #T2 #_ #HT2 #IHT1 #L1 #HL12 +lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +qed-. + +lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S). +#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma index 8cfdf349e..50fda9065 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -40,21 +40,24 @@ definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝ definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. -definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. +definition s_r_transitive: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → LTC … R1 L1 T1 T2. -definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. +definition s_rs_transitive: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → LTC … R1 L1 T1 T2. + +definition s_r_confluent1: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2. + ∀L1,T1,T2. R1 L1 T1 T2 → ∀L2. R2 T1 L1 L2 → R2 T2 L1 L2. lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 → ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & TC … R1 a2 a. #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 [ #a1 #Ha01 #a2 #Ha02 - elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ + elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 - elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5/ + elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5 by step, ex2_intro/ ] qed. @@ -63,10 +66,10 @@ lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 → ∃∃a. TC … R2 a1 a & R1 a2 a. #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 [ #a2 #Ha02 #a1 #Ha01 - elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ + elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01 elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0 - elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3/ + elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3 by step, ex2_intro/ ] qed. @@ -74,10 +77,10 @@ lemma TC_confluent2: ∀A,R1,R2. confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2). #A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 [ #a1 #Ha01 #a2 #Ha02 - elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/ + elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 - elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5/ + elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5 by step, ex2_intro/ ] qed. @@ -86,10 +89,10 @@ lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 → ∃∃a. R2 a1 a & TC … R1 a a2. #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 [ #a0 #Ha10 #a2 #Ha02 - elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ + elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a0 #_ #Ha0 #IHa #a2 #Ha02 elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02 - elim (IHa … Ha0) -a /4 width=5/ + elim (IHa … Ha0) -a /4 width=5 by step, ex2_intro/ ] qed. @@ -98,10 +101,10 @@ lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 → ∃∃a. TC … R2 a1 a & R1 a a2. #A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 [ #a2 #Ha02 #a1 #Ha10 - elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ + elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a2 #_ #Ha02 #IHa #a1 #Ha10 elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0 - elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3/ + elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3 by step, ex2_intro/ ] qed. @@ -109,10 +112,10 @@ lemma TC_transitive2: ∀A,R1,R2. transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2). #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 [ #a0 #Ha10 #a2 #Ha02 - elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/ + elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3 by inj, ex2_intro/ | #a #a0 #_ #Ha0 #IHa #a2 #Ha02 elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02 - elim (IHa … Ha0) -a /4 width=5/ + elim (IHa … Ha0) -a /4 width=5 by step, ex2_intro/ ] qed. @@ -130,15 +133,15 @@ inductive SN (A) (R,S:relation A): predicate A ≝ lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. #A #R #S #a1 #Ha1 @SN_intro #a2 #HRa12 #HSa12 -elim HSa12 -HSa12 /2 width=1/ +elim HSa12 -HSa12 /2 width=1 by/ qed. lemma SN_to_NF: ∀A,R,S. NF_dec A R S → ∀a1. SN A R S a1 → ∃∃a2. star … R a1 a2 & NF A R S a2. #A #R #S #HRS #a1 #H elim H -a1 -#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3/ -* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3/ +#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3 by srefl, ex2_intro/ +* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3 by star_compl, ex2_intro/ qed-. definition NF_sn: ∀A. relation A → relation A → predicate A ≝ @@ -151,23 +154,28 @@ inductive SN_sn (A) (R,S:relation A): predicate A ≝ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. #A #R #S #a2 #Ha2 @SN_sn_intro #a1 #HRa12 #HSa12 -elim HSa12 -HSa12 /2 width=1/ +elim HSa12 -HSa12 /2 width=1 by/ qed. lemma LTC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S. -#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] +#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 /3 width=3 by inj/ #T #T2 #_ #HT2 #IHT1 #L1 #HL12 -lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3 by step/ qed-. -lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S. -#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] -#T #T2 #_ #HT2 #IHT1 #L1 #HL12 -lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +lemma s_r_conf1_LTC1: ∀A,B,S,R. s_r_confluent1 A B S R → s_r_confluent1 A B (LTC … S) R. +#A #B #S #R #HSR #L1 #T1 #T2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3 by/ +qed-. + +lemma s_r_trans_LTC1: ∀A,B,S,R. s_r_confluent1 A B S R → + s_r_transitive A B S R → s_rs_transitive A B S R. +#A #B #S #R #H1SR #H2SR #L2 #T1 #T2 #H @(TC_ind_dx … T1 H) -T1 /2 width=3 by/ +#T1 #T #HT1 #_ #IHT2 #L1 #HL12 lapply (H2SR … HT1 … HL12) -H2SR -HT1 +/4 width=5 by s_r_conf1_LTC1, trans_TC/ qed-. -lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S). -#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/ +lemma s_r_trans_LTC2: ∀A,B,S,R. s_rs_transitive A B S R → s_r_transitive A B S (LTC … R). +#A #B #S #R #HSR #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /3 width=3 by inj/ qed-. (* relations on unboxed pairs ***********************************************) @@ -177,9 +185,9 @@ lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R → ∃∃a,b. bi_TC … R a1 b1 a b & R a2 b2 a b. #A #B #R #HR #a0 #a1 #b0 #b1 #H01 #a2 #b2 #H elim H -a2 -b2 [ #a2 #b2 #H02 - elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4/ + elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4 by ex2_2_intro, bi_inj/ | #a2 #b2 #a3 #b3 #_ #H23 * #a #b #H1 #H2 - elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4/ + elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4 by ex2_2_intro, bi_step/ ] qed. @@ -187,10 +195,10 @@ lemma bi_TC_confluent: ∀A,B,R. bi_confluent A B R → bi_confluent A B (bi_TC … R). #A #B #R #HR #a0 #a1 #b0 #b1 #H elim H -a1 -b1 [ #a1 #b1 #H01 #a2 #b2 #H02 - elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4/ + elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4 by ex2_2_intro, bi_inj/ | #a1 #b1 #a3 #b3 #_ #H13 #IH #a2 #b2 #H02 elim (IH … H02) -a0 -b0 #a0 #b0 #H10 #H20 - elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/ + elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7 by ex2_2_intro, bi_step/ ] qed. @@ -198,7 +206,7 @@ lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B. ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → R a1 b1 a2 b2 ∨ ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2. -#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/ +#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4 by ex2_2_intro, or_intror/ qed-. lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. @@ -206,8 +214,8 @@ lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. R a1 b1 a2 b2 ∨ ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2. #A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1 -[ /2 width=1/ -| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/ +[ /2 width=1 by or_introl/ +| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4 by ex2_2_intro, or_intror/ (**) (* auto fails without #_ *) ] qed-. @@ -218,29 +226,29 @@ definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ ∧∧ a1 = a2 & b1 = b2 & c1 = c2. lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). -/3 width=1/ qed. +/3 width=1 by and3_intro, or_intror/ qed. definition tri_star: ∀A,B,C,R. tri_relation A B C ≝ λA,B,C,R. tri_RC A B C (tri_TC … R). lemma tri_star_tri_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_star … R). -/2 width=1/ qed. +/2 width=1 by/ qed. lemma tri_TC_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. tri_TC A B C R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. -/2 width=1/ qed. +/2 width=1 by or_introl/ qed. lemma tri_R_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. -/3 width=1/ qed. +/3 width=1 by tri_TC_to_tri_star, tri_inj/ qed. lemma tri_star_strap1: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. tri_star A B C R a1 b1 c1 a b c → R a b c a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ +[ /3 width=5 by tri_TC_to_tri_star, tri_step/ +| * #H1 #H2 #H3 destruct /2 width=1 by tri_R_to_tri_star/ ] qed. @@ -248,8 +256,8 @@ lemma tri_star_strap2: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. R a1 b1 c1 a b c → tri_star A B C R a b c a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ +[ /3 width=5 by tri_TC_to_tri_star, tri_TC_strap/ +| * #H1 #H2 #H3 destruct /2 width=1 by tri_R_to_tri_star/ ] qed. @@ -258,8 +266,8 @@ lemma tri_star_to_tri_TC_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. tri_TC A B C R a b c a2 b2 c2 → tri_TC A B C R a1 b1 c1 a2 b2 c2. #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * -[ /2 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ +[ /2 width=5 by tri_TC_transitive/ +| * #H1 #H2 #H3 destruct /2 width=1 by/ ] qed. @@ -268,15 +276,15 @@ lemma tri_TC_to_tri_star_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. tri_star A B C R a b c a2 b2 c2 → tri_TC A B C R a1 b1 c1 a2 b2 c2. #A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * -[ /2 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ +[ /2 width=5 by tri_TC_transitive/ +| * #H1 #H2 #H3 destruct /2 width=1 by/ ] qed. lemma tri_tansitive_tri_star: ∀A,B,C,R. tri_transitive A B C (tri_star … R). #A #B #C #R #a1 #a #b1 #b #c1 #c #H #a2 #b2 #c2 * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ +[ /3 width=5 by tri_star_to_tri_TC_to_tri_TC, tri_TC_to_tri_star/ +| * #H1 #H2 #H3 destruct /2 width=1 by/ ] qed. @@ -284,7 +292,7 @@ lemma tri_star_ind: ∀A,B,C,R,a1,b1,c1. ∀P:relation3 A B C. P a1 b1 c1 → (∀a,a2,b,b2,c,c2. tri_star … R a1 b1 c1 a b c → R a b c a2 b2 c2 → P a b c → P a2 b2 c2) → ∀a2,b2,c2. tri_star … R a1 b1 c1 a2 b2 c2 → P a2 b2 c2. #A #B #C #R #a1 #b1 #c1 #P #H #IH #a2 #b2 #c2 * -[ #H12 elim H12 -a2 -b2 -c2 /2 width=6/ -H /3 width=6/ +[ #H12 elim H12 -a2 -b2 -c2 /3 width=6 by tri_TC_to_tri_star/ | * #H1 #H2 #H3 destruct // ] qed-. @@ -293,7 +301,7 @@ lemma tri_star_ind_dx: ∀A,B,C,R,a2,b2,c2. ∀P:relation3 A B C. P a2 b2 c2 → (∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c → tri_star … R a b c a2 b2 c2 → P a b c → P a1 b1 c1) → ∀a1,b1,c1. tri_star … R a1 b1 c1 a2 b2 c2 → P a1 b1 c1. #A #B #C #R #a2 #b2 #c2 #P #H #IH #a1 #b1 #c1 * -[ #H12 @(tri_TC_ind_dx … a1 b1 c1 H12) -a1 -b1 -c1 /2 width=6/ -H /3 width=6/ +[ #H12 @(tri_TC_ind_dx … a1 b1 c1 H12) -a1 -b1 -c1 /3 width=6 by tri_TC_to_tri_star/ | * #H1 #H2 #H3 destruct // ] qed-. -- 2.39.2