From d0e3208d69d24a9dc9e066e381f1601bc8e109be Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 4 Apr 2017 17:14:20 +0000 Subject: [PATCH] advances non lfsx ... --- .../basic_2/rt_computation/lfsx.ma | 59 ++++------------ .../basic_2/rt_computation/lfsx_lfsx.ma | 69 +++++++++++++++++++ .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 4 ++ .../lambdadelta/basic_2/static/lfxs.ma | 8 +++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + 5 files changed, 97 insertions(+), 44 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 51596c44e..2311f424c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -45,56 +45,27 @@ lemma lfsx_intro: ∀h,o,G,L1,T. (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. /5 width=1 by lfdeq_sym, SN_intro/ qed. -(* + +(* Basic_2A1: was: lsx_sort *) lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H * [ #H1 #H2 destruct // -| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct - @lfdeq_sort +| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_sort, lfxs_isid, frees_sort_gen, frees_inv_sort/ +] qed. -lemma lfsx_gref: ∀h,o,G,L,l,p. G ⊢ ⬈*[h, o, §p, l] L. -#h #o #G #L1 #l #p @lfsx_intro -#L2 #HL12 #H elim H -H -/3 width=4 by lfpx_fwd_length, lfdeq_gref/ +(* Basic_2A1: was: lsx_gref *) +lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. +#h #o #G #L1 #s @lfsx_intro +#L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H * +[ #H1 #H2 destruct // +| #I #K1 #K2 #V1 #V2 #HK12 #H1 #H2 destruct + /4 width=4 by lfdeq_gref, lfxs_isid, frees_gref_gen, frees_inv_gref/ +] qed. -(* Basic forward lemmas *****************************************************) - -lemma lfsx_fwd_bind_sn: ∀h,o,a,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L. -#h #o #a #I #G #L #V #T #l #H @(lfsx_ind … H) -L -#L1 #_ #IHL1 @lfsx_intro -#L2 #HL12 #HV @IHL1 /3 width=4 by lfdeq_fwd_bind_sn/ -qed-. - -lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L. -#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L -#L1 #_ #IHL1 @lfsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/ -qed-. - -lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, T, l] L. -#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L -#L1 #_ #IHL1 @lfsx_intro -#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/ -qed-. - -lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L. -#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → - G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L. -/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-. - -(* Basic_2A1: removed theorems 5: - lsx_atom lsx_sort lsx_gref lsx_ge_up lsx_ge -*) +(* Basic_2A1: removed theorems 2: + lsx_ge_up lsx_ge *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma new file mode 100644 index 000000000..5ea3071b0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfdeq_lfdeq.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". +include "basic_2/rt_computation/lfsx.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +axiom pippo: ∀h,o,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L & L ≡[h, o, V] L2. + +(* Advanced properties ******************************************************) + +lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. L1 ≡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +#h #o #G #L1 #T #H @(lfsx_ind … H) -L1 +#L1 #_ #IHL1 #L2 #HL12 @lfsx_intro +#L #HL2 #HnL2 elim (lfdeq_lfpx_trans … HL2 … HL12) -HL2 +/4 width=5 by lfdeq_repl/ +qed-. + +(* Advanced forward lemmas **************************************************) + +(* Basic_2A1: was: lsx_fwd_bind_sn *) +lemma lfsx_fwd_bind_sn: ∀h,o,p,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L⦄ → + G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄. +#h #o #p #I #G #L #V #T #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #H #HnL12 elim (pippo … o p I … T H) -H +/6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_bind_sn/ +qed-. +(* +lemma lfsx_fwd_flat_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L. +#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_sn/ +qed-. + +lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, T, l] L. +#h #o #I #G #L #V #T #l #H @(lfsx_ind … H) -L +#L1 #_ #IHL1 @lfsx_intro +#L2 #HL12 #HV @IHL1 /3 width=3 by lfdeq_fwd_flat_dx/ +qed-. + +lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ②{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L. +#h #o * /2 width=4 by lfsx_fwd_bind_sn, lfsx_fwd_flat_sn/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T,l. G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L → + G ⊢ ⬈*[h, o, V, l] L ∧ G ⊢ ⬈*[h, o, T, l] L. +/3 width=3 by lfsx_fwd_flat_sn, lfsx_fwd_flat_dx, conj/ qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index 71b1c0d4f..c42edd196 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -42,6 +42,10 @@ theorem lfdeq_canc_sn: ∀h,o,T. left_cancellable … (lfdeq h o T). theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T). /3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. +theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → + ∀K1. L1 ≡[h, o, T] K1 → ∀K2. L2 ≡[h, o, T] K2 → K1 ≡[h, o, T] K2. +/3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-. + (* Advanced properies on negated lazy equivalence *****************************) (* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred ************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index f754e46de..1d7781d7e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -89,6 +89,14 @@ lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ qed-. +lemma lfxs_isid: ∀R1,R2,L1,L2,T1,T2. + (∀f. L1 ⊢ 𝐅*⦃T1⦄ ≡ f → 𝐈⦃f⦄) → + (∀f. 𝐈⦃f⦄ → L1 ⊢ 𝐅*⦃T2⦄ ≡ f) → + L1 ⦻*[R1, T1] L2 → L1 ⦻*[R2, T2] L2. +#R1 #R2 #L1 #L2 #T1 #T2 #H1 #H2 * +/4 width=7 by lexs_co_isid, ex2_intro/ +qed-. + (* Basic inversion lemmas ***************************************************) lemma lfxs_inv_atom_sn: ∀R,Y2,T. ⋆ ⦻*[R, T] Y2 → Y2 = ⋆. 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 5019e8956..68759e53b 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 @@ -113,6 +113,7 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) + [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] -- 2.39.2