From: Ferruccio Guidi Date: Fri, 8 Jun 2018 18:27:21 +0000 (+0200) Subject: milestone update in basic_2 X-Git-Tag: make_still_working~309 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cac0166656e08399eaaf1a1e19f0ccea28c36d39;p=helm.git milestone update in basic_2 componemt rt_computation cpmpleted! --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lprs/lprs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lprs/lprs.etc new file mode 100644 index 000000000..60493eaee --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lprs/lprs.etc @@ -0,0 +1,9 @@ +lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G). +/3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-. + +(* Basic_1: was just: pr3_pr3_pr3_t *) +(* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *) +lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G). +#G @b_c_to_b_rs_trans @b_c_trans_CTC2 +@b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma index 721330c1b..1ea7cc963 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/lpr_lpr.ma". include "basic_2/rt_computation/cpms_lpr.ma". include "basic_2/rt_computation/cprs_cpr.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma index c06e0278d..827a963be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs.ma @@ -27,20 +27,53 @@ interpretation (* Basic properties *********************************************************) -lemma lprs_refl (h) (G): ∀L. ⦃G, L⦄ ⊢ ➡*[h] L. -/2 width=1 by lex_refl/ qed. - (* Basic_2A1: uses: lprs_pair_refl *) lemma lprs_bind_refl_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ∀I. ⦃G, L1.ⓘ{I}⦄ ⊢ ➡*[h] L2.ⓘ{I}. /2 width=1 by lex_bind_refl_dx/ qed. +lemma lprs_pair (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → + ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡*[h] V2 → + ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2.ⓑ{I}V2. +/2 width=1 by lex_pair/ qed. + +lemma lprs_refl (h) (G): ∀L. ⦃G, L⦄ ⊢ ➡*[h] L. +/2 width=1 by lex_refl/ qed. + (* Basic inversion lemmas ***************************************************) (* Basic_2A1: uses: lprs_inv_atom1 *) lemma lprs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ➡*[h] L2 → L2 = ⋆. /2 width=2 by lex_inv_atom_sn/ qed-. +(* Basic_2A1: was: lprs_inv_pair1 *) +lemma lprs_inv_pair_sn (h) (G): + ∀I,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 & L2 = K2.ⓑ{I}V2. +/2 width=1 by lex_inv_pair_sn/ qed-. + (* Basic_2A1: uses: lprs_inv_atom2 *) lemma lprs_inv_atom_dx (h) (G): ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] ⋆ → L1 = ⋆. /2 width=2 by lex_inv_atom_dx/ qed-. + +(* Basic_2A1: was: lprs_inv_pair2 *) +lemma lprs_inv_pair_dx (h) (G): + ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 & L1 = K1.ⓑ{I}V1. +/2 width=1 by lex_inv_pair_dx/ qed-. + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: was: lprs_ind_alt *) +lemma lprs_ind (h) (G): ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2. + ⦃G, K1⦄ ⊢ ➡*[h] K2 → + R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I}) + ) → ( + ∀I,K1,K2,V1,V2. + ⦃G, K1⦄ ⊢ ➡*[h] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h] V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → R L1 L2. +/3 width=4 by lex_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma new file mode 100644 index 000000000..b16c21601 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cpms.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/lprs_lpr.ma". + +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) + +(* Properties with t-bound context-sensitive rt-computarion for terms *******) + +lemma lprs_cpms_trans (n) (h) (G): + ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[n, h] T2 → + ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2. +#n #h #G #L2 #T1 #T2 #HT12 #L1 #H +@(lprs_ind_sn … H) -L1 /2 width=3 by lpr_cpms_trans/ +qed-. + +lemma lprs_cpm_trans (n) (h) (G): + ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 → + ∀L1. ⦃G, L1⦄ ⊢ ➡*[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2. +/3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-. + +(* Basic_2A1: includes cprs_bind2 *) +lemma cpms_bind_dx (n) (h) (G) (L): + ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡*[n, h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2. +/4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed. + +(* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *) + +(* Basic_1: was: pr3_gen_abst *) +(* Basic_2A1: includes: cprs_inv_abst1 *) +(* Basic_2A1: uses: scpds_inv_abst1 *) +lemma cpms_inv_abst_sn (n) (h) (G) (L): + ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 & + X2 = ⓛ{p}V2.T2. +#n #h #G #L #p #V1 #T1 #X2 #H +@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/ +#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct +elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct +/5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/ +qed-. + +(* Basic_2A1: includes: cprs_inv_abst *) +lemma cpms_inv_abst_bi (n) (h) (G) (L): + ∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2. +#n #h #G #L #p #W1 #W2 #T1 #T2 #H +elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct +/2 width=1 by conj/ +qed-. + +(* Basic_1: was pr3_gen_abbr *) +(* Basic_2A1: includes: cprs_inv_abbr1 *) +lemma cpms_inv_abbr_sn (n) (h) (G) (L): + ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡*[n, h] X2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T2 & X2 = ⓓ{p}V2.T2 + | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n ,h] T2 & ⬆*[1] X2 ≘ T2 & p = Ⓣ. +#n #h #G #L #p #V1 #T1 #X2 #H +@(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/ +#n1 #n2 #X #X2 #_ * * +[ #V #T #HV1 #HT1 #H #HX2 destruct + elim (cpm_inv_abbr1 … HX2) -HX2 * + [ #V2 #T2 #HV2 #HT2 #H destruct + /6 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro, or_introl/ + | #T2 #HT2 #HXT2 #Hp + /6 width=7 by lprs_cpm_trans, lprs_pair, cpms_trans, ex3_intro, or_intror/ + ] +| #T #HT1 #HXT #Hp #HX2 + elim (cpm_lifts_sn … HX2 (Ⓣ) … (L.ⓓV1) … HXT) -X + /4 width=3 by cpms_step_dx, drops_refl, drops_drop, ex3_intro, or_intror/ +] +qed-. + +(* Basic_2A1: uses: scpds_inv_abbr_abst *) +lemma cpms_inv_abbr_abst (n) (h) (G) (L): + ∀p1,p2,V1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓓ{p1}V1.T1 ➡*[n, h] ⓛ{p2}W2.T2 → + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡*[n, h] T & ⬆*[1] ⓛ{p2}W2.T2 ≘ T & p1 = Ⓣ. +#n #h #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H +elim (cpms_inv_abbr_sn … H) -H * +[ #V #T #_ #_ #H destruct +| /2 width=3 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma index b910b2763..958fcab3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma @@ -12,56 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/computation/cprs_cprs.ma". -include "basic_2/computation/lprs.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". -(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) (* Advanced properties ******************************************************) -lemma lprs_pair: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2. -/2 width=1 by TC_lpx_sn_pair/ qed. +(* Basic_2A1: was: lprs_pair2 *) +lemma lprs_pair_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h] L2 → + ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h] V2 → + ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h] L2.ⓑ{I}V2. +/3 width=3 by lprs_pair, lprs_cpms_trans/ qed. -(* Advanced inversion lemmas ************************************************) +(* Properties on context-sensitive parallel r-computation for terms *********) -lemma lprs_inv_pair1: ∀I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡* L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 & - L2 = K2.ⓑ{I}V2. -/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-. - -lemma lprs_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡* K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡* K2 & ⦃G, K1⦄ ⊢ V1 ➡* V2 & - L1 = K1.ⓑ{I}V1. -/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-. - -(* Advanced eliminators *****************************************************) - -lemma lprs_ind_alt: ∀G. ∀R:relation lenv. - R (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - ⦃G, K1⦄ ⊢ ➡* K2 → ⦃G, K1⦄ ⊢ V1 ➡* V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → R L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ qed-. - -(* Properties on context-sensitive parallel computation for terms ***********) - -lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G). -/3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-. - -(* Basic_1: was just: pr3_pr3_pr3_t *) -(* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *) -lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G). -#G @b_c_to_b_rs_trans @b_c_trans_CTC2 -@b_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 @(lprs_ind … H) -L1 /2 width=3 by ex2_intro/ +lemma lprs_cprs_conf_dx (h) (G): ∀L0.∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡*[h] T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T. +#h #G #L0 #T0 #T1 #HT01 #L1 #H +@(lprs_ind_dx … 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 @@ -69,112 +39,21 @@ 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 → - ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. -/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-. +lemma lprs_cpr_conf_dx (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T. +/3 width=3 by lprs_cprs_conf_dx, cpm_cpms/ 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 +(* Note: this can be proved on its own using lprs_ind_sn *) +lemma lprs_cprs_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡*[h] T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T. +#h #G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 -/3 width=3 by lprs_cprs_trans, ex2_intro/ +/3 width=3 by lprs_cpms_trans, ex2_intro/ qed-. -lemma lprs_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → - ∀L1. ⦃G, L0⦄ ⊢ ➡* L1 → - ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡* T & ⦃G, L1⦄ ⊢ T0 ➡* T. -/3 width=3 by lprs_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=5 by lprs_cprs_trans, lprs_pair, cprs_bind/ qed. - -(* Inversion lemmas on context-sensitive parallel computation for terms *****) - -(* Basic_1: was: pr3_gen_abst *) -lemma cprs_inv_abst1: ∀a,G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* U2 → - ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 & - U2 = ⓛ{a}W2.T2. -#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) ?) -/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/ -qed-. - -(* Basic_1: was pr3_gen_abbr *) -lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & - U2 = ⓓ{a}V2.T2 - ) ∨ - ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 & ⬆[0, 1] U2 ≘ T2 & a = true. -#a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ -#U0 #U2 #_ #HU02 * * -[ #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) ?) - /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 - /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 - /4 width=3 by cprs_strap1, drop_drop, ex3_intro, or_intror/ -] -qed-. - -(* More advanced properties *************************************************) - -lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2. -/3 width=3 by lprs_pair, lprs_cprs_trans/ qed. - -(* Advanced inversion lemmas ************************************************) - -(* Basic_2A1: uses: scpds_inv_abst1 *) -lemma cpms_inv_abst_sn (n) (h) (G) (L): - ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 & - X2 = ⓛ{p}V2.T2. -#n #h #G #L #p #V1 #T1 #X2 #H -@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/ -#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct -elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct -@ex3_2_intro [1,2,5: // ] -[ /2 width=3 by cprs_step_dx/ -| @(cpms_trans … HT1) -T1 -V2 -n1 - -/3 width=5 by cprs_step_dx, cpms_step_dx, ex3_2_intro/ - - - -#d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct -elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct -/3 width=6 by ex4_2_intro, ex3_2_intro/ -qed-. - -lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 → - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true. -#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct -elim (cprs_inv_abbr1 … H2) -H2 * -[ #V2 #U2 #HV12 #HU12 #H destruct -| /3 width=6 by ex4_2_intro, ex3_intro/ -] -qed-. -*) +lemma lprs_cpr_conf_sn (h) (G): ∀L0. ∀T0,T1:term. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h] L1 → + ∃∃T. ⦃G, L0⦄ ⊢ T1 ➡*[h] T & ⦃G, L1⦄ ⊢ T0 ➡*[h] T. +/3 width=3 by lprs_cprs_conf_sn, cpm_cpms/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma index 91ad13808..e442a66b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lpr.ma @@ -12,9 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lex_tc.ma". -include "basic_2/rt_computation/cprs_lpr.ma". -include "basic_2/rt_computation/lprs_ctc.ma". +include "basic_2/rt_computation/lprs_tc.ma". (* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) @@ -46,3 +44,12 @@ lemma lprs_step_sn (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ➡[h] L → lemma lprs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ➡*[h] L → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ ➡*[h] L2. /4 width=3 by lprs_inv_CTC, lprs_CTC, lpr_cprs_trans, lex_CTC_step_dx/ qed-. + +lemma lprs_strip (h) (G): confluent2 … (lprs h G) (lpr h G). +#h #G #L0 #L1 #HL01 #L2 #HL02 +elim (TC_strip1 … L1 ?? HL02) -HL02 +[ /3 width=3 by lprs_TC, ex2_intro/ | skip +| /2 width=1 by lprs_inv_TC/ +| /2 width=3 by lpr_conf/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma index 1bb611012..ae645f6aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_lprs.ma @@ -12,20 +12,22 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpr_lpr.ma". -include "basic_2/computation/lprs.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". -(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) - -(* Advanced properties ******************************************************) - -lemma lprs_strip: ∀G. confluent2 … (lprs G) (lpr G). -/3 width=3 by TC_strip1, lpr_conf/ qed-. +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) (* Main properties **********************************************************) -theorem lprs_conf: ∀G. confluent2 … (lprs G) (lprs G). -/3 width=3 by TC_confluent2, lpr_conf/ qed-. +theorem lprs_trans (h) (G): Transitive … (lprs h G). +/4 width=5 by lprs_cpms_trans, cprs_trans, lex_trans/ qed-. -theorem lprs_trans: ∀G. Transitive … (lprs G). -/2 width=3 by trans_TC/ qed-. +theorem lprs_conf (h) (G): confluent2 … (lprs h G) (lprs h G). +#h #G #L0 #L1 #HL01 #L2 #HL02 +elim (TC_confluent2 … L0 L1 … L2) +[ /3 width=3 by lprs_TC, ex2_intro/ |5,6: skip +| /2 width=1 by lprs_inv_TC/ +| /2 width=1 by lprs_inv_TC/ +| /2 width=3 by lpr_conf/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma new file mode 100644 index 000000000..cec8e47f5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_tc.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lex_tc.ma". +include "basic_2/rt_computation/lprs_ctc.ma". +include "basic_2/rt_computation/cprs_lpr.ma". + +(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************) + +(* Properties with transitive closure ***************************************) + +lemma lprs_TC (h) (G): + ∀L1,L2. TC … (lex (λL.cpm h G L 0)) L1 L2 → ⦃G, L1⦄⊢ ➡*[h] L2. +/4 width=3 by lprs_CTC, lex_CTC, lpr_cprs_trans/ qed. + +(* Inversion lemmas with transitive closure *********************************) + +lemma lprs_inv_TC (h) (G): + ∀L1,L2. ⦃G, L1⦄⊢ ➡*[h] L2 → TC … (lex (λL.cpm h G L 0)) L1 L2. +/3 width=3 by lprs_inv_CTC, lex_inv_CTC/ 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 index d6538eb9f..9375fee8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -46,13 +46,13 @@ lemma lpxs_refl (h) (G): reflexive … (lpxs h G). lemma lpxs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ⬈*[h] L2 → L2 = ⋆. /2 width=2 by lex_inv_atom_sn/ qed-. -lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 → - ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}. +lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢ ⬈*[h] L2 → + ∃∃I2,K2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}. /2 width=1 by lex_inv_bind_sn/ qed-. (* Basic_2A1: was: lpxs_inv_pair1 *) -lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2. +lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2. /2 width=1 by lex_inv_pair_sn/ qed-. (* Basic_2A1: was: lpxs_inv_atom2 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt deleted file mode 100644 index fb1ffd58a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ /dev/null @@ -1,14 +0,0 @@ -cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_cnx.ma cpxs_cpxs.ma -cpxs_ext.ma -lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma -csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lpxs.ma csx_csx.ma -csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma -rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma -lsubsx.ma lsubsx_rdsx.ma lsubsx_lsubsx.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_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma -fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma -fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma -cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_lpr.ma cpms_cpxs.ma cpms_cpms.ma -cprs.ma cprs_ctc.ma cprs_drops.ma cprs_cpr.ma cprs_lpr.ma cprs_cprs.ma -cprs_ext.ma -lprs.ma lprs_ctc.ma lprs_length.ma lprs_drops.ma lprs_aaa.ma lprs_lpr.ma lprs_lpxs.ma 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 8bfc16d8e..39ffd838a 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" + + Behavioral component rt_computation completed. + "Big tree" theorem (anniversary milestone). @@ -52,8 +55,7 @@ (anniversary milestone). - First behavioral component completed: - rt_transition. + Behavioral component rt_transition completed. Generic candidates of reducibility. 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 71e720142..b82479065 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 @@ -73,7 +73,7 @@ table { ] *) [ { "context-sensitive parallel r-computation" * } { - [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" (* + "lprs_cprs" + "lprs_lprs" *) * ] + [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ] [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ] [ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_ctc" + "cprs_drops" + "cprs_cpr" + "cprs_lpr" + "cprs_cprs" * ] } diff --git a/matita/matita/contribs/lambdadelta/compile_partial.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh index 59b18afc7..4ed7b622d 100644 --- a/matita/matita/contribs/lambdadelta/compile_partial.sh +++ b/matita/matita/contribs/lambdadelta/compile_partial.sh @@ -1,7 +1,5 @@ ../../matitac.opt `cat partial.txt` -cd basic_2/rt_computation/ -../../../../matitac.opt `cat partial.txt` -cd ../rt_equivalence/ +cd basic_2/rt_equivalence/ ../../../../matitac.opt `cat partial.txt` cd ../dynamic/ ../../../../matitac.opt `cat partial.txt` diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 54e9d27e5..12e10e1fe 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -6,6 +6,7 @@ basic_2/s_computation basic_2/static basic_2/i_static basic_2/rt_transition +basic_2/rt_computation basic_2/rt_conversion apps_2/examples/ex_cpr_omega.ma apps_2/models/