From: Ferruccio Guidi Date: Fri, 11 May 2018 19:28:42 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~321 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d02c188ee3d4bd9885490447e63453adb2cb4ea1 update in basic_2 + first file on r-equivalence + renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma deleted file mode 100644 index 75964c615..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs.ma +++ /dev/null @@ -1,96 +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/pconvstar_4.ma". -include "basic_2/conversion/cpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -definition cpcs: relation4 genv lenv term term ≝ - λG. CTC … (cpc G). - -interpretation "context-sensitive parallel equivalence (term)" - 'PConvStar G L T1 T2 = (cpcs G L T1 T2). - -(* Basic eliminators ********************************************************) - -lemma cpcs_ind: ∀G,L,T1. ∀R:predicate term. R T1 → - (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → R T → R T2) → - ∀T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T2. -normalize /3 width=6 by TC_star_ind/ -qed-. - -lemma cpcs_ind_dx: ∀G,L,T2. ∀R:predicate term. R T2 → - (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → R T → R T1) → - ∀T1. ⦃G, L⦄ ⊢ T1 ⬌* T2 → R T1. -normalize /3 width=6 by TC_star_ind_dx/ -qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was: pc3_refl *) -lemma cpcs_refl: ∀G,L. reflexive … (cpcs G L). -/2 width=1 by inj/ qed. - -(* Basic_1: was: pc3_s *) -lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L). -normalize /3 width=1 by cpc_sym, TC_symmetric/ -qed-. - -lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/2 width=1 by inj/ qed. - -lemma cpcs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -normalize /2 width=3 by step/ -qed-. - -lemma cpcs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌ T → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -normalize /2 width=3 by TC_strap/ -qed-. - -(* Basic_1: was: pc3_pr2_r *) -lemma cpr_cpcs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=1 by cpc_cpcs, or_introl/ qed. - -(* Basic_1: was: pc3_pr2_x *) -lemma cpr_cpcs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡ T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=1 by cpc_cpcs, or_intror/ qed. - -lemma cpcs_cpr_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap1, or_introl/ qed-. - -(* Basic_1: was: pc3_pr2_u *) -lemma cpcs_cpr_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap2, or_introl/ qed-. - -lemma cpcs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap1, or_intror/ qed-. - -lemma cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpr_cpcs_dx, cpcs_strap1, or_intror/ qed-. - -(* Basic_1: was: pc3_pr2_u2 *) -lemma cpcs_cpr_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_strap2, or_intror/ qed-. - -(* Basic_1: removed theorems 9: - clear_pc3_trans pc3_ind_left - pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 - pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0 - pc3_gen_abst pc3_gen_abst_shift -*) -(* Basic_1: removed local theorems 6: - pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left - pc3_wcpr0_t_aux -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma deleted file mode 100644 index 4f9223886..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma +++ /dev/null @@ -1,30 +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/computation/cpxs_aaa.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Main inversion lemmas about atomic arity assignment on terms *************) - -theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → - A1 = A2. -#G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 -elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -lapply (cprs_aaa_conf … HA1 … HT1) -T1 #HA1 -lapply (cprs_aaa_conf … HA2 … HT2) -T2 #HA2 -lapply (aaa_mono … HA1 … HA2) -L -T // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma deleted file mode 100644 index 7b9645afa..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cpcs.ma +++ /dev/null @@ -1,212 +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/computation/lprs_cprs.ma". -include "basic_2/conversion/cpc_cpc.ma". -include "basic_2/equivalence/cpcs_cprs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Advanced inversion lemmas ************************************************) - -lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. -#G #L #T1 #T2 #H @(cpcs_ind … H) -T2 -[ /3 width=3 by ex2_intro/ -| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 - [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ - | /3 width=5 by cprs_strap2, ex2_intro/ - ] -] -qed-. - -(* Basic_1: was: pc3_gen_sort *) -lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2. -#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H -#T #H1 >(cprs_inv_sort1 … H1) -T #H2 -lapply (cprs_inv_sort1 … H2) -L #H destruct // -qed-. - -lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T → - ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. -#a #G #L #W1 #T1 #T #H -elim (cpcs_inv_cprs … H) -H #X #H1 #H2 -elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct -/3 width=6 by cprs_bind, ex2_2_intro/ -qed-. - -lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 → - ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. -/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-. - -(* Basic_1: was: pc3_gen_sort_abst *) -lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥. -#a #G #L #W #T #s #H -elim (cpcs_inv_cprs … H) -H #X #H1 ->(cprs_inv_sort1 … H1) -X #H2 -elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct -qed-. - -(* Basic_1: was: pc3_gen_lift *) -lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → - ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2. -#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 -elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 -elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 -elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU ->(lift_inj … HXU … HTU) -X -U -l -k /2 width=3 by cprs_div/ -qed-. - -(* Advanced properties ******************************************************) - -lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H -/4 width=5 by cprs_div, lpr_cprs_trans/ -qed-. - -lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H -/4 width=5 by cprs_div, lprs_cprs_trans/ -qed-. - -lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cpr_cprs_div/ -qed-. - -lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cprs_cpr_div/ -qed-. - -lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 -/2 width=3 by cprs_div/ -qed-. - -lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 -/2 width=3 by cprs_div/ -qed-. - -(* Basic_1: was: pc3_wcpr0_t *) -(* Basic_1: note: pc3_wcpr0_t should be renamed *) -(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *) -lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1 -/2 width=3 by cprs_div/ -qed-. - -(* Basic_1: was only: pc3_pr0_pr2_t *) -(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) -lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -/3 width=5 by lpr_cprs_conf, cpr_cprs/ qed-. - -(* Basic_1: was only: pc3_thin_dx *) -lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 -elim (cpcs_inv_cprs … HV12) -HV12 -elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_flat, cprs_div/ -qed. - -lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → - ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. -/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. - -lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2. -#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_div, cprs_bind/ -qed. - -lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. -#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 -/3 width=5 by cprs_div, cprs_bind/ -qed. - -lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → - ∀L2. L2 ⫃ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 -/3 width=5 by cprs_div, lsubr_cprs_trans/ -qed-. - -(* Basic_1: was: pc3_lift *) -lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → - ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → - ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. -#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 -elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 -elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/ -qed. - -lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 → - ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0. -#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-. - -(* More inversion lemmas ****************************************************) - -(* Note: there must be a proof suitable for llpr *) -lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → - ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2. -#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct -elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct -lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 -lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 -/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ -qed-. - -lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → - ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2. -#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 -#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ -qed-. - -(* Main properties **********************************************************) - -(* Basic_1: was pc3_t *) -theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. - -theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed-. - -theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cpcs_sym/ qed-. - -lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → - ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. - -lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → - ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 → - ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. -/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. - -(* Basic_1: was: pc3_wcpr0 *) -lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. -#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H -/3 width=5 by cpcs_canc_dx, lpr_cprs_conf/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma deleted file mode 100644 index d9db0509f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_cprs.ma +++ /dev/null @@ -1,62 +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/computation/cprs.ma". -include "basic_2/equivalence/cpcs.ma". - -(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) - -(* Properties about context sensitive computation on terms ******************) - -(* Basic_1: was: pc3_pr3_r *) -lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind … H) -T2 -/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/ -qed. - -(* Basic_1: was: pc3_pr3_x *) -lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 -/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/ -qed. - -lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/ -qed-. - -lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/ -qed-. - -lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/ -qed-. - -(* Basic_1: was: pc3_pr3_conf *) -lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/ -qed-. - -(* Basic_1: was: pc3_pr3_t *) -(* Basic_1: note: pc3_pr3_t should be renamed *) -lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 -/2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/ -qed. - -lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=5 by cpr_cprs, cprs_div/ qed-. - -lemma cpr_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. -/3 width=3 by cpr_cprs, cprs_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma deleted file mode 100644 index 657763483..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes.ma +++ /dev/null @@ -1,37 +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/dpconvstar_8.ma". -include "basic_2/computation/scpds.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ - λh,o,d1,d2,G,L,T1,T2. - ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T. - -interpretation "stratified decomposed parallel equivalence (term)" - 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2). - -(* Basic properties *********************************************************) - -lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2. - ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → - ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/2 width=3 by ex2_intro/ qed. - -lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1. -#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma deleted file mode 100644 index f42ebdbc9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_aaa.ma +++ /dev/null @@ -1,29 +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/computation/scpds_aaa.ma". -include "basic_2/equivalence/scpes.ma". - -(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) - -(* Main inversion lemmas about atomic arity assignment on terms *************) - -theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → - A1 = A2. -#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 -lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1 -lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2 -lapply (aaa_mono … HA1 … HA2) -L -T // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma deleted file mode 100644 index f8ef46db1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_cpcs.ma +++ /dev/null @@ -1,39 +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/computation/scpds_scpds.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/scpes.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -(* Inversion lemmas on parallel equivalence for terms ***********************) - -lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → - ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 → - ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. -#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2 -/3 width=8 by scpds_inv_lstas_eq, cprs_div/ -qed-. - -(* Properties on parallel equivalence for terms *****************************) - -lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → - ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 → - ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 → - ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 → - ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2. -#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12 -elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma deleted file mode 100644 index 24ea20ec0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma +++ /dev/null @@ -1,69 +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/computation/scpds_scpds.ma". -include "basic_2/equivalence/scpes.ma". - -(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) - -(* Advanced inversion lemmas ************************************************) - -lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 → - ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & - ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T. -#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H -elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/ -qed-. - -(* Advanced properties ******************************************************) - -lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → - ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T. -#h #o #G #L #T #d1 #d2 #Hd21 #Hd1 -elim (da_lstas … Hd1 … d2) #U #HTU #_ -/3 width=3 by scpds_div, lstas_scpds/ -qed. - -lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 → - ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T → - ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2. -#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 * -/3 width=3 by scpds_div, lstas_scpds_trans/ qed-. - -(* Properties on parallel computation for terms *****************************) - -lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → - ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d → - ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → - ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2. -#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0) -#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1 -/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/ -qed. - -(* Main properties **********************************************************) - -theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → - ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2 -elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/ -qed-. - -theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 → - ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/3 width=4 by scpes_trans, scpes_sym/ qed-. - -theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → - ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. -/3 width=4 by scpes_trans, scpes_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma index 4c9e62514..40765b785 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconv_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌ [ break term 46 h ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌[ break term 46 h ] break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma deleted file mode 100644 index f263e5d06..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_4.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌* break term 46 T2 )" - non associative with precedence 45 - for @{ 'PConvStar $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma new file mode 100644 index 000000000..83f5e2cbd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pconvstar_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌*[ break term 46 h ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PConvStar $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma new file mode 100644 index 000000000..8fc12c258 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs.ma @@ -0,0 +1,104 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/lib/star.ma". +include "basic_2/notation/relations/pconvstar_5.ma". +include "basic_2/rt_conversion/cpc.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************) + +definition cpcs: sh → relation4 genv lenv term term ≝ + λh,G. CTC … (cpc h G). + +interpretation "context-sensitive parallel r-equivalence (term)" + 'PConvStar h G L T1 T2 = (cpcs h G L T1 T2). + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: was: cpcs_ind_dx *) +lemma cpcs_ind_sn (h): ∀G,L,T2. ∀R:predicate term. R T2 → + (∀T1,T. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → R T → R T1) → + ∀T1. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T1. +normalize /3 width=6 by TC_star_ind_dx/ +qed-. + +(* Basic_2A1: was: cpcs_ind *) +lemma cpcs_ind_dx (h): ∀G,L,T1. ∀R:predicate term. R T1 → + (∀T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → R T → R T2) → + ∀T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T2 → R T2. +normalize /3 width=6 by TC_star_ind/ +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was: pc3_refl *) +lemma cpcs_refl (h): ∀G. c_reflexive … (cpcs h G). +/2 width=1 by inj/ qed. + +(* Basic_1: was: pc3_s *) +lemma cpcs_sym (h): ∀G,L. symmetric … (cpcs h G L). +#h #G #L @TC_symmetric +/2 width=1 by cpc_sym/ +qed-. + +lemma cpc_cpcs (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/2 width=1 by inj/ qed. + +(* Basic_2A1: was: cpcs_strap2 *) +lemma cpcs_step_sn (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T → ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +normalize /2 width=3 by TC_strap/ +qed-. + +(* Basic_2A1: was: cpcs_strap1 *) +lemma cpcs_step_dx (h): ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ⦃G, L⦄ ⊢ T ⬌[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +normalize /2 width=3 by step/ +qed-. + +(* Basic_1: was: pc3_pr2_r *) +lemma cpr_cpcs_dx (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=1 by cpc_cpcs, or_introl/ qed. + +(* Basic_1: was: pc3_pr2_x *) +lemma cpr_cpcs_sn (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡[h] T1 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=1 by cpc_cpcs, or_intror/ qed. + +(* Basic_1: was: pc3_pr2_u *) +(* Basic_2A1: was: cpcs_cpr_strap2 *) +lemma cpcs_cpr_step_sn (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_sn, or_introl/ qed-. + +(* Basic_2A1: was: cpcs_cpr_strap1 *) +lemma cpcs_cpr_step_dx (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_dx, or_introl/ qed-. + +lemma cpcs_cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌*[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_dx, or_intror/ qed-. + +lemma cpr_div (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡[h] T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡[h] T → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-. + +(* Basic_1: was: pc3_pr2_u2 *) +lemma cpcs_cpr_conf (h): ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌*[h] T2 → ⦃G, L⦄ ⊢ T1 ⬌*[h] T2. +/3 width=3 by cpcs_step_sn, or_intror/ qed-. + +(* Basic_1: removed theorems 9: + clear_pc3_trans pc3_ind_left + pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 + pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0 + pc3_gen_abst pc3_gen_abst_shift +*) +(* Basic_1: removed local theorems 6: + pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left + pc3_wcpr0_t_aux +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma new file mode 100644 index 000000000..4f9223886 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_aaa.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cpxs_aaa.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Main inversion lemmas about atomic arity assignment on terms *************) + +theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → + A1 = A2. +#G #L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +lapply (cprs_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (cprs_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma new file mode 100644 index 000000000..7b9645afa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma @@ -0,0 +1,212 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/lprs_cprs.ma". +include "basic_2/conversion/cpc_cpc.ma". +include "basic_2/equivalence/cpcs_cprs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Advanced inversion lemmas ************************************************) + +lemma cpcs_inv_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. +#G #L #T1 #T2 #H @(cpcs_ind … H) -T2 +[ /3 width=3 by ex2_intro/ +| #T #T2 #_ #HT2 * #T0 #HT10 elim HT2 -HT2 #HT2 #HT0 + [ elim (cprs_strip … HT0 … HT2) -T /3 width=3 by cprs_strap1, ex2_intro/ + | /3 width=5 by cprs_strap2, ex2_intro/ + ] +] +qed-. + +(* Basic_1: was: pc3_gen_sort *) +lemma cpcs_inv_sort: ∀G,L,s1,s2. ⦃G, L⦄ ⊢ ⋆s1 ⬌* ⋆s2 → s1 = s2. +#G #L #s1 #s2 #H elim (cpcs_inv_cprs … H) -H +#T #H1 >(cprs_inv_sort1 … H1) -T #H2 +lapply (cprs_inv_sort1 … H2) -L #H destruct // +qed-. + +lemma cpcs_inv_abst1: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ⬌* T → + ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +#a #G #L #W1 #T1 #T #H +elim (cpcs_inv_cprs … H) -H #X #H1 #H2 +elim (cprs_inv_abst1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct +/3 width=6 by cprs_bind, ex2_2_intro/ +qed-. + +lemma cpcs_inv_abst2: ∀a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T ⬌* ⓛ{a}W1.T1 → + ∃∃W2,T2. ⦃G, L⦄ ⊢ T ➡* ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +/3 width=1 by cpcs_inv_abst1, cpcs_sym/ qed-. + +(* Basic_1: was: pc3_gen_sort_abst *) +lemma cpcs_inv_sort_abst: ∀a,G,L,W,T,s. ⦃G, L⦄ ⊢ ⋆s ⬌* ⓛ{a}W.T → ⊥. +#a #G #L #W #T #s #H +elim (cpcs_inv_cprs … H) -H #X #H1 +>(cprs_inv_sort1 … H1) -X #H2 +elim (cprs_inv_abst1 … H2) -H2 #W0 #T0 #_ #_ #H destruct +qed-. + +(* Basic_1: was: pc3_gen_lift *) +lemma cpcs_inv_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → + ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → + ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, K⦄ ⊢ T1 ⬌* T2. +#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HU12 +elim (cpcs_inv_cprs … HU12) -HU12 #U #HU1 #HU2 +elim (cprs_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 +elim (cprs_inv_lift1 … HU2 … HLK … HTU2) -L -U2 #X #HXU +>(lift_inj … HXU … HTU) -X -U -l -k /2 width=3 by cprs_div/ +qed-. + +(* Advanced properties ******************************************************) + +lemma lpr_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, lpr_cprs_trans/ +qed-. + +lemma lprs_cpcs_trans: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → + ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/4 width=5 by cprs_div, lprs_cprs_trans/ +qed-. + +lemma cpr_cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cpr_cprs_div/ +qed-. + +lemma cprs_cpr_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T2 ⬌* T1. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_strip … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_cpr_div/ +qed-. + +lemma cprs_conf_cpcs: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ➡* T1 → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T #T1 #T2 #HT1 #HT2 elim (cprs_conf … HT1 … HT2) -HT1 -HT2 +/2 width=3 by cprs_div/ +qed-. + +lemma lprs_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (lprs_cprs_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was: pc3_wcpr0_t *) +(* Basic_1: note: pc3_wcpr0_t should be renamed *) +(* Note: alternative proof /3 width=5 by lprs_cprs_conf, lpr_lprs/ *) +lemma lpr_cprs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #HL12 #T1 #T2 #HT12 elim (cprs_lpr_conf_dx … HT12 … HL12) -L1 +/2 width=3 by cprs_div/ +qed-. + +(* Basic_1: was only: pc3_pr0_pr2_t *) +(* Basic_1: note: pc3_pr0_pr2_t should be renamed *) +lemma lpr_cpr_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +/3 width=5 by lpr_cprs_conf, cpr_cprs/ qed-. + +(* Basic_1: was only: pc3_thin_dx *) +lemma cpcs_flat: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. +#G #L #V1 #V2 #HV12 #T1 #T2 #HT12 +elim (cpcs_inv_cprs … HV12) -HV12 +elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_flat, cprs_div/ +qed. + +lemma cpcs_flat_dx_cpr_rev: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V2 ➡ V1 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → + ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬌* ⓕ{I}V2.T2. +/3 width=1 by cpr_cpcs_sn, cpcs_flat/ qed. + +lemma cpcs_bind_dx: ∀a,I,G,L,V,T1,T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V.T1 ⬌* ⓑ{a,I}V.T2. +#a #I #G #L #V #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, cprs_bind/ +qed. + +lemma cpcs_bind_sn: ∀a,I,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬌* V2 → ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T ⬌* ⓑ{a,I}V2. T. +#a #I #G #L #V1 #V2 #T #HV12 elim (cpcs_inv_cprs … HV12) -HV12 +/3 width=5 by cprs_div, cprs_bind/ +qed. + +lemma lsubr_cpcs_trans: ∀G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → + ∀L2. L2 ⫃ L1 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #T1 #T2 #HT12 elim (cpcs_inv_cprs … HT12) -HT12 +/3 width=5 by cprs_div, lsubr_cprs_trans/ +qed-. + +(* Basic_1: was: pc3_lift *) +lemma cpcs_lift: ∀G,L,K,b,l,k. ⬇[b, l, k] L ≘ K → + ∀T1,U1. ⬆[l, k] T1 ≘ U1 → ∀T2,U2. ⬆[l, k] T2 ≘ U2 → + ⦃G, K⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. +#G #L #K #b #l #k #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 #HT12 +elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2 +elim (lift_total T l k) /3 width=12 by cprs_div, cprs_lift/ +qed. + +lemma cpcs_strip: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ⬌* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌ T2 → + ∃∃T0. ⦃G, L⦄ ⊢ T1 ⬌ T0 & ⦃G, L⦄ ⊢ T2 ⬌* T0. +#G #L #T1 #T @TC_strip1 /2 width=3 by cpc_conf/ qed-. + +(* More inversion lemmas ****************************************************) + +(* Note: there must be a proof suitable for llpr *) +lemma cpcs_inv_abst_sn: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬌* T2 & a1 = a2. +#a1 #a2 #G #L #W1 #W2 #T1 #T2 #H +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (cprs_inv_abst1 … H1) -H1 #W0 #T0 #HW10 #HT10 #H destruct +elim (cprs_inv_abst1 … H2) -H2 #W #T #HW2 #HT2 #H destruct +lapply (lprs_cprs_conf … (L.ⓛW) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 +lapply (lprs_cpcs_trans … (L.ⓛW1) … HT2) /2 width=1 by lprs_pair/ -HT2 #HT2 +/4 width=3 by and3_intro, cprs_div, cpcs_cprs_div, cpcs_sym/ +qed-. + +lemma cpcs_inv_abst_dx: ∀a1,a2,G,L,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{a1}W1.T1 ⬌* ⓛ{a2}W2.T2 → + ∧∧ ⦃G, L⦄ ⊢ W1 ⬌* W2 & ⦃G, L.ⓛW2⦄ ⊢ T1 ⬌* T2 & a1 = a2. +#a1 #a2 #G #L #W1 #W2 #T1 #T2 #HT12 lapply (cpcs_sym … HT12) -HT12 +#HT12 elim (cpcs_inv_abst_sn … HT12) -HT12 /3 width=1 by cpcs_sym, and3_intro/ +qed-. + +(* Main properties **********************************************************) + +(* Basic_1: was pc3_t *) +theorem cpcs_trans: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #HT1 #T2 @(trans_TC … HT1) qed-. + +theorem cpcs_canc_sn: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T ⬌* T1 → ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. + +theorem cpcs_canc_dx: ∀G,L,T,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T → ⦃G, L⦄ ⊢ T2 ⬌* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=3 by cpcs_trans, cpcs_sym/ qed-. + +lemma cpcs_bind1: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → + ∀T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. + +lemma cpcs_bind2: ∀a,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬌* V2 → + ∀T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌* T2 → + ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ⬌* ⓑ{a,I}V2. T2. +/3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed. + +(* Basic_1: was: pc3_wcpr0 *) +lemma lpr_cpcs_conf: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ⦃G, L2⦄ ⊢ T1 ⬌* T2. +#G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H +/3 width=5 by cpcs_canc_dx, lpr_cprs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma new file mode 100644 index 000000000..d9db0509f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cprs.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cprs.ma". +include "basic_2/equivalence/cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) + +(* Properties about context sensitive computation on terms ******************) + +(* Basic_1: was: pc3_pr3_r *) +lemma cpcs_cprs_dx: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T2 #H @(cprs_ind … H) -T2 +/3 width=3 by cpcs_cpr_strap1, cpcs_strap1, cpc_cpcs/ +qed. + +(* Basic_1: was: pc3_pr3_x *) +lemma cpcs_cprs_sn: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T2 ➡* T1 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 +/3 width=3 by cpcs_cpr_div, cpcs_strap1, cpcs_cprs_dx/ +qed. + +lemma cpcs_cprs_strap1: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /2 width=3 by cpcs_cpr_strap1/ +qed-. + +lemma cpcs_cprs_strap2: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /2 width=3 by cpcs_cpr_strap2/ +qed-. + +lemma cpcs_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ⬌* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /2 width=3 by cpcs_cpr_div/ +qed-. + +(* Basic_1: was: pc3_pr3_conf *) +lemma cpcs_cprs_conf: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T ➡* T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /2 width=3 by cpcs_cpr_conf/ +qed-. + +(* Basic_1: was: pc3_pr3_t *) +(* Basic_1: note: pc3_pr3_t should be renamed *) +lemma cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +#G #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 +/2 width=3 by cpcs_cpr_div, cpcs_cprs_dx/ +qed. + +lemma cprs_cpr_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡ T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=5 by cpr_cprs, cprs_div/ qed-. + +lemma cpr_cprs_div: ∀G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡ T → ∀T2. ⦃G, L⦄ ⊢ T2 ➡* T → ⦃G, L⦄ ⊢ T1 ⬌* T2. +/3 width=3 by cpr_cprs, cprs_div/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt new file mode 100644 index 000000000..5072a8ac4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/partial.txt @@ -0,0 +1 @@ +cpcs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma new file mode 100644 index 000000000..657763483 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes.ma @@ -0,0 +1,37 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dpconvstar_8.ma". +include "basic_2/computation/scpds.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +definition scpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ + λh,o,d1,d2,G,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T. + +interpretation "stratified decomposed parallel equivalence (term)" + 'DPConvStar h o d1 d2 G L T1 T2 = (scpes h o d1 d2 G L T1 T2). + +(* Basic properties *********************************************************) + +lemma scpds_div: ∀h,o,G,L,T1,T2,T,d1,d2. + ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/2 width=3 by ex2_intro/ qed. + +lemma scpes_sym: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d1] T1. +#h #o #G #L #T1 #T2 #L1 #d2 * /2 width=3 by scpds_div/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma new file mode 100644 index 000000000..f42ebdbc9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_aaa.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/scpds_aaa.ma". +include "basic_2/equivalence/scpes.ma". + +(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) + +(* Main inversion lemmas about atomic arity assignment on terms *************) + +theorem scpes_aaa_mono: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → + A1 = A2. +#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 +lapply (scpds_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (scpds_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.ma new file mode 100644 index 000000000..f8ef46db1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_cpcs.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/computation/scpds_scpds.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/scpes.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +(* Inversion lemmas on parallel equivalence for terms ***********************) + +lemma scpes_inv_lstas_eq: ∀h,o,G,L,T1,T2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2 → + ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, d1] U1 → + ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, d2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. +#h #o #G #L #T1 #T2 #d1 #d2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2 +/3 width=8 by scpds_inv_lstas_eq, cprs_div/ +qed-. + +(* Properties on parallel equivalence for terms *****************************) + +lemma cpcs_scpes: ∀h,o,G,L,T1,d11. ⦃G, L⦄ ⊢ T1 ▪[h, o] d11 → + ∀U1,d12. d12 ≤ d11 → ⦃G, L⦄ ⊢ T1 •*[h, d12] U1 → + ∀T2,d21. ⦃G, L⦄ ⊢ T2 ▪[h, o] d21 → + ∀U2,d22. d22 ≤ d21 → ⦃G, L⦄ ⊢ T2 •*[h, d22] U2 → + ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d12, d22] T2. +#h #o #G #L #T1 #d11 #HT1 #U1 #d12 #Hd121 #HTU1 #T2 #d21 #HT2 #U2 #d22 #Hd221 #HTU2 #HU12 +elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by scpds_div, ex4_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.ma new file mode 100644 index 000000000..24ea20ec0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/scpes_scpes.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/computation/scpds_scpds.ma". +include "basic_2/equivalence/scpes.ma". + +(* STRATIFIED DECOMPOSED PARALLEL EQUIVALENCE FOR TERMS *********************) + +(* Advanced inversion lemmas ************************************************) + +lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 → + ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & + ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T. +#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H +elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +(* Advanced properties ******************************************************) + +lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 → + ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T. +#h #o #G #L #T #d1 #d2 #Hd21 #Hd1 +elim (da_lstas … Hd1 … d2) #U #HTU #_ +/3 width=3 by scpds_div, lstas_scpds/ +qed. + +lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 → + ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T → + ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2. +#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 * +/3 width=3 by scpds_div, lstas_scpds_trans/ qed-. + +(* Properties on parallel computation for terms *****************************) + +lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T → + ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d → + ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T → + ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2. +#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0) +#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1 +/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/ +qed. + +(* Main properties **********************************************************) + +theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → + ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2 +elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/ +qed-. + +theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 → + ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/3 width=4 by scpes_trans, scpes_sym/ qed-. + +theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T → + ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2. +/3 width=4 by scpes_trans, scpes_sym/ 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 46255ef35..3fe65458a 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 @@ -44,20 +44,20 @@ table { ] } ] -(* class "prune" - [ { "equivalence" * } { + [ { "rt-equivalence" * } { +(* [ { "decomposed rt-equivalence" * } { [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] } ] - [ { "context-sensitive equivalence" * } { - [ [ "" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ] +*) + [ { "context-sensitive parallel r-equivalence" * } { + [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ] } ] } ] -*) class "blue" [ { "rt-conversion" * } { [ { "context-sensitive parallel r-conversion" * } { diff --git a/matita/matita/contribs/lambdadelta/compile_partial.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh index cc92f87dc..59b18afc7 100644 --- a/matita/matita/contribs/lambdadelta/compile_partial.sh +++ b/matita/matita/contribs/lambdadelta/compile_partial.sh @@ -1,6 +1,8 @@ ../../matitac.opt `cat partial.txt` cd basic_2/rt_computation/ ../../../../matitac.opt `cat partial.txt` +cd ../rt_equivalence/ +../../../../matitac.opt `cat partial.txt` cd ../dynamic/ ../../../../matitac.opt `cat partial.txt` cd ../../