From 10b733131aa2667d8ba4318d517f0ba3cf137359 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 6 Mar 2017 22:20:11 +0000 Subject: [PATCH] - advances on lfxs for lfpxs - ex_cpr_omega (2-steps loop) --- .../examples/ex_cpr_omega.ma | 20 ++-- .../examples/ex_fpbg_refl.ma | 0 .../examples/ex_snv_eta.ma | 0 .../examples/ex_sta_ldec.ma | 0 .../lambdadelta/apps_2/web/apps_2_src.tbl | 12 ++- .../lambdadelta/basic_2/etc/cpxs/cpxs.etc | 3 +- .../basic_2/etc/lfxs/lfxs_drops.etc | 93 ------------------ .../basic_2/etc/lfxs/lfxs_lfxs.etc | 59 ------------ .../{etc/lfxs/lfxs.etc => i_static/lfxss.ma} | 96 +++++++------------ .../lambdadelta/basic_2/i_static/lfxss_etc.ma | 31 ++++++ .../relations/predtysnstar_5.ma} | 13 +-- .../relations/relationstarstar_4.ma} | 13 +-- .../basic_2/rt_computation/cpxs_tsts.ma | 36 +++---- .../basic_2/rt_computation/csx_vector.ma | 16 ++-- .../basic_2/rt_computation/lfpxs.ma | 54 +++++++++++ .../basic_2/rt_computation/lfpxs_etc.ma | 3 + .../basic_2/rt_computation/lfpxs_fqup.ma | 42 ++++++++ .../basic_2/rt_computation/lfpxs_length.ma | 7 ++ .../basic_2/rt_computation/lpxs.ma | 74 -------------- .../basic_2/rt_computation/partial.txt | 2 + .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 12 --- .../lambdadelta/basic_2/web/basic_2_src.tbl | 28 +++--- .../matita/contribs/lambdadelta/partial.txt | 1 + 23 files changed, 238 insertions(+), 377 deletions(-) rename matita/matita/contribs/lambdadelta/{basic_2 => apps_2}/examples/ex_cpr_omega.ma (71%) rename matita/matita/contribs/lambdadelta/{basic_2 => apps_2}/examples/ex_fpbg_refl.ma (100%) rename matita/matita/contribs/lambdadelta/{basic_2 => apps_2}/examples/ex_snv_eta.ma (100%) rename matita/matita/contribs/lambdadelta/{basic_2 => apps_2}/examples/ex_sta_ldec.ma (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc rename matita/matita/contribs/lambdadelta/basic_2/{etc/lfxs/lfxs.etc => i_static/lfxss.ma} (71%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma rename matita/matita/contribs/lambdadelta/basic_2/{etc/lfxs/lfxs_length.etc => notation/relations/predtysnstar_5.ma} (73%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lfxs/lfxs_fqup.etc => notation/relations/relationstarstar_4.ma} (72%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma rename to matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma index ad4d40bb9..0bbe88b88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_cpr_omega.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cpr_omega.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/cpr.ma". +include "basic_2/rt_transition/cpr.ma". (* EXAMPLES *****************************************************************) @@ -26,18 +26,16 @@ definition Omega2: term → term ≝ λW. +ⓓⓝW.(Delta W).ⓐ#0.#0. (* Basic properties *********************************************************) -lemma Delta_lift: ∀W1,W2,l,k. ⬆[l, k] W1 ≡ W2 → - ⬆[l, k] (Delta W1) ≡ (Delta W2). -/4 width=1 by lift_flat, lift_bind, lift_lref_lt/ qed. +lemma Delta_lifts: ∀W1,W2,f. ⬆*[f] W1 ≡ W2 → + ⬆*[f] (Delta W1) ≡ (Delta W2). +/4 width=1 by lifts_lref, lifts_bind, lifts_flat/ qed. (* Main properties **********************************************************) -theorem cpr_Omega_12: ∀G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡ Omega2 W. -/2 width=1 by cpr_beta/ qed. +theorem cpr_Omega_12: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega1 W ➡[h] Omega2 W. +/2 width=1 by cpm_beta/ qed. -theorem cpr_Omega_21: ∀G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡ Omega1 W. -#G #L #W1 elim (lift_total W1 0 1) #W2 #HW12 -@(cpr_zeta … (Omega1 W2)) /3 width=1 by Delta_lift, lift_flat/ -@cpr_flat @(cpr_delta … (Delta W1) ? 0) -[3,5,8,10: /2 width=2 by Delta_lift/ |4,9: /2 width=1 by cpr_eps/ |*: skip ] +theorem cpr_Omega_21: ∀h,G,L,W. ⦃G, L⦄ ⊢ Omega2 W ➡[h] Omega1 W. +#h #G #L #W1 elim (lifts_total W1 (𝐔❴1❵)) +/5 width=5 by lifts_flat, cpm_zeta, cpm_eps, cpm_appl, cpm_delta, Delta_lifts/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/examples/ex_fpbg_refl.ma rename to matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/examples/ex_snv_eta.ma rename to matita/matita/contribs/lambdadelta/apps_2/examples/ex_snv_eta.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/examples/ex_sta_ldec.ma rename to matita/matita/contribs/lambdadelta/apps_2/examples/ex_sta_ldec.ma diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 9a19a7715..d43a58823 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -10,7 +10,7 @@ table { } ] (* - class "orange" + class "yellow" [ { "MLTT1" * } { [ { "" * } { [ "genv_primitive" "judgment" * ] @@ -19,7 +19,7 @@ table { } ] *) - class "red" + class "orange" [ { "functional" * } { [ { "reduction and type machine" * } { [ "rtm" "rtm_step ( ? ⇨ ? )" * ] @@ -31,6 +31,14 @@ table { ] } ] + class "red" + [ { "examples" * } { + [ { "terms with special features" * } { + [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ] + } + ] + } + ] } class "top" { * } diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc index 89e1466f7..ada873d81 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs.etc @@ -7,8 +7,7 @@ lemma cprs_cpxs: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈* T2 → ⦃G, L⦄ ⊢ cpr_cpx/ qed. -lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] -𝐍⦃T⦄ → T = U. +lemma cpxs_inv_cnx1: ∀h,o,G,L,T,U. ⦃G, L⦄ ⊢ T ⬈*[h] U → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → T = U. #h #o #G #L #T #U #H @(cpxs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc deleted file mode 100644 index 0a3f287bb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_drops.etc +++ /dev/null @@ -1,93 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/relocation/drops_ceq.ma". -include "basic_2/relocation/drops_lexs.ma". -include "basic_2/static/frees_drops.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -definition dedropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → - ∀K2,T. K1 ⦻*[R, T] K2 → ∀U. ⬆*[f] T ≡ U → - ∃∃L2. L1 ⦻*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. - -definition dropable_sn: predicate (relation3 lenv term term) ≝ - λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → - ∀L2,U. L1 ⦻*[R, U] L2 → ∀T. ⬆*[f] T ≡ U → - ∃∃K2. K1 ⦻*[R, T] K2 & ⬇*[b, f] L2 ≡ K2. - -definition dropable_dx: predicate (relation3 lenv term term) ≝ - λR. ∀L1,L2,U. L1 ⦻*[R, U] L2 → - ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U → - ∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⦻*[R, T] K2. - -(* Properties with generic slicing for local environments *******************) - -(* Basic_2A1: includes: llpx_sn_lift_le llpx_sn_lift_ge *) -lemma lfxs_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable2 R → dedropable_sn R. -#R #H1R #H2R #b #f #L1 #K1 #HLK1 #K2 #T * #f1 #Hf1 #HK12 #U #HTU -elim (frees_total L1 U) #f2 #Hf2 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf -elim (lexs_liftable_co_dedropable … H1R … H2R … HLK1 … HK12 … Hf) -f1 -K1 -/3 width=6 by cfull_lift, ex3_intro, ex2_intro/ -qed-. - -(* Inversion lemmas with generic slicing for local environments *************) - -(* Basic_2A1: restricts: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *) -(* Basic_2A1: was: llpx_sn_drop_conf_O *) -lemma lfxs_dropable_sn: ∀R. dropable_sn R. -#R #b #f #L1 #K1 #HLK1 #H1f #L2 #U * #f2 #Hf2 #HL12 #T #HTU -elim (frees_total K1 T) #f1 #Hf1 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #H2f -elim (lexs_co_dropable_sn … HLK1 … HL12 … H2f) -f2 -L1 -/3 width=3 by ex2_intro/ -qed-. - -(* Basic_2A1: was: llpx_sn_drop_trans_O *) -(* Note: the proof might be simplified *) -lemma lfxs_dropable_dx: ∀R. dropable_dx R. -#R #L1 #L2 #U * #f2 #Hf2 #HL12 #b #f #K2 #HLK2 #H1f #T #HTU -elim (drops_isuni_ex … H1f L1) #K1 #HLK1 -elim (frees_total K1 T) #f1 #Hf1 -lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -K1 #H2f -elim (lexs_co_dropable_dx … HL12 … HLK2 … H2f) -L2 -/4 width=9 by frees_inv_lifts, ex2_intro/ -qed-. - -(* Basic_2A1: was: llpx_sn_inv_lift_O *) -lemma lfxs_inv_lift_bi: ∀R,L1,L2,U. L1 ⦻*[R, U] L2 → - ∀K1,K2,i. ⬇*[i] L1 ≡ K1 → ⬇*[i] L2 ≡ K2 → - ∀T. ⬆*[i] T ≡ U → K1 ⦻*[R, T] K2. -#R #L1 #L2 #U #HL12 #K1 #K2 #i #HLK1 #HLK2 #T #HTU -elim (lfxs_dropable_sn … HLK1 … HL12 … HTU) -L1 -U // #Y #HK12 #HY -lapply (drops_mono … HY … HLK2) -L2 -i #H destruct // -qed-. - -lemma lfxs_inv_lref_sn: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. -#R #L1 #L2 #i #HL12 #I #K1 #V1 #HLK1 elim (lfxs_dropable_sn … HLK1 … HL12 (#0)) -HLK1 -HL12 // -#Y #HY #HLK2 elim (lfxs_inv_zero_pair_sn … HY) -HY -#K2 #V2 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ -qed-. - -lemma lfxs_inv_lref_dx: ∀R,L1,L2,i. L1 ⦻*[R, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & K1 ⦻*[R, V1] K2 & R K1 V1 V2. -#R #L1 #L2 #i #HL12 #I #K2 #V2 #HLK2 elim (lfxs_dropable_dx … HL12 … HLK2 … (#0)) -HLK2 -HL12 // -#Y #HLK1 #HY elim (lfxs_inv_zero_pair_dx … HY) -HY -#K1 #V1 #HK12 #HV12 #H destruct /2 width=5 by ex3_2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc index 307740bea..4ca71664c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_lfxs.etc @@ -1,41 +1,3 @@ -(**************************************************************************) -(* ___ *) -(* ||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/lexs_lexs.ma". -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/frees_frees.ma". -include "basic_2/static/lfxs.ma". - -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Main properties **********************************************************) - -theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T. - L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 → - L1 ⦻*[R, ⓑ{p,I}V1.T] L2. -#R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 -elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2)) -/3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/ -qed. - -theorem lfxs_flat: ∀R,I,L1,L2,V,T. - L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 → - L1 ⦻*[R, ⓕ{I}V.T] L2. -#R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) -/3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ -qed. - theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → ∀T. Transitive … (lfxs R T). #R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 @@ -47,24 +9,3 @@ lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 /4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ qed-. - -theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → - R_confluent2_lfxs R R R R → - ∀T. confluent … (lfxs R T). -#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 -lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 -lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 -elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] -[ #L #HL1 #HL2 - elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1 - elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2 - lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 - lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 - /3 width=5 by ex2_intro/ -| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02 - elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 - lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 - lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 - elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc rename to matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma index f09a2cfc2..757d3e684 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma @@ -12,83 +12,52 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_id.ma". -include "basic_2/notation/relations/relationstar_4.ma". -include "basic_2/relocation/lexs.ma". -include "basic_2/static/frees.ma". +include "basic_2/notation/relations/relationstarstar_4.ma". +include "basic_2/static/lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) -definition lfxs (R) (T): relation lenv ≝ - λL1,L2. ∃∃f. L1 ⊢ 𝐅*⦃T⦄ ≡ f & L1 ⦻*[R, cfull, f] L2. +definition lfxss (R) (T): relation lenv ≝ TC … (lfxs R T). -interpretation "generic extension on referred entries (local environment)" - 'RelationStar R T L1 L2 = (lfxs R T L1 L2). - -definition R_frees_confluent: predicate (relation3 lenv term term) ≝ - λRN. - ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 → - ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. - -definition lexs_frees_confluent: relation (relation3 lenv term term) ≝ - λRN,RP. - ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → - ∀L2. L1 ⦻*[RN, RP, f1] L2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. - -definition R_confluent2_lfxs: relation4 (relation3 lenv term term) - (relation3 lenv term term) … ≝ - λR1,R2,RP1,RP2. - ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → - ∃∃T. R2 L1 T1 T & R1 L2 T2 T. +interpretation "tc of generic extension on referred entries (local environment)" + 'RelationStarStar R T L1 L2 = (lfxss R T L1 L2). (* Basic properties ***********************************************************) -lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. -/3 width=3 by lexs_atom, frees_atom, ex2_intro/ -qed. +lemma lfxss_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. +/2 width=1 by inj/ qed. -lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s. - L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/ +lemma lfxss_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 +/3 width=4 by lfxs_sort, step, inj/ qed. -lemma lfxs_zero: ∀R,I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, #0] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 * /3 width=3 by lexs_next, frees_zero, ex2_intro/ +lemma lfxss_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 +/3 width=4 by lfxs_lref, step, inj/ qed. -lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i. - L1 ⦻*[R, #i] L2 → L1.ⓑ{I}V1 ⦻*[R, #⫯i] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ +lemma lfxss_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 +/3 width=4 by lfxs_gref, step, inj/ qed. -lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l. - L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/ -qed. - -lemma lfxs_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. - L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V1 → - ∀V2. R L1 V V2 → - L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V2. -#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR -/3 width=5 by lexs_pair_repl, ex2_intro/ +lemma lfxss_sym: ∀R. lexs_frees_confluent R cfull → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (lfxss R T). +#R #H1R #H2R #T #L1 #L2 #H elim H -L2 +/4 width=3 by lfxs_sym, TC_strap, inj/ qed-. -lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxs R T). -#R #H1R #H2R #T #L1 #L2 * #f1 #Hf1 #HL12 elim (H1R … Hf1 … HL12) -Hf1 -/4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/ +lemma lfxss_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2. +#R1 #R2 #HR #L1 #L2 #T #H elim H -L2 +/4 width=5 by lfxs_co, step, inj/ qed-. - -lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. -#R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ -qed-. - +(* (* Basic inversion lemmas ***************************************************) lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. @@ -100,7 +69,7 @@ lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. qed-. lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 @@ -113,7 +82,7 @@ lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → qed-. lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * @@ -124,7 +93,7 @@ lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → qed-. lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. #R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * @@ -262,3 +231,4 @@ qed-. llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx *) +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma new file mode 100644 index 000000000..f063b1816 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma @@ -0,0 +1,31 @@ +(* +lemma lfxss_zero: ∀R,I,L1,L2,V1. L1 ⦻**[R, V1] L2 → ∀V2. + R L1 V1 V2 → L1.ⓑ{I}V1 ⦻**[R, #0] L2.ⓑ{I}V2. +#R #I #L1 #L2 #V1 #H + +elim H -L2 /3 width=5 by lfxs_zero, inj/ +#L #L2 #H0 #HL2 #IH #V2 #HV12 +lapply (IH … HV12) -IH #HL1 +@(step … HL1) -HL1 @lfxs_zero + +axiom pippo_fwd: ∀R,I,Y1,L2,V2,T. Y1 ⦻*[R, T] L2.ⓑ{I}V2 → + ∃∃L1,V1. Y1 = L1.ⓑ{I}V1. + +fact pippo: ∀R,I,L1,Y,T,V. L1.ⓑ{I}V ⦻**[R, T] Y → + ∀L2,V1. Y = L2.ⓑ{I}V1 → + ∀V2. R L1 V V2 → + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. +#R #I #L1 #Y #T #V #H elim H -Y +[ /3 width=2 by lfxs_pair_repl_dx, inj/ +| #L #Y #_ #HL2 #IH #L2 #V1 #H #V2 #HV2 destruct + elim (pippo_fwd … HL2) #L0 #V0 #H destruct + @step [2: @(IH … HV2) // | skip ] -IH -HV2 + +lemma lfxss_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V1 → + ∀V2. R L1 V V2 → + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. +#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR +/3 width=5 by lexs_pair_repl, ex2_intro/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma similarity index 73% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma index 01dd82cf4..d0362ba88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_length.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma @@ -12,13 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lexs_length.ma". -include "basic_2/static/lfxs.ma". +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Forward lemmas with length for local environments ************************) - -lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|. -#R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ -qed-. +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedTySnStar $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma similarity index 72% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma index 62c5b0564..145078d07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfxs/lfxs_fqup.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstarstar_4.ma @@ -12,13 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/static/frees_fqup.ma". -include "basic_2/static/lfxs.ma". +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) - -(* Advanced properties ******************************************************) - -lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. -#R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ -qed. +notation "hvbox( L1 ⦻ * * [ break term 46 R , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'RelationStarStar $R $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma index c9d5f5ae9..64f1facd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tsts.ma @@ -13,38 +13,30 @@ (**************************************************************************) include "basic_2/syntax/tsts.ma". -include "basic_2/computation/lpxs_cpxs.ma". +include "basic_2/rt_computation/lfpxs_cpxs.ma". -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) - -(* Forward lemmas involving same top term structure *************************) +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) +(* Forward lemmas with same top term structure ******************************) +(* lemma cpxs_fwd_cnx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ⬈*[h, o] U → T ≂ U. #h #o #G #L #T #HT #U #H >(cpxs_inv_cnx1 … H HT) -G -L -T // qed-. - -lemma cpxs_fwd_sort: ∀h,o,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h, o] U → - ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h, o] U. -#h #o #G #L #U #s #H -elim (cpxs_inv_sort1 … H) -H #n #d generalize in match s; -s @(nat_ind_plus … n) -n -[ #s #_ #H -d destruct /2 width=1 by or_introl/ -| #n #IHn #s >plus_plus_comm_23 #Hnd #H destruct - lapply (deg_next_SO … Hnd) -Hnd #Hnd - elim (IHn … Hnd) -IHn - [ #H lapply (tsts_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/ - | generalize in match Hnd; -Hnd @(nat_ind_plus … n) -n - /4 width=3 by cpxs_strap2, cpx_st, or_intror/ - | >iter_SO >iter_n_Sm // - ] +*) +lemma cpxs_fwd_sort: ∀h,G,L,U,s. ⦃G, L⦄ ⊢ ⋆s ⬈*[h] U → + ⋆s ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h s) ⬈*[h] U. +#h #G #L #U #s #H elim (cpxs_inv_sort1 … H) -H * +[ #H destruct /2 width=1 by or_introl/ +| #n #H destruct + @or_intror >iter_S <(iter_n_Sm … (next h)) // (**) ] qed-. (* Basic_1: was just: pr3_iso_beta *) -lemma cpxs_fwd_beta: ∀h,o,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ⬈*[h, o] U → - ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ⬈*[h, o] U. -#h #o #a #G #L #V #W #T #U #H -elim (cpxs_inv_appl1 … H) -H * +lemma cpxs_fwd_beta: ∀h,p,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{p}W.T ⬈*[h] U → + ⓐV.ⓛ{p}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V.T ⬈*[h] U. +#h #p #G #L #V #W #T #U #H elim (cpxs_inv_appl1 … H) -H * [ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma index 7d23b2f92..03651de12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma @@ -13,27 +13,27 @@ (**************************************************************************) include "basic_2/syntax/term_vector.ma". -include "basic_2/computation/csx.ma". +include "basic_2/rt_computation/csx.ma". -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) +(* STRONGLY NORMALIZING TERMS VECTORS FOR UNCOUNTED PARALLEL RT-TRANSITION **) definition csxv: ∀h. sd h → relation3 genv lenv (list term) ≝ λh,o,G,L. all … (csx h o G L). interpretation - "context-sensitive strong normalization (term vector)" - 'SN h o G L Ts = (csxv h o G L Ts). + "strong normalization for uncounted context-sensitive parallel rt-transition (term vector)" + 'PRedTyStrong h o G L Ts = (csxv h o G L Ts). (* Basic inversion lemmas ***************************************************) -lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬊*[h, o] T @ Ts → - ⦃G, L⦄ ⊢ ⬊*[h, o] T ∧ ⦃G, L⦄ ⊢ ⬊*[h, o] Ts. +lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T@Ts⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Ts⦄. normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Ⓐ Vs.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, o] T. +lemma csx_fwd_applv: ∀h,o,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄ → + ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. #h #o #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/ #V #Vs #IHVs #HVs lapply (csx_fwd_pair_sn … HVs) #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma new file mode 100644 index 000000000..7e1b32915 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/predtysnstar_5.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +definition lfpxs: ∀h. relation4 genv term lenv lenv ≝ + λh,G,T. TC … (lfpx h G T). + +interpretation + "uncounted parallel rt-computation on referred entries (local environment)" + 'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2). + +(* Basic properties *********************************************************) + +(* Basic_2A1: was just: lpx_lpxs *) +lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=1 by inj/ qed. + +(* Basic_2A1: was just: lpxs_strap1 *) +lemma lfpxs_strap1: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by step/ qed. + +(* Basic_2A1: was just: lpxs_strap2 *) +lemma lfpxs_strap2: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by TC_strap/ qed. +(* +(* Basic_2A1: was just: lpxs_pair_refl *) +lemma lfpxs_pair_refl: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. +/2 width=1 by TC_lpx_sn_pair_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: was just: lpxs_inv_atom1 *) +lemma lfpxs_inv_atom1: ∀h,G,L2.T. ⦃G, ⋆⦄ ⊢ ⬈*[h, T] L2 → L2 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. + +(* Basic_2A1: was just: lpxs_inv_atom2 *) +lemma lfpxs_inv_atom2: ∀h,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] ⋆ → L1 = ⋆. +/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma new file mode 100644 index 000000000..8c8679a47 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma @@ -0,0 +1,3 @@ +(* Basic_2A1: was just: lprs_lpxs *) +lemma lprs_lfpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. +/3 width=3 by lpr_lpx, monotonic_TC/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma new file mode 100644 index 000000000..ce2496b91 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lfpx_fqup.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Advanced eliminators *****************************************************) + +(* Basic_2A1: was just: lpxs_ind *) +lemma lfpxs_ind: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. +#h #G #L1 #T #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +(* Basic_2A1: was just: lpxs_ind_dx *) +lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1. +#h #o #G #L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was just: lpxs_refl *) +lemma lfpxs_refl: ∀h,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, T] L. +/2 width=1 by lfpx_lfpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma new file mode 100644 index 000000000..ac2f64dc5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma @@ -0,0 +1,7 @@ +(* Basic forward lemmas *****************************************************) + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: was just: lpxs_fwd_length *) +lemma lfpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, o] L2 → |L1| = |L2|. +/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma deleted file mode 100644 index b6c91c8b1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/predsnstar_5.ma". -include "basic_2/reduction/lpx.ma". -include "basic_2/computation/lprs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) - -definition lpxs: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,o,G. TC … (lpx h o G). - -interpretation "extended parallel computation (local environment, sn variant)" - 'PRedSnStar h o G L1 L2 = (lpxs h o G L1 L2). - -(* Basic eliminators ********************************************************) - -lemma lpxs_ind: ∀h,o,G,L1. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L → ⦃G, L⦄ ⊢ ➡[h, o] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L2. -#h #o #G #L1 #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. - -lemma lpxs_ind_dx: ∀h,o,G,L2. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ➡[h, o] L → ⦃G, L⦄ ⊢ ➡*[h, o] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1. -#h #o #G #L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Basic properties *********************************************************) - -lemma lprs_lpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/3 width=3 by lpr_lpx, monotonic_TC/ qed. - -lemma lpx_lpxs: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=1 by inj/ qed. - -lemma lpxs_refl: ∀h,o,G,L. ⦃G, L⦄ ⊢ ➡*[h, o] L. -/2 width=1 by lprs_lpxs/ qed. - -lemma lpxs_strap1: ∀h,o,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L → ⦃G, L⦄ ⊢ ➡[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=3 by step/ qed. - -lemma lpxs_strap2: ∀h,o,G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L → ⦃G, L⦄ ⊢ ➡*[h, o] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2. -/2 width=3 by TC_strap/ qed. - -lemma lpxs_pair_refl: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V. -/2 width=1 by TC_lpx_sn_pair_refl/ qed. - -(* Basic inversion lemmas ***************************************************) - -lemma lpxs_inv_atom1: ∀h,o,G,L2. ⦃G, ⋆⦄ ⊢ ➡*[h, o] L2 → L2 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. - -lemma lpxs_inv_atom2: ∀h,o,G,L1. ⦃G, L1⦄ ⊢ ➡*[h, o] ⋆ → L1 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → |L1| = |L2|. -/2 width=2 by TC_lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 556cb5704..cb191dab1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,2 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_cpxs.ma +lfpxs.ma lfpxs_fqup.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 654ab4d0d..26289760b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -35,19 +35,7 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T. #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2) /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/ qed. -(* -theorem lfxs_trans: ∀R. lexs_frees_confluent R cfull → - ∀T. Transitive … (lfxs R T). -#R #H1R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 -elim (H1R … Hf1 … HL1) #f #H0 #H1 -lapply (frees_mono … Hf2 … H0) -Hf2 -H0 #Hf2 -lapply (lexs_eq_repl_back … HL2 … Hf2) -f2 #HL2 -lapply (sle_lexs_trans … HL1 … H1) -HL1 // #Hl1 -@(ex2_intro … f) -/4 width=7 by lreq_trans, lexs_eq_repl_back, ex2_intro/ -qed-. -*) theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull → R_confluent2_lfxs R R R R → ∀T. confluent … (lfxs R T). diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 03c104136..f3d9d6021 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 @@ -11,14 +11,6 @@ table { ] (* class "wine" - [ { "examples" * } { - [ { "terms with special features" * } { - [ "ex_sta_ldec" + "ex_cpr_omega" + "ex_fpbg_refl" + "ex_snv_eta" * ] - } - ] - } - ] - class "magenta" [ { "" * } { [ { "" * } { [ "" * ] @@ -35,7 +27,7 @@ table { } ] *) - class "prune" + class "magenta" [ { "dynamic typing" * } { (* [ { "local env. ref. for native type assignment" * } { @@ -58,7 +50,7 @@ table { ] } ] - class "blue" + class "prune" [ { "equivalence" * } { [ { "decomposed rt-equivalence" * } { [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] @@ -70,7 +62,7 @@ table { ] } ] - class "sky" + class "blue" [ { "conversion" * } { [ { "context-sensitive conversion" * } { [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ] @@ -79,7 +71,7 @@ table { } ] *) - class "cyan" + class "sky" [ { "rt-computation" * } { (* [ { "evaluation for context-sensitive rt-reduction" * } { @@ -121,13 +113,15 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] *) + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_cpxs" * ] } ] } ] - class "water" + class "cyan" [ { "rt-transition" * } { [ { "parallel qrst-transition" * } { (* [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" + "fpbq_aaa" * ] *) @@ -159,6 +153,14 @@ table { ] } ] + class "water" + [ { "iterated static typing" * } { + [ { "generic extension on referred entries" * } { + [ "lfxss ( ? ⦻**[?,?] ? )" * ] + } + ] + } + ] class "green" [ { "static typing" * } { [ { "generic reducibility" * } { diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 1c14e9fed..7596031ba 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -4,3 +4,4 @@ basic_2/relocation basic_2/s_transition basic_2/s_computation basic_2/static +basic_2/i_static -- 2.39.2