From: Ferruccio Guidi Date: Mon, 12 Mar 2018 22:26:55 +0000 (+0100) Subject: update in basic_2 X-Git-Tag: make_still_working~355 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a5c71699f1d0cf63a769c71dd8b8cd5dfff1933d update in basic_2 advances on fpb to be continued ... --- diff --git a/helm/www/lambdadelta/web/home/documentation_3.tbl b/helm/www/lambdadelta/web/home/documentation_3.tbl index b8a0eb9d8..4522bea00 100644 --- a/helm/www/lambdadelta/web/home/documentation_3.tbl +++ b/helm/www/lambdadelta/web/home/documentation_3.tbl @@ -24,7 +24,7 @@ table { "F. Guidi:" + @@("download/ld_talk_10s.pdf" "Adding Schematic Abstraction to λP") + - "(revised 2018-02)." + + "(2018-02)." + "Presentation at University of Bologna (slides)." * } ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_fleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_fleq.etc deleted file mode 100644 index 6463870f1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_fleq.etc +++ /dev/null @@ -1,41 +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/multiple/fleq.ma". -include "basic_2/reduction/fpb_lleq.ma". - -(* "RST" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************************) - -(* Properties on lazy equivalence for closures ******************************) - -lemma fleq_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≡[0] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≡[0] ⦃G2, L2, U2⦄. -#h #o #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 -#K2 #HK12 #G2 #L2 #U2 #H12 elim (lleq_fpb_trans … HK12 … H12) -K2 -/3 width=5 by fleq_intro, ex2_3_intro/ -qed-. - -(* Inversion lemmas on lazy equivalence for closures ************************) - -lemma fpb_inv_fleq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≡[0] ⦃G2, L2, T2⦄ → ⊥. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -[ #G2 #L2 #T2 #H12 #H elim (fleq_inv_gen … H) -H - /3 width=8 by lleq_fwd_length, fqu_inv_eq/ -| #T2 #_ #HnT #H elim (fleq_inv_gen … H) -H /2 width=1 by/ -| #L2 #_ #HnL #H elim (fleq_inv_gen … H) -H /2 width=1 by/ -] -qed-. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma new file mode 100644 index 000000000..1d0d211d5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/ffdeq.ma". +include "basic_2/rt_transition/fpb_lfdeq.ma". + +(* PROPER PARALLEL RST-TRANSITION FOR CLOSURES ******************************) + +(* Properties with degree-based equivalence for closures ********************) + +(* Basic_2A1: uses: fleq_fpb_trans *) +lemma ffdeq_fpb_trans: ∀h,o,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≛[h, o] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, o] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, o] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≛[h, o] ⦃G2, L2, U2⦄. +#h #o #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 +#K2 #T2 #HK12 #HT12 #G2 #L2 #U2 #H12 +elim (tdeq_fpb_trans … HT12 … H12) -T2 #K0 #T0 #H #HT0 #HK0 +elim (lfdeq_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0 +@(ex2_3_intro … H) -H (**) (* full auto too slow *) +/4 width=3 by ffdeq_intro_dx, lfdeq_trans, tdeq_lfdeq_conf, tdeq_trans/ +qed-. + +(* Inversion lemmas with degree-based equivalence for closures **************) +(* +(* Basic_2A1: uses: fpb_inv_fleq *) +lemma fpb_inv_ffdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⊥. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #H elim (ffdeq_inv_gen_sn … H) -H + #_ #H1 #H2 +(* + + /3 width=8 by lfdeq_fwd_length, fqu_inv_eq/ +*) +| #T2 #_ #HnT #H elim (ffdeq_inv_gen_sn … H) -H /2 width=1 by/ +| #L2 #_ #HnL #H elim (ffdeq_inv_gen_sn … H) -H /2 width=1 by/ +] +qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma index c4489bccf..b98034aa3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_lfdeq.ma @@ -21,6 +21,20 @@ include "basic_2/rt_transition/fpb.ma". (* Properties with degree-based equivalence for local environments **********) +lemma tdeq_fpb_trans: ∀h,o,U2,U1. U2 ≛[h, o] U1 → + ∀G1,G2,L1,L2,T1. ⦃G1, L1, U1⦄ ≻[h, o] ⦃G2, L2, T1⦄ → + ∃∃L,T2. ⦃G1, L1, U2⦄ ≻[h, o] ⦃G2, L, T2⦄ & T2 ≛[h, o] T1 & L ≛[h, o, T1] L2. +#h #o #U2 #U1 #HU21 #G1 #G2 #L1 #L2 #T1 * -G2 -L2 -T1 +[ #G2 #L2 #T1 #H + elim (tdeq_fqu_trans … H … HU21) -H + /3 width=5 by fpb_fqu, ex3_2_intro/ +| #T1 #HUT1 #HnUT1 + elim (tdeq_cpx_trans … HU21 … HUT1) -HUT1 + /6 width=5 by fpb_cpx, tdeq_canc_sn, tdeq_trans, ex3_2_intro/ +| /6 width=5 by fpb_lfpx, lfpx_tdeq_div, tdeq_lfdeq_conf, ex3_2_intro/ +] +qed-. + (* Basic_2A1: was just: lleq_fpb_trans *) lemma lfdeq_fpb_trans: ∀h,o,F,K1,K2,T. K1 ≛[h, o, T] K2 → ∀G,L2,U. ⦃F, K2, T⦄ ≻[h, o] ⦃G, L2, U⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 9dc71abaf..856fccf53 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -36,6 +36,13 @@ lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2. /3 width=5 by lfpx_fsge_comp, lfxs_bind_dx_split_void/ qed-. +lemma lfpx_tdeq_conf: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpx h G). +/2 width=5 by tdeq_lfxs_conf/ qed-. + +lemma lfpx_tdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀G,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T2] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T1] L2. +/2 width=5 by tdeq_lfxs_div/ qed-. + lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o). #h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/ [ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 14994967a..9784f3490 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -73,14 +73,21 @@ lemma frees_lfdeq_conf: ∀h,o,f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → ∀L2. L1 ≛[h, o, f] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. /2 width=7 by frees_tdeq_conf_lfdeq, tdeq_refl/ qed-. -lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). -#h #o #L1 #T1 #T2 #HT12 #L2 * +lemma tdeq_lfxs_conf: ∀R,h,o. s_r_confluent1 … (cdeq h o) (lfxs R). +#R #h #o #L1 #T1 #T2 #HT12 #L2 * /3 width=5 by frees_tdeq_conf, ex2_intro/ qed-. +lemma tdeq_lfxs_div: ∀R,h,o,T1,T2. T1 ≛[h, o] T2 → + ∀L1,L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. +/3 width=5 by tdeq_lfxs_conf, tdeq_sym/ qed-. + +lemma tdeq_lfdeq_conf: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). +/2 width=5 by tdeq_lfxs_conf/ qed-. + lemma tdeq_lfdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 → ∀L1,L2. L1 ≛[h, o, T2] L2 → L1 ≛[h, o, T1] L2. -/3 width=3 by tdeq_lfdeq_conf, tdeq_sym/ qed-. +/2 width=5 by tdeq_lfxs_div/ qed-. lemma lfdeq_atom: ∀h,o,I. ⋆ ≛[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index dcf2f4693..f1f4b8415 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -34,6 +34,9 @@ Stage "A2": "Extending the Applicability Condition" + + Support for rt-computation completed. + Exclusion binder in local environments. Syntactic component updated: @@ -45,7 +48,7 @@ (anniversary milestone). - First behavioral component reconstructed: + First behavioral component completed: rt_transition. @@ -58,7 +61,7 @@ Confluence for context-sensitive parallel r-transition on terms. - Syntactic component reconstructed: + Syntactic component completed: syntax, relocation, s_transition, s_computation, static (anniversary milestone). 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 4da8d232f..e8cb49308 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 @@ -123,7 +123,7 @@ table { [ { "rt-transition" * } { [ { "uncounted parallel rst-transition" * } { [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] + [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" + "fpb_ffdeq" * ] } ] [ { "context-sensitive parallel r-transition" * } {