From: Ferruccio Guidi Date: Tue, 27 Mar 2018 13:29:01 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~347 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=97c627e9d169b5df0308d440a449a6853108f372 update in basic_2 + last property of fpbs proved --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index 27fd06b7b..8dc5a03a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -53,8 +53,8 @@ lemma fqus_cpxs_trans: ∀h,b,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 #U1 #HTU1 #H2 elim (IHTU2 … H2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ qed-. -(* Note: a proof based on fqu_cpx_trans_ntdeq might exist *) -lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → +(* Note: a proof based on fqu_cpx_trans_tdneq might exist *) +lemma fqu_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 @@ -86,33 +86,33 @@ lemma fqu_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ] qed-. -lemma fquq_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → +lemma fquq_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 -[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 +[ #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. -lemma fqup_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → +lemma fqup_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 - #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_ntdeq … H1 … HTU1 H) -T1 + #U1 #HTU1 #H #H12 elim (fqu_cpxs_trans_tdneq … H1 … HTU1 H) -T1 /3 width=8 by fqup_strap2, ex3_intro/ ] qed-. -lemma fqus_cpxs_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → +lemma fqus_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 -[ #H12 elim (fqup_cpxs_trans_ntdeq … H12 … HTU2 H) -T2 +[ #H12 elim (fqup_cpxs_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma new file mode 100644 index 000000000..9677e98ee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpx.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_ffdeq.ma". +include "basic_2/rt_computation/lpxs_cpxs.ma". +include "basic_2/rt_computation/fpbs_lpxs.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with uncounted context-sensitive parallel rt-transition *******) + +(* Basic_2A1: uses: fpbs_cpx_trans_neq *) +lemma fpbs_cpx_tdneq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, o] ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 +elim (fpbs_inv_star … H) -H #G0 #L0 #L3 #T0 #T3 #HT10 #H10 #HL03 #H32 +elim (ffdeq_cpx_trans … H32 … HTU2) -HTU2 #T4 #HT34 #H42 +lapply (ffdeq_tdneq_repl_dx … H32 … H42 … HnTU2) -T2 #HnT34 +lapply (lpxs_cpx_trans … HT34 … HL03) -HT34 #HT34 +elim (fqus_cpxs_trans_tdneq … H10 … HT34 HnT34) -T3 #T2 #HT02 #HnT02 #H24 +elim (tdeq_dec h o T1 T0) [ #H10 | -HnT02 #HnT10 ] +[ lapply (cpxs_trans … HT10 … HT02) -HT10 -HT02 #HT12 + elim (cpxs_tdneq_fwd_step_sn … o … HT12) [2: /3 width=3 by tdeq_canc_sn/ ] -T0 -HT12 +| elim (cpxs_tdneq_fwd_step_sn … HT10 … HnT10) -HT10 -HnT10 +] +/4 width=16 by fpbs_intro_star, cpxs_tdeq_fpbs_trans, ex3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma index 8500d2ddd..9269fd393 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_cpxs.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/ffdeq_fqup.ma". include "basic_2/rt_computation/cpxs.ma". include "basic_2/rt_computation/fpbs_fqup.ma". @@ -37,6 +36,11 @@ lemma cpxs_fpbs_trans: ∀h,o,G1,G2,L1,L2,T,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, /3 width=5 by fpbs_strap2, fpbq_cpx/ qed-. +lemma cpxs_tdeq_fpbs_trans: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀T0. T ≛[h, o] T0 → + ∀G2,L2,T2. ⦃G1, L1, T0⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=3 by cpxs_fpbs_trans, tdeq_fpbs_trans/ qed-. + lemma cpxs_tdeq_fpbs: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬈*[h] T → ∀T2. T ≛[h, o] T2 → ⦃G, L, T1⦄ ≥[h, o] ⦃G, L, T2⦄. /4 width=3 by cpxs_fpbs_trans, ffdeq_fpbs, tdeq_ffdeq/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma index af425aa48..4cef4f396 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_fqup.ma @@ -13,10 +13,17 @@ (**************************************************************************) include "basic_2/s_computation/fqus_fqup.ma". +include "basic_2/static/ffdeq_fqup.ma". include "basic_2/rt_computation/fpbs_fqus.ma". (* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) +(* Advanced properties ******************************************************) + +lemma tdeq_fpbs_trans: ∀h,o,T1,T. T1 ≛[h, o] T → + ∀G1,G2,L1,L2,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄. +/3 width=5 by ffdeq_fpbs_trans, tdeq_ffdeq/ qed-. + (* Properties with plus-iterated structural successor for closures **********) lemma fqup_fpbs: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma index 3c0e8e372..5a8c400b5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma @@ -66,19 +66,17 @@ lemma cpxs_fqus_lfpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → (* Advanced properties ******************************************************) -(* Basic_2A1: uses: fpbs_intro_alt *) -lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → - ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ → - ∀L0. ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 → - ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ . +lemma fpbs_intro_fstar: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ → + ∀L0. ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 → + ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ . /3 width=5 by cpxs_fqus_lfpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed. (* Advanced inversion lemmas *************************************************) -(* Basic_2A1: uses: fpbs_inv_alt *) -lemma fpbs_inv_star: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → - ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ - & ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +lemma fpbs_inv_fstar: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ + & ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 [ /2 width=9 by ex4_5_intro/ | #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma new file mode 100644 index 000000000..8a0a18405 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lfeq.ma". +include "basic_2/rt_computation/lfpxs_lpxs.ma". +include "basic_2/rt_computation/fpbs_lfpxs.ma". + +(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************) + +(* Properties with uncounted parallel rt-computation on local environments **) + +(* Basic_2A1: uses: fpbs_intro_alt *) +lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T → + ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ → + ∀L0. ⦃G, L⦄ ⊢ ⬈*[h] L0 → + ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ . +/3 width=9 by fpbs_intro_fstar, lfpxs_lpxs/ qed. + +(* Eliminators with uncounted parallel rt-computation on local environments *) + +(* Basic_2A1: uses: fpbs_inv_alt *) +lemma fpbs_inv_star: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ → + ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ + & ⦃G, L⦄ ⊢ ⬈*[h] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H +elim (fpbs_inv_fstar … H) -H #G #L #L0 #T #T0 #HT1 #H10 #HL0 #H02 +elim (lfpxs_inv_lpxs_lfeq … HL0) -HL0 #L3 #HL3 #HL30 +/3 width=11 by lfeq_lfdeq_trans, ex4_5_intro/ +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 c92ce8415..fc893a1d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -6,6 +6,6 @@ csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma cs csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma -fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma +fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma fsb.ma fsb_ffdeq.ma fsb_fpbg.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma new file mode 100644 index 000000000..3b029ea5a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ffdeq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/cpx_lfdeq.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) + +(* Properties with degree-based equivalence for closures ********************) + +lemma ffdeq_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T⦄ → + ∀T2. ⦃G2, L2⦄ ⊢ T ⬈[h] T2 → + ∃∃T0. ⦃G1, L1⦄ ⊢ T1 ⬈[h] T0 & ⦃G1, L1, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T #H #T2 #HT2 +elim (ffdeq_inv_gen_dx … H) -H #H #HL12 #HT1 destruct +elim (lfdeq_cpx_trans … HL12 … HT2) #T0 #HT0 #HT02 +lapply (cpx_lfdeq_conf_dx … HT2 … HL12) -HL12 #HL12 +elim (tdeq_cpx_trans … HT1 … HT0) -T #T #HT1 #HT0 +/4 width=5 by ffdeq_intro_dx, tdeq_trans, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 0744bd0fc..06a3573c0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -66,7 +66,7 @@ lemma fqus_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, ] qed-. -lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → +lemma fqu_cpx_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 @@ -98,33 +98,33 @@ lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ] qed-. -lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → +lemma fquq_cpx_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 -[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 +[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. -lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → +lemma fqup_cpx_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 - #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_ntdeq … H1 … HTU1 H) -T1 + #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_tdneq … H1 … HTU1 H) -T1 /3 width=8 by fqup_strap2, ex3_intro/ ] qed-. -lemma fqus_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → +lemma fqus_cpx_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≛[h, o] U2 → ⊥) → ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. #h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 -[ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2 +[ #H12 elim (fqup_cpx_trans_tdneq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma index 40a805259..cbd1284ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_ffdeq.ma @@ -39,3 +39,14 @@ theorem ffdeq_canc_sn: ∀h,o,G,G1,G2,L,L1,L2,T,T1,T2. theorem ffdeq_canc_dx: ∀h,o,G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G2, L2, T2⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. /3 width=5 by ffdeq_trans, ffdeq_sym/ qed-. + +(* Main inversion lemmas with degree-based equivalence on terms *************) + +theorem ffdeq_tdneq_repl_dx: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → + ∀U1,U2. ⦃G1, L1, U1⦄ ≛[h, o] ⦃G2, L2, U2⦄ → + (T2 ≛[h, o] U2 → ⊥) → (T1 ≛[h, o] U1 → ⊥). +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #HT #U1 #U2 #HU #HnTU2 #HTU1 +elim (ffdeq_inv_gen_sn … HT) -HT #_ #_ #HT +elim (ffdeq_inv_gen_sn … HU) -HU #_ #_ #HU +/3 width=5 by tdeq_repl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_lfeq.ma new file mode 100644 index 000000000..e0453bf32 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq_lfeq.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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_lfeq.ma". +include "basic_2/static/ffdeq.ma". + +(* DEGREE-BASED EQUIVALENCE FOR CLOSURES ON REFERRED ENTRIES ****************) + +(* Properties with syntactic equivalence on referred entries ****************) + +lemma lfeq_lfdeq_trans: ∀h,o,L1,L,T1. L1 ≐[T1] L → + ∀G1,G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #L1 #L #T1 #HL1 #G1 #G2 #L2 #T2 #H +elim (ffdeq_inv_gen_sn … H) -H #H #HL2 #T12 destruct +/3 width=3 by ffdeq_intro_sn, lfeq_lfdeq_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma index 5682e7218..8d13d1984 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma @@ -12,12 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/static/lfeq.ma". +include "basic_2/static/lfeq_fsle.ma". include "basic_2/static/lfdeq.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) (* Properties with syntactic equivalence on referred entries ****************) -lemma lfeq_lfdeq: ∀h,o,L1,L2,T. L1 ≐[T] L2 → L1 ≛[h, o, T] L2. +lemma lfeq_lfdeq: ∀h,o,L1,L2. ∀T:term. L1 ≐[T] L2 → L1 ≛[h, o, T] L2. /2 width=3 by lfxs_co/ qed. + +lemma lfeq_lfdeq_trans: ∀h,o,L1,L. ∀T:term. L1 ≐[T] L → + ∀L2. L ≛[h, o, T] L2 → L1 ≛[h, o, T] L2. +/2 width=3 by lfeq_lfxs_trans/ 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 c56156618..6e484843a 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 @@ -87,7 +87,7 @@ table { [ { "uncounted context-sensitive parallel rst-computation" * } { [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ] [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ] - [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ] + [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } ] [ { "uncounted context-sensitive parallel rt-computation" * } { @@ -125,7 +125,7 @@ table { [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fquq" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] - [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ] + [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" + "cpx_ffdeq" * ] } ] [ { "counted context-sensitive parallel rt-transition" * } { @@ -156,7 +156,7 @@ table { } ] [ { "degree-based equivalence" * } { - [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_fqus" + "ffdeq_ffdeq" * ] + [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_fqus" + "ffdeq_lfeq" + "ffdeq_ffdeq" * ] [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfeq" + "lfdeq_lfdeq" * ] } ]