From 78b27990925c54b2a34cff609fc9bcfbeb6b48f3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 Apr 2014 13:57:19 +0000 Subject: [PATCH] commit completed: - pointwise ordinary reduction: we park the "lazy" version and we restore the "full" version annotating the source with our understandings - pointwise extended reduction: we use the "lazy" version for now a better understanding of the relationship between the "full" version and the "lazy" version (lpx_sn_llpx_sn) allows to link the two --- .../basic_2/computation/cpds_cpds.ma | 2 +- .../basic_2/computation/cprs_cprs.ma | 69 +++--- .../basic_2/computation/cprs_lift.ma | 7 +- .../basic_2/computation/cpxs_lleq.ma | 14 +- .../lambdadelta/basic_2/computation/fpbs.ma | 10 +- .../basic_2/computation/fpbs_fpbs.ma | 8 - .../basic_2/computation/fpbs_lift.ma | 1 + .../basic_2/computation/fpbs_lpr.ma | 36 +++ .../lambdadelta/basic_2/computation/fpbu.ma | 6 +- .../basic_2/computation/fpbu_lleq.ma | 2 +- .../lambdadelta/basic_2/computation/llpxs.ma | 4 - .../basic_2/computation/llpxs_aaa.ma | 5 +- .../basic_2/computation/llpxs_lprs.ma | 25 +++ .../lpx_sn/lprs.etc => computation/lprs.ma} | 0 .../lprs_alt.etc => computation/lprs_alt.ma} | 0 .../lprs_cprs.ma} | 59 +++-- .../lprs_ldrop.ma} | 0 .../lprs_lprs.ma} | 0 .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 1 + .../basic_2/dynamic/snv_lsstas_lpr.ma | 1 + .../basic_2/equivalence/cpcs_cpcs.ma | 8 +- .../basic_2/etc/llpr/cpcs_cpcs.etc | 205 ++++++++++++++++++ .../basic_2/etc/llpr/cprs_cprs.etc | 166 ++++++++++++++ .../basic_2/etc/llpr/cprs_lift.etc | 63 ++++++ .../llpr/lazypredsn_5.etc} | 0 .../llpr/lazypredsnstar_5.etc} | 0 .../{reduction/llpr.ma => etc/llpr/llpr.etc} | 0 .../llpr_ldrop.ma => etc/llpr/llpr_ldrop.etc} | 6 +- .../llpr_llpr.ma => etc/llpr/llpr_llpr.etc} | 0 .../llprs.ma => etc/llpr/llprs.etc} | 0 .../llprs_cprs.ma => etc/llpr/llprs_cprs.etc} | 40 +++- .../llpr/llprs_llprs.etc} | 0 .../llpr/llpx_sn_llpx_sn.etc} | 0 .../lpx_sn/lpx_sn.etc => grammar/lpx_sn.ma} | 0 .../lpx_sn_lpx_sn.ma} | 0 .../lpx_sn_tc.etc => grammar/lpx_sn_tc.ma} | 10 +- .../contribs/lambdadelta/basic_2/names.txt | 1 - .../relations/predsn_3.ma} | 0 .../relations/predsnstar_3.ma} | 0 .../relations/predsnstaralt_3.ma} | 0 .../basic_2/reduction/cpr_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 10 +- .../basic_2/reduction/cpx_llpx_sn.ma | 2 +- .../lambdadelta/basic_2/reduction/fpb.ma | 5 +- .../lambdadelta/basic_2/reduction/llpx.ma | 5 +- .../lambdadelta/basic_2/reduction/llpx_aaa.ma | 5 +- .../basic_2/reduction/llpx_ldrop.ma | 2 +- .../lambdadelta/basic_2/reduction/llpx_lpr.ma | 25 +++ .../{etc/lpx_sn/lpr.etc => reduction/lpr.ma} | 2 +- .../lpr_ldrop.etc => reduction/lpr_ldrop.ma} | 0 .../lpr_lpr.etc => reduction/lpr_lpr.ma} | 4 +- .../ldrop_lpx_sn.ma} | 26 +++ .../basic_2/relocation/llpx_sn_lpx_sn.ma | 38 ++++ .../basic_2/static/ssta_llpx_sn.ma | 43 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 49 ++--- 56 files changed, 806 insertions(+), 163 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lprs.etc => computation/lprs.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lprs_alt.etc => computation/lprs_alt.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lprs_cprs.etc => computation/lprs_cprs.ma} (74%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lprs_ldrop.etc => computation/lprs_ldrop.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lprs_lprs.etc => computation/lprs_lprs.ma} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cpcs_cpcs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_cprs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_lift.etc rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazypredsn_5.ma => etc/llpr/lazypredsn_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazypredsnstar_5.ma => etc/llpr/lazypredsnstar_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpr.ma => etc/llpr/llpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpr_ldrop.ma => etc/llpr/llpr_ldrop.etc} (95%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/llpr_llpr.ma => etc/llpr/llpr_llpr.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llprs.ma => etc/llpr/llprs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llprs_cprs.ma => etc/llpr/llprs_cprs.etc} (68%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/llprs_llprs.ma => etc/llpr/llprs_llprs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_llpx_sn.ma => etc/llpr/llpx_sn_llpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_sn.etc => grammar/lpx_sn.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_sn_lpx_sn.etc => grammar/lpx_sn_lpx_sn.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpx_sn_tc.etc => grammar/lpx_sn_tc.ma} (92%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsn_3.etc => notation/relations/predsn_3.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsnstar_3.etc => notation/relations/predsnstar_3.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/predsnstaralt_3.etc => notation/relations/predsnstaralt_3.ma} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpr.etc => reduction/lpr.ma} (98%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpr_ldrop.etc => reduction/lpr_ldrop.ma} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/lpr_lpr.etc => reduction/lpr_lpr.ma} (99%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lpx_sn/ldrop_lpx_sn.etc => relocation/ldrop_lpx_sn.ma} (76%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma index 60b490393..ef1e56d90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". -include "basic_2/computation/llprs_cprs.ma". +include "basic_2/computation/lprs_cprs.ma". include "basic_2/computation/cpxs_cpxs.ma". include "basic_2/computation/cpds.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index a85488cdf..809bf173c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/llpr_llpr.ma". +include "basic_2/reduction/lpr_lpr.ma". include "basic_2/computation/cprs_lift.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -22,7 +22,7 @@ include "basic_2/computation/cprs_lift.ma". (* Basic_1: was: pr3_t *) (* Basic_1: includes: pr1_t *) theorem cprs_trans: ∀G,L. Transitive … (cprs G L). -normalize /2 width=3 by trans_TC/ qed-. +normalize /2 width=3 by trans_TC/ qed-. (* Basic_1: was: pr3_confluence *) (* Basic_1: includes: pr1_confluence *) @@ -61,14 +61,14 @@ qed. theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 +#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H @(cprs_ind … H) -W2 /3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/ qed. theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 +#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(cprs_ind_dx … H) -V1 /3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/ qed. @@ -91,9 +91,9 @@ lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12 lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 - /5 width=5 by cprs_flat_dx, cpr_cprs, cprs_bind, lsubr_abst, ex2_3_intro, or3_intro1/ + /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_abst, ex2_3_intro, or3_intro1/ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct - @or3_intro2 @(ex4_5_intro … HV2 HT10) /3 width=3 by cprs_flat_sn, cprs_strap1, cpr_cprs, cprs_bind/ (**) (* full auto is too slow 11s *) + /5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/ ] | /4 width=9 by cprs_strap1, or3_intro1, ex2_3_intro/ | /4 width=11 by cprs_strap1, or3_intro2, ex4_5_intro/ @@ -104,63 +104,52 @@ qed-. (* Basic_1: was just: pr3_pr2_pr2_t *) (* Basic_1: includes: pr3_pr0_pr2_t *) -lemma llpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (llpr G 0). +lemma lpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lpr G). #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 [ /2 width=3 by/ | #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (llpr_inv_lref_ge_dx … HL12 … HLK2) -L2 - /5 width=7 by cprs_delta, cprs_strap2, llpr_cpr_conf/ -| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (llpr_inv_bind_O … HL12) -HL12 /4 width=1 by cprs_bind/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 - elim (llpr_inv_flat … HL12) -HL12 /3 width=1 by cprs_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 - elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_zeta/ -| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12 - elim (llpr_inv_flat … HL12) /3 width=1 by cprs_tau/ -| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12 - elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12 - elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_beta/ -| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 - elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12 - elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_theta/ + elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H + elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct + /4 width=6 by cprs_strap2, cprs_delta/ +|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/ +|4,6: /3 width=1 by cprs_flat, cprs_tau/ +|5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/ ] qed-. lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -/4 width=9 by llpr_cpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed. +/4 width=5 by lpr_cpr_trans, cprs_bind_dx, lpr_pair/ qed. (* Advanced properties ******************************************************) (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) -lemma cprs_llpr_trans: ∀G. s_rs_transitive … (cpr G) (llpr G 0). -/3 width=6 by llpr_cpr_trans, llpr_cpr_conf, s_r_trans_LTC1/ qed-. +lemma lpr_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lpr G). +#G @s_r_trans_LTC1 /2 width=3 by lpr_cpr_trans/ (**) (* full auto fails *) +qed-. (* Basic_1: was: pr3_strip *) (* Basic_1: includes: pr1_strip *) lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L). normalize /4 width=3 by cpr_conf, TC_strip1/ qed-. -lemma cprs_llpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. -#G #L0 #T0 #T1 #H @(cprs_ind_dx … T0 H) -T0 /2 width=3 by ex2_intro/ -#T0 #T #HT0 #_ #IHT1 #L1 #HL01 -elim (IHT1 … L1) /2 by llpr_cpr_conf/ -IHT1 #T2 #HT12 #HT2 -elim (llpr_cpr_conf_dx … HT0 … HL01) -L0 #T3 #HT03 #HT3 -elim (cprs_strip … HT2 … HT3) -T +lemma cprs_lpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #H @(cprs_ind … H) -T1 /2 width=3 by ex2_intro/ +#T #T1 #_ #HT1 #IHT0 #L1 #HL01 elim (IHT0 … HL01) +#T2 #HT2 #HT02 elim (lpr_cpr_conf_dx … HT1 … HL01) -L0 +#T3 #HT3 #HT13 elim (cprs_strip … HT2 … HT3) -T /4 width=5 by cprs_strap2, cprs_strap1, ex2_intro/ qed-. -lemma cprs_llpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 → - ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. -#G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cprs_llpr_conf_dx … HT01 … HL01) -/4 width=5 by cprs_llpr_trans, cprs_llpr_conf, ex2_intro/ +lemma cprs_lpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 +/3 width=3 by lpr_cprs_trans, ex2_intro/ qed-. lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -/4 width=9 by cprs_llpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed. +/4 width=5 by lpr_cprs_trans, cprs_bind_dx, lpr_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma index 27f0bb6e5..b883ad18e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/llpr_ldrop.ma". +include "basic_2/reduction/cpr_lift.ma". include "basic_2/computation/cprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -29,9 +29,6 @@ lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/ qed. -lemma cprs_llpr_conf: ∀G. s_r_confluent1 … (cprs G) (llpr G 0). -/3 width=5 by llpr_cpr_conf, s_r_conf1_LTC1/ qed-. - (* Advanced inversion lemmas ************************************************) (* Basic_1: was: pr3_gen_lref *) @@ -47,7 +44,7 @@ lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 → | * #K #V1 #T1 #HLK #HVT1 #HT1 lapply (ldrop_fwd_drop2 … HLK) #H0LK elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T - /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/ + /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma index 7a5666593..ce575a47b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma @@ -22,14 +22,18 @@ include "basic_2/computation/cpxs.ma". lemma lleq_cpxs_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. #h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1 -/4 width=6 by lleq_cpx_conf_dx, lleq_cpx_trans, cpxs_strap2/ +/4 width=6 by cpx_lleq_conf_dx, lleq_cpx_trans, cpxs_strap2/ qed-. -lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → +lemma cpxs_lleq_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → + ∀L1. L2 ⋕[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. +/3 width=3 by lleq_cpxs_trans, lleq_sym/ qed-. + +lemma cpxs_lleq_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. -#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/ +#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by cpx_lleq_conf_dx/ qed-. -lemma lleq_cpxs_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 → +lemma cpxs_lleq_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 → ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. -/4 width=6 by lleq_cpxs_conf_dx, lleq_sym/ qed-. +/4 width=6 by cpxs_lleq_conf_dx, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 361353ece..87d1d71d8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -79,14 +79,10 @@ qed. lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. /3 width=1 by cprs_cpxs, cpxs_fpbs/ qed. - -lemma llprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. +(* +lamma llprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. /3 width=1 by llprs_llpxs, llpxs_fpbs/ qed. - -lemma cpr_llpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 → - ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. -/4 width=5 by fpbs_strap1, llpr_fpb, cpr_fpb/ qed. - +*) lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma index 109dcda03..0a9f3af8c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -20,11 +20,3 @@ include "basic_2/computation/fpbs_lift.ma". theorem fpbs_trans: ∀h,g. tri_transitive … (fpbs h g). /2 width=5 by tri_TC_transitive/ qed-. - -(* Advanced properties ******************************************************) - -lemma cpr_llpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. - ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 → - ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → - ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. -/3 width=5 by fpbs_trans, cpr_llpr_fpbs, ssta_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index 70cabad47..8bcc50cd1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -23,6 +23,7 @@ lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. /3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. +(* Note: this should be moved *) lemma ssta_fpbs: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma new file mode 100644 index 000000000..34b60ad1d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lift.ma". +include "basic_2/reduction/llpx_lpr.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Properties on sn parallel reduction for local environments ***************) + +(* Note: this is used in the closure proof *) +(* Note: original proof: /4 width=5 by fpbs_strap1, lpr_fpb, cpr_fpb/ *) +(* Note: this should be moved *) +lemma cpr_lpr_fpbs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. +/5 width=5 by fpbs_strap1, cpr_fpb, fpb_llpx, lpr_llpx/ qed. + +(* Note: this is used in the closure proof *) +(* Note: this should be moved *) +lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. + ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → + ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. +/4 width=5 by fpbs_strap1, cpr_lpr_fpbs, ssta_cpx, fpb_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index 52c00a82b..4373c210e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -33,11 +33,11 @@ interpretation lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpbu_cpxs, cprs_cpxs/ qed. - -lemma llprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → (L1 ⋕[T, 0] L2 → ⊥) → +(* +lamma llprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → (L1 ⋕[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. /3 width=1 by fpbu_llpxs, llprs_llpxs/ qed. - +*) (* Basic forward lemmas *****************************************************) lemma fpbu_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma index a08672bc8..d1b1c9c94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma @@ -27,7 +27,7 @@ lemma lleq_fpbu_trans: ∀h,g,F,K1,K2,T. K1 ⋕[T, 0] K2 → #h #g #F #K1 #K2 #T #HT #G #L2 #U * -G -L2 -U [ #G #L2 #U #H2 elim (lleq_fqup_trans … H2 … HT) -K2 /3 width=3 by fpbu_fqup, ex2_intro/ -| /4 width=10 by fpbu_cpxs, lleq_cpxs_conf_sn, lleq_cpxs_trans, ex2_intro/ +| /4 width=10 by fpbu_cpxs, cpxs_lleq_conf_sn, lleq_cpxs_trans, ex2_intro/ | /5 width=3 by fpbu_llpxs, lleq_llpxs_trans, lleq_canc_sn, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma index 154c24f20..750d0b5b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma @@ -14,7 +14,6 @@ include "basic_2/notation/relations/lazypredsnstar_7.ma". include "basic_2/reduction/llpx.ma". -include "basic_2/computation/llprs.ma". (* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************) @@ -42,9 +41,6 @@ qed-. (* Basic properties *********************************************************) -lemma llprs_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2. -normalize /3 width=3 by llpr_llpx, monotonic_TC/ qed. - lemma llpx_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2. normalize /2 width=1 by inj/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma index f9b30323a..ededb03a2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma @@ -24,7 +24,8 @@ lemma aaa_llpxs_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → #h #g #G #L1 #T #A #HT #L2 #HL12 @(TC_Conf3 … (λL,A. ⦃G, L⦄ ⊢ T ⁝ A) … HT ? HL12) /2 width=5 by aaa_llpx_conf/ qed-. - -lemma aaa_llprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → +(* +lamma aaa_llprs_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡*[T, 0] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. /3 width=5 by aaa_llpxs_conf, llprs_llpxs/ qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma new file mode 100644 index 000000000..32d7bbc38 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/llpx_lpr.ma". +include "basic_2/computation/lprs.ma". +include "basic_2/computation/llpxs.ma". + +(* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************) + +(* Properties on sn parallel computation ************************************) + +(* Note: this should be moved *) +lemma lprs_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2. +normalize /3 width=3 by lpr_llpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_alt.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lprs_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma index 70345be5c..9ce393c43 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_cprs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_cprs.ma @@ -37,26 +37,25 @@ lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 → (* Properties on context-sensitive parallel computation for terms ***********) -lemma lprs_cpr_trans: ∀G. s_r_trans … (cpr G) (lprs G). -/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-. +lemma lprs_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lprs G). +/3 width=5 by s_r_trans_LTC2, lpr_cprs_trans/ qed-. (* Basic_1: was just: pr3_pr3_pr3_t *) -lemma lprs_cprs_trans: ∀G. s_rs_trans … (cpr G) (lprs G). -/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-. +(* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *) +lemma lprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (λ_. lprs G). +#G @s_r_to_s_rs_trans @s_r_trans_LTC2 +@s_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *) +qed-. lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. -#G #L0 #T0 #T1 #HT01 #L1 #H elim H -L1 -[ #L1 #HL01 - elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3 by ex2_intro/ -| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0 - elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12 - elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03 - elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3 - lapply (cprs_trans … HT03 … HT3) -T3 - lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3 by ex2_intro/ -] +#G #L0 #T0 #T1 #HT01 #L1 #H @(lprs_ind … H) -L1 /2 width=3 by ex2_intro/ +#L #L1 #_ #HL1 * #T #HT1 #HT0 -L0 +elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 +elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 +elim (cprs_conf … HT2 … HT3) -T +/3 width=5 by cprs_trans, ex2_intro/ qed-. lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → @@ -64,12 +63,13 @@ lemma lprs_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. /3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-. +(* Note: this can be proved on its own using lprs_ind_dx *) lemma lprs_cprs_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1 -lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3 by ex2_intro/ +elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 +/3 width=3 by lprs_cprs_trans, ex2_intro/ qed-. lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → @@ -80,9 +80,7 @@ lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 -lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1 by lprs_pair, cprs_bind/ -qed. +/4 width=5 by lprs_cprs_trans, lprs_pair, cprs_bind/ qed. (* Inversion lemmas on context-sensitive parallel computation for terms *****) @@ -93,15 +91,14 @@ lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 → #a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5 by ex3_2_intro/ #U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct elim (cpr_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct -lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 -lapply (cprs_strap1 … HV10 … HV02) -V0 -lapply (cprs_trans … HT10 … HT02) -T0 /2 width=5 by ex3_2_intro/ +lapply (lprs_cpr_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lprs_pair, cprs_trans, cprs_strap1, ex3_2_intro/ qed-. lemma cprs_inv_abst: ∀a,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 ∧ ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2. -#a #G #L #W1 #W2 #T1 #T2 #H -elim (cprs_inv_abst1 … H) -H #W #T #HW1 #HT1 #H destruct /2 width=1 by conj/ +#a #G #L #W1 #W2 #T1 #T2 #H elim (cprs_inv_abst1 … H) -H +#W #T #HW1 #HT1 #H destruct /2 width=1 by conj/ qed-. (* Basic_1: was pr3_gen_abbr *) @@ -115,16 +112,14 @@ lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → [ #V0 #T0 #HV10 #HT10 #H destruct elim (cpr_inv_abbr1 … HU02) -HU02 * [ #V2 #T2 #HV02 #HT02 #H destruct - lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1 by lprs_pair/ -HT02 #HT02 - lapply (cprs_strap1 … HV10 … HV02) -V0 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5 by ex3_2_intro, or_introl/ + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lprs_pair, cprs_trans, cprs_strap1, ex3_2_intro, or_introl/ | #T2 #HT02 #HUT2 - lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1 by lprs_pair/ -V0 #HT02 - lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3 by ex3_intro, or_intror/ + lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lprs_pair, cprs_trans, ex3_intro, or_intror/ ] -| #U1 #HTU1 #HU01 - elim (lift_total U2 0 1) #U #HU2 - lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 +| #U1 #HTU1 #HU01 elim (lift_total U2 0 1) + #U #HU2 lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lprs_lprs.etc rename to matita/matita/contribs/lambdadelta/basic_2/computation/lprs_lprs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index dbdbfd24f..d40cc3224 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". -include "basic_2/computation/fpbg_fpns.ma". +include "basic_2/computation/fpbg_fleq.ma". include "basic_2/equivalence/cpes_cpds.ma". include "basic_2/dynamic/snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 367312794..3634321be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/computation/fpbs_lpr.ma". include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_snv.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index 9213b4d57..4e6d1b33c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/computation/cpds_cpds.ma". +include "basic_2/computation/fpbs_lpr.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lsstas.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma index cf1c5d95f..8a5e0e323 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma @@ -23,7 +23,7 @@ include "basic_2/equivalence/cpcs_cprs.ma". lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. #G #L #T1 #T2 #H @(cpcs_ind … H) -T2 -[ /3 width=3/ +[ /3 width=3 by ex2_intro/ | #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ | /3 width=5 by cprs_strap2, ex2_intro/ @@ -106,9 +106,12 @@ qed-. (* Basic_1: was: pc3_wcpr0_t *) (* Basic_1: note: pc3_wcpr0_t should be renamed *) +(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *) lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -/3 width=5 by lprs_cprs_conf, lpr_lprs/ qed-. +#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. (* Basic_1: was only: pc3_pr0_pr2_t *) (* Basic_1: note: pc3_pr0_pr2_t should be renamed *) @@ -161,6 +164,7 @@ lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ (* More inversion lemmas ****************************************************) +(* Note: there must be a proof suitable for llpr *) lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2. #a1 #a2 #G #L #W1 #W2 #T1 #T2 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cpcs_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cpcs_cpcs.etc new file mode 100644 index 000000000..d31f9cacd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cpcs_cpcs.etc @@ -0,0 +1,205 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/llprs_cprs.ma". +include "basic_2/conversion/cpc_cpc.ma". +include "basic_2/equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. +#G #L #T1 #T2 #H @(cpcs_ind … H) -T2 +[ /3 width=3 by ex2_intro/ +| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 + [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ + | /3 width=5 by cprs_strap2, ex2_intro/ + ] +] +qed-. + +(* Basic_1: was: pc3_gen_sort *) +lemma cpcs_inv_sort: ∀G,L,k1,k2. ⦃G, L⦄ ⊢ ⋆k1 ⬌* ⋆k2 → k1 = k2. +#G #L #k1 #k2 #H elim (cpcs_inv_cprs … H) -H +#T #H1 >(cprs_inv_sort1 … H1) -T #H2 +lapply (cprs_inv_sort1 … H2) -L #H destruct // +qed-. + +lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T → + ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +#a #G #L #W1 #T1 #T #H +elim (cpcs_inv_cprs … H) -H #X #H1 #H2 +elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct +/3 width=6 by cprs_bind, ex2_2_intro/ +qed-. + +lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 → + ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-. + +(* Basic_1: was: pc3_gen_sort_abst *) +lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,k. ⦃G, L⦄ ⊢ ⋆k ⬌* ⓛ{a}W.T → ⊥. +#a #G #L #W #T #k #H +elim (cpcs_inv_cprs … H) -H #X #H1 +>(cprs_inv_sort1 … H1) -X #H2 +elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct +qed-. + +(* Basic_1: was: pc3_gen_lift *) +lemma cpcs_inv_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → + ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2. +#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 +elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 +elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 +elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU +>(lift_inj … HXU … HTU) -X -U -d -e /2 width=3 by cprs_div/ +qed-. + +(* Advanced properties ******************************************************) + +lemma llpr_cpcs_trans: ∀G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ ➡[T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 → + ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #T1 #T2 #HT1 #HT2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, cprs_llpr_trans/ +qed-. + +lemma llprs_cpcs_trans: ∀G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ ➡*[T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡*[T2, 0] L2 → + ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #T1 #T2 #HT1 #HT2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, llprs_cprs_trans/ +qed-. + +lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cpr_cprs_div/ +qed-. + +lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_cpr_div/ +qed-. + +lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was: pc3_wcpr0_t *) +(* Basic_1: note: pc3_wcpr0_t should be renamed *) +lemma llpr_cprs_conf: ∀G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡[T1, 0] L2 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #T1 #HL12 #T2 #HT12 elim (cprs_llpr_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was only: pc3_pr0_pr2_t *) +(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) +lemma llpr_cpr_conf: ∀G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡[T1, 0] L2 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +/3 width=5 by llpr_cprs_conf, cpr_cprs/ qed-. + +(* Basic_1: was only: pc3_thin_dx *) +lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. +#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HV12) -HV12 +elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_flat, cprs_div/ +qed. + +lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. +/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. + +lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2. +#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, cprs_bind/ +qed. + +lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. +#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 +/3 width=5 by cprs_div, cprs_bind/ +qed. + +lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → + ∀L2. L2 ⊑ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, lsubr_cprs_trans/ +qed-. + +(* Basic_1: was: pc3_lift *) +lemma cpcs_lift: ∀G,L,K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 → + ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. +#G #L #K #s #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +elim (lift_total T d e) /3 width=12 by cprs_div, cprs_lift/ +qed. + +lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 → + ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0. +#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-. + +(* More inversion lemmas ****************************************************) + +axiom cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2. +(* +#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct +elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct +lapply (llprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by llprs_pair/ -HT2 #HT2 +lapply (llprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by llprs_pair/ -HT2 #HT2 +/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ +qed-. +*) +lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2. +#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 +#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ +qed-. + +(* Main properties **********************************************************) + +(* Basic_1: was pc3_t *) +theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. + +theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. + +theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. + +lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → + ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. + +lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → + ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. + +(* Basic_1: was: pc3_wcpr0 *) +lemma llpr_cpcs_conf: ∀G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ ➡[T1, 0] L2 → ⦃G, L1⦄ ⊢ ➡[T2, 0] L2 → + ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #T1 #T2 #HT1 #HT2 #H elim (cpcs_inv_cprs … H) -H +/3 width=5 by cpcs_canc_dx, llpr_cprs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_cprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_cprs.etc new file mode 100644 index 000000000..a85488cdf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_cprs.etc @@ -0,0 +1,166 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llpr_llpr.ma". +include "basic_2/computation/cprs_lift.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: pr3_t *) +(* Basic_1: includes: pr1_t *) +theorem cprs_trans: ∀G,L. Transitive … (cprs G L). +normalize /2 width=3 by trans_TC/ qed-. + +(* Basic_1: was: pr3_confluence *) +(* Basic_1: includes: pr1_confluence *) +theorem cprs_conf: ∀G,L. confluent2 … (cprs G L) (cprs G L). +normalize /3 width=3 by cpr_conf, TC_confluent2/ qed-. + +theorem cprs_bind: ∀a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 +/3 width=5 by cprs_trans, cprs_bind_dx/ +qed. + +(* Basic_1: was: pr3_flat *) +theorem cprs_flat: ∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → + ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡* ⓕ{I}V2.T2. +#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 +/3 width=3 by cprs_flat_dx, cprs_strap1, cpr_pair_sn/ +qed. + +theorem cprs_beta_rc: ∀a,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2. +#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1 by cprs_beta_dx/ +#W #W2 #_ #HW2 #IHW1 (**) (* fulla uto too slow 14s *) +@(cprs_trans … IHW1) -IHW1 /3 width=1 by cprs_flat_dx, cprs_bind/ +qed. + +theorem cprs_beta: ∀a,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2. +#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1 by cprs_beta_rc/ +#V #V2 #_ #HV2 #IHV1 +@(cprs_trans … IHV1) -IHV1 /3 width=1 by cprs_flat_sn, cprs_bind/ +qed. + +theorem cprs_theta_rc: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → + ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 +/3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/ +qed. + +theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. + ⇧[0, 1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → + ⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. +#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 +/3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/ +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was pr3_gen_appl *) +lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & + U2 = ⓐV2. T2 + | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T & + ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡* U2 + | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 & + ⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T & + ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2. +#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ +#U #U2 #_ #HU2 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpr_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cprs_strap1, or3_intro0, ex3_2_intro/ + | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct + lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12 + lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 + /5 width=5 by cprs_flat_dx, cpr_cprs, cprs_bind, lsubr_abst, ex2_3_intro, or3_intro1/ + | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + @or3_intro2 @(ex4_5_intro … HV2 HT10) /3 width=3 by cprs_flat_sn, cprs_strap1, cpr_cprs, cprs_bind/ (**) (* full auto is too slow 11s *) + ] +| /4 width=9 by cprs_strap1, or3_intro1, ex2_3_intro/ +| /4 width=11 by cprs_strap1, or3_intro2, ex4_5_intro/ +] +qed-. + +(* Properties concerning sn parallel reduction on local environments ********) + +(* Basic_1: was just: pr3_pr2_pr2_t *) +(* Basic_1: includes: pr3_pr0_pr2_t *) +lemma llpr_cpr_trans: ∀G. s_r_transitive … (cpr G) (llpr G 0). +#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 +[ /2 width=3 by/ +| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 + elim (llpr_inv_lref_ge_dx … HL12 … HLK2) -L2 + /5 width=7 by cprs_delta, cprs_strap2, llpr_cpr_conf/ +| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (llpr_inv_bind_O … HL12) -HL12 /4 width=1 by cprs_bind/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12 + elim (llpr_inv_flat … HL12) -HL12 /3 width=1 by cprs_flat/ +| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12 + elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_zeta/ +| #G #L2 #V2 #T1 #T2 #HT12 #IHT12 #L1 #HL12 + elim (llpr_inv_flat … HL12) /3 width=1 by cprs_tau/ +| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #HL12 + elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12 + elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_beta/ +| #a #G #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12 + elim (llpr_inv_flat … HL12) -HL12 #HV1 #HL12 + elim (llpr_inv_bind_O … HL12) /3 width=3 by cprs_theta/ +] +qed-. + +lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +/4 width=9 by llpr_cpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed. + +(* Advanced properties ******************************************************) + +(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) +lemma cprs_llpr_trans: ∀G. s_rs_transitive … (cpr G) (llpr G 0). +/3 width=6 by llpr_cpr_trans, llpr_cpr_conf, s_r_trans_LTC1/ qed-. + +(* Basic_1: was: pr3_strip *) +(* Basic_1: includes: pr1_strip *) +lemma cprs_strip: ∀G,L. confluent2 … (cprs G L) (cpr G L). +normalize /4 width=3 by cpr_conf, TC_strip1/ qed-. + +lemma cprs_llpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #H @(cprs_ind_dx … T0 H) -T0 /2 width=3 by ex2_intro/ +#T0 #T #HT0 #_ #IHT1 #L1 #HL01 +elim (IHT1 … L1) /2 by llpr_cpr_conf/ -IHT1 #T2 #HT12 #HT2 +elim (llpr_cpr_conf_dx … HT0 … HL01) -L0 #T3 #HT03 #HT3 +elim (cprs_strip … HT2 … HT3) -T +/4 width=5 by cprs_strap2, cprs_strap1, ex2_intro/ +qed-. + +lemma cprs_llpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡[T0, 0] L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #T0 #T1 #HT01 #L1 #HL01 +elim (cprs_llpr_conf_dx … HT01 … HL01) +/4 width=5 by cprs_llpr_trans, cprs_llpr_conf, ex2_intro/ +qed-. + +lemma cprs_bind2_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → + ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. +/4 width=9 by cprs_llpr_trans, cprs_bind_dx, llpr_bind_repl_O/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_lift.etc new file mode 100644 index 000000000..27f0bb6e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/cprs_lift.etc @@ -0,0 +1,63 @@ +(**************************************************************************) +(* ___ *) +(* ||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/llpr_ldrop.ma". +include "basic_2/computation/cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) + +(* Advanced properties ******************************************************) + +(* Note: apparently this was missing in basic_1 *) +lemma cprs_delta: ∀G,L,K,V,V2,i. + ⇩[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡* V2 → + ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2. +#G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6 by cpr_cprs, cpr_delta/ ] +#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2 +lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK +elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/ +qed. + +lemma cprs_llpr_conf: ∀G. s_r_confluent1 … (cprs G) (llpr G 0). +/3 width=5 by llpr_cpr_conf, s_r_conf1_LTC1/ qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_1: was: pr3_gen_lref *) +lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 → + T2 = #i ∨ + ∃∃K,V1,T1. ⇩[i] L ≡ K.ⓓV1 & ⦃G, K⦄ ⊢ V1 ➡* T1 & + ⇧[0, i + 1] T1 ≡ T2. +#G #L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=6 by cpr_cprs, ex3_3_intro, or_intror/ +| * #K #V1 #T1 #HLK #HVT1 #HT1 + lapply (ldrop_fwd_drop2 … HLK) #H0LK + elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/ +] +qed-. + +(* Relocation properties ****************************************************) + +(* Basic_1: was: pr3_lift *) +lemma cprs_lift: ∀G. l_liftable (cprs G). +/3 width=10 by l_liftable_LTC, cpr_lift/ qed. + +(* Basic_1: was: pr3_gen_lift *) +lemma cprs_inv_lift1: ∀G. l_deliftable_sn (cprs G). +/3 width=6 by l_deliftable_sn_LTC, cpr_inv_lift1/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsn_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsn_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsnstar_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/lazypredsnstar_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_ldrop.etc similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_ldrop.etc index 0ca90bae4..74f7cc6b3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_ldrop.etc @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/relocation/fquq_alt.ma". +include "basic_2/static/ssta_llpx_sn.ma". include "basic_2/reduction/cpr_lift.ma". include "basic_2/reduction/cpr_llpx_sn.ma". include "basic_2/reduction/llpr.ma". @@ -49,8 +50,11 @@ lemma llpr_bind_repl_O: ∀I,G,L1,L2,V1,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[T, 0] (* Advanced properties ******************************************************) +lemma llpr_ssta_conf: ∀h,g,G. s_r_confluent1 … (ssta h g G) (llpr G 0). +/3 width=10 by ssta_llpx_sn_conf, cpr_lift/ qed-. + 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-. +/3 width=10 by cpr_llpx_sn_conf, cpr_inv_lift1, cpr_lift/ qed-. (* Properties on context-sensitive parallel reduction for terms *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_llpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/llpr_llpr.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpr_llpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_cprs.etc similarity index 68% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_cprs.etc index 910bedfe9..b9bf0f963 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_cprs.etc @@ -35,10 +35,44 @@ lemma llprs_cprs_trans: ∀G. s_rs_transitive … (cpr G) (llprs G 0). /3 width=5 by cprs_llpr_trans, s_rs_trans_TC1/ (**) (* full auto too slow *) qed-. +(* Note: this is an instance of a general theorem *) +lemma llprs_cprs_conf_dx: ∀G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡* U2 → + ∀L0. ⦃G2, L0⦄ ⊢ ➡*[T2, O] L2 → ⦃G2, L0⦄ ⊢ ➡*[U2, O] L2. +#G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llprs_ind_dx … H) -L0 // +#L0 #L #HL0 #HL2 #IHL2 @(llprs_strap2 … IHL2) -IHL2 +lapply (llprs_cprs_trans … HTU2 … HL2) -L2 #HTU2 +/3 width=3 by cprs_llpr_trans, cprs_llpr_conf/ +qed-. + +(* Note: this is an instance of a general theorem *) +lemma llprs_cpr_conf_dx: ∀G2,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → + ∀L0. ⦃G2, L0⦄ ⊢ ➡*[T2, O] L2 → ⦃G2, L0⦄ ⊢ ➡*[U2, O] L2. +#G2 #L2 #T2 #U2 #HTU2 #L0 #H @(llprs_ind_dx … H) -L0 // +#L0 #L #HL0 #HL2 #IHL2 @(llprs_strap2 … IHL2) -IHL2 +lapply (llprs_cpr_trans … HTU2 … HL2) -L2 #HTU2 +/3 width=3 by cprs_llpr_trans, cprs_llpr_conf/ +qed-. + +lemma llprs_cprs_conf_sn: ∀G,L0,L1,T0. ⦃G, L0⦄ ⊢ ➡*[T0, 0] L1 → + ∀T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +#G #L0 #L1 #T0 #H @(llprs_ind_dx … H) -L0 /2 width=3 by ex2_intro/ +#L0 #L #HL0 #HL1 #IHL1 #T1 #HT01 elim (cprs_llpr_conf_sn … HT01 … HL0) +#T2 #HT12 #HT02 elim (IHL1 … HT02) -IHL1 -HT02 +lapply (cprs_trans … HT01 … HT12) #HT02 +lapply (cprs_llpr_conf … HT02 … HL0) -HT02 -HL0 +/4 width=5 by cprs_llpr_trans, cprs_trans, ex2_intro/ +qed-. + +lemma llprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[T0, 0] L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. +/3 width=3 by llprs_cprs_conf_sn, cpr_cprs/ qed-. + lemma cprs_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2. -/4 width=3 by llprs_cprs_trans, llprs_pair_dx, cprs_bind/ qed. +/4 width=3 by llprs_cprs_trans, llprs_pair_dx, cprs_bind/ qed-. (* Inversion lemmas on context-sensitive parallel computation for terms *****) @@ -82,3 +116,7 @@ lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → /4 width=3 by cprs_strap1, ldrop_drop, ex3_intro, or_intror/ ] qed-. + +(* Note: we loose lprs_cprs_conf_dx and derivatives: + lprs_cpr_conf_dx lprs_cprs_conf +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_llprs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/llprs_llprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llprs_llprs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpx_sn_llpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/llpr/llpx_sn_llpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_lpx_sn.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma similarity index 92% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc rename to matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma index 2919d9d10..6dc76e174 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lpx_sn_tc.ma @@ -54,7 +54,7 @@ lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. ] qed-. -lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … 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 @@ -65,7 +65,7 @@ lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_trans … R (lpx_sn R) → ] qed-. -lemma TC_lpx_sn_ind: ∀R. s_rs_trans … R (lpx_sn R) → +lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀S:relation lenv. S (⋆) (⋆) → ( ∀I,K1,K2,V1,V2. @@ -88,7 +88,7 @@ lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. ] qed-. -fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … 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. @@ -98,12 +98,12 @@ fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_trans … R (lpx_sn R) → ] qed-. -lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_trans … R (lpx_sn R) → +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … 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) → +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → lpx_sn (LTC … R) L1 L2. /3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index a9008510e..6c685b0bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -76,7 +76,6 @@ b: "big tree" reduction c: conversion d: decomposed extended reduction e: decomposed extended conversion -n: reduction for "big tree" normal forms q: restricted reduction r: reduction s: substitution diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsn_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstar_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_3.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/predsnstaralt_3.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstaralt_3.ma 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 index ba2210f69..9d1d92e8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/cpr.ma". (* Properties on lazy sn pointwise extensions *******************************) -lemma llpx_sn_cpr_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → +lemma cpr_llpx_sn_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 [ // 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 a6afafbdb..7779c7f92 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -43,13 +43,13 @@ lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → ] qed-. -lemma lleq_cpx_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → +lemma cpx_lleq_conf: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → ∀L1. L2 ⋕[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. /3 width=3 by lleq_cpx_trans, lleq_sym/ qed-. -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 cpx_lleq_conf_sn: ∀h,g,G. s_r_confluent1 … (cpx h g G) (lleq 0). +/3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-. -lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → +lemma cpx_lleq_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. -/4 width=6 by lleq_cpx_conf_sn, lleq_sym/ qed-. +/4 width=6 by cpx_lleq_conf_sn, lleq_sym/ qed-. 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 36a97fc62..fdef2b619 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 @@ -20,7 +20,7 @@ include "basic_2/reduction/cpx.ma". (* Properties on lazy sn pointwise extensions *******************************) (* Note: lemma 1000 *) -lemma llpx_sn_cpx_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → +lemma cpx_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → ∀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 [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 0a7705e3d..4cf9d4bb0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -35,6 +35,7 @@ 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 llpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[T, 0] L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. +(* +lamma llpr_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_llpx, llpr_llpx/ qed. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma index 17bcd5a7a..3276008b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazypredsn_7.ma". -include "basic_2/reduction/llpr.ma". +include "basic_2/relocation/llpx_sn.ma". include "basic_2/reduction/cpx.ma". (* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************) @@ -67,6 +67,3 @@ lemma llpx_lref: ∀h,g,I,G,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → lemma llpx_refl: ∀h,g,G,T,d. reflexive … (llpx h g G d T). /2 width=1 by llpx_sn_refl/ qed. - -lemma llpr_llpx: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[T, d] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2. -/3 width=3 by llpx_sn_co, cpr_cpx/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma index 7c0949133..99eef8d55 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma @@ -76,6 +76,7 @@ lemma aaa_llpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L 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. +(* +lamma 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 0b9d88b99..3e4bcab8f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma @@ -55,7 +55,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. 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-. +/3 width=10 by cpx_llpx_sn_conf, cpx_inv_lift1, cpx_lift/ qed-. (* Inversion lemmas on relocation *******************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma new file mode 100644 index 000000000..6ceb64b51 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/llpx_sn_lpx_sn.ma". +include "basic_2/reduction/lpr.ma". +include "basic_2/reduction/llpx.ma". + +(* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************) + +(* Properties on sn parallel reduction **************************************) + +(* Note: this should be moved *) +lemma lpr_llpx: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2. +/3 width=4 by cpr_cpx, lpx_sn_llpx_sn, llpx_sn_co/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma index 7636e38e6..7bcf22df5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma @@ -49,7 +49,7 @@ lemma lpr_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡ L. lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V1 ➡ V2 → ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2. -/2 width=1/ qed. +/2 width=1 by lpx_sn_pair/ qed. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index deaeff927..7b65286ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr_lpr.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -341,13 +341,13 @@ theorem cpr_conf: ∀G,L. confluent … (cpr G L). lemma lpr_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L1⦄ ⊢ T1 ➡ T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3 by ex2_intro/ +elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) /2 width=3 by ex2_intro/ qed-. lemma lpr_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L0⦄ ⊢ T1 ➡ T. #G #L0 #T0 #T1 #HT01 #L1 #HL01 -elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3 by ex2_intro/ +elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) /2 width=3 by ex2_intro/ qed-. (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma similarity index 76% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc rename to matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma index 3dc3b2f79..c392bf54c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ldrop_lpx_sn.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma @@ -19,6 +19,32 @@ include "basic_2/relocation/ldrop_leq.ma". (* Properties on sn pointwise extension *************************************) +lemma lpx_sn_ldrop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by ldrop_drop_lt, ex3_2_intro/ + ] +] +qed-. + +lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K2,V2,i. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by ldrop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by ldrop_drop_lt, ex3_2_intro/ + ] +] +qed-. + lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). #R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma new file mode 100644 index 000000000..84c81f3b6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_lpx_sn.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lpx_sn.ma". +include "basic_2/relocation/llpx_sn.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Properties on pointwise extensions ***************************************) + +lemma lpx_sn_llpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀T,L1,L2,d. lpx_sn R L1 L2 → llpx_sn R d T L1 L2. +#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * +[ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/ +| -HR #i elim (lt_or_ge i (|L1|)) + [2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ] + #Hi #Hn #L2 #d elim (ylt_split i d) + [ -n /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ] + #Hdi #HL12 elim (ldrop_O1_lt L1 i) // + #I #K1 #V1 #HLK1 elim (lpx_sn_ldrop_conf … HL12 … HLK1) -HL12 + /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/ +| -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_gref/ +| /4 width=1 by llpx_sn_bind, lpx_sn_pair/ +| -HR /3 width=1 by llpx_sn_flat/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma new file mode 100644 index 000000000..72122143a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ssta.ma". + +(* STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ******************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma ssta_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → + ∀h,g,G. s_r_confluent1 … (ssta h g G) (llpx_sn R 0). +#R #H1R #H2R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ +| #G #Ls #Ks #V1s #W2s #V2s #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 *) +| #G #Ls #Ks #V1s #W1s #l #i #HLKs #Hl #HVW1s #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 … HVW1s) -HLKs -HLKd -HVW1s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index cb5bedd59..a5f14f196 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 @@ -84,21 +84,17 @@ table { } ] [ { "strongly normalizing extended computation" * } { - [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] - [ "lsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "lsx_ldrop" + "lsx_cpxs" + "lsx_csx" * ] +(* [ "lcosx ( ? ⊢ ⧤⬊*[?,?,?] ? )" "lcosx_cpxs" * ] *) + [ "llsx ( ? ⊢ ⋕⬊*[?,?,?,?] ? )" "llsx_alt ( ? ⊢ ⋕⬊⬊*[?,?,?,?] ? )" "llsx_ldrop" + "llsx_llpx" + "llsx_llpxs" + "llsx_csx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ] } ] [ { "\"big tree\" parallel computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ] - [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ] - [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpns" + "fpbs_fpbs" + "fpbs_ext" * ] - } - ] - [ { "parallel computation for \"big tree\" normal forms" * } { - [ "fpns ( ⦃?,?,?⦄ ⊢ ⋕➡*[?,?] ⦃?,?,?⦄ )" "fpns_fpns" * ] + [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] + [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] + [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_lpr" + "fpbs_fpbs" + "fpbs_ext" * ] } ] [ { "decomposed extended computation" * } { @@ -106,7 +102,8 @@ table { } ] [ { "context-sensitive extended computation" * } { - [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] + [ "llpxs ( ⦃?,?⦄ ⊢ ➡*[?,?,?,?] ? )" "llpxs_lleq" + "llpxs_aaa" + "llpxs_lprs" "llpxs_cpxs" + "llpxs_llpxs" * ] +(* [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] *) [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] @@ -136,7 +133,8 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] + [ "llpx ( ⦃?,?⦄ ⊢ ➡[?,?,?,?] ? )" "llpx_ldrop" + "llpx_lleq" + "llpx_aaa" + "llpx_lpr" * ] +(* [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] *) [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ] } ] @@ -154,7 +152,7 @@ table { ] [ { "context-sensitive reduction" * } { [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpr" * ] - [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ] + [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ] } ] [ { "irreducible forms for context-sensitive reduction" * } { @@ -190,7 +188,7 @@ table { } ] [ { "stratified static type assignment" * } { - [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ssta" * ] + [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_lpx_sn" + "ssta_ssta" * ] } ] [ { "local env. ref. for degree assignment" * } { @@ -213,9 +211,14 @@ table { ] class "yellow" [ { "substitution" * } { + [ { "lazy equivalence" * } { + [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] + } + ] [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ] - [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ] + [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] [ { "iterated local env. slicing" * } { @@ -236,23 +239,19 @@ table { class "orange" [ { "relocation" * } { [ { "structural successor for closures" * } { - [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ] - [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ] + [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] + [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" * ] } ] [ { "global env. slicing" * } { [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] } ] - [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_leq" + "lleq_ldrop" + "lleq_lleq" * ] - } - ] [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_llpx_sn" * ] + [ "llpx_sn" "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ] } - ] - [ { "basic local env. slicing" * } { + ] + [ { "basic local env. slicing" * } { [ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ] } ] -- 2.39.2