From f79d97a42a84f94d37ad9589fcce46149ee23d12 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 29 Jul 2012 17:41:46 +0000 Subject: [PATCH] - context free computation for terms and local environments --- .../contribs/lambda_delta/basic_2/basic_1.txt | 10 +-- .../lambda_delta/basic_2/computation/cprs.ma | 9 ++ .../lambda_delta/basic_2/computation/ltprs.ma | 81 +++++++++++++++++ .../basic_2/computation/ltprs_alt.ma | 34 ++++++++ .../basic_2/computation/ltprs_ldrop.ma | 27 ++++++ .../basic_2/computation/ltprs_ltprs.ma | 32 +++++++ .../lambda_delta/basic_2/computation/tprs.ma | 87 +++++++++++++++++++ .../basic_2/computation/tprs_lift.ma | 43 +++++++++ .../basic_2/computation/tprs_tprs.ma | 43 +++++++++ .../lambda_delta/basic_2/grammar/lenv_px.ma | 84 ++++++++++++++---- .../contribs/lambda_delta/basic_2/notation.ma | 4 + .../basic_2/reducibility/ltpr_ltpr.ma | 2 +- .../basic_2/substitution/ldrop.ma | 28 ++++++ .../contribs/lambda_delta/ground_2/star.ma | 7 ++ 14 files changed, 465 insertions(+), 26 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma create mode 100644 matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt index 70d162599..178f0d0a8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt +++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt @@ -170,17 +170,11 @@ pr0/fwd pr0_gen_void pr0/dec nf0_dec pr0/subst1 pr0_subst1_back pr0/subst1 pr0_subst1_fwd -pr1/pr1 pr1_strip -pr1/pr1 pr1_confluence -pr1/props pr1_pr0 -pr1/props pr1_t -pr1/props pr1_head_1 -pr1/props pr1_head_2 -pr1/props pr1_comp + pr1/props pr1_eta + pr2/fwd pr2_gen_void pr3/fwd pr3_gen_void -pr3/pr1 pr3_pr1 pr3/props pr3_eta sn3/props sns3_lifts sty1/cnt sty1_cnt diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma index 0891cb00c..ae0c1ae62 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/reducibility/cnf.ma". +include "basic_2/computation/tprs.ma". (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************) @@ -68,6 +69,11 @@ lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 @(cprs_strap1 … IHT2) -IHT2 /2 width=1/ qed. +(* Basic_1: was: pr3_pr1 *) +lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2. +#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/ +qed. + (* Basic inversion lemmas ***************************************************) (* Basic_1: was: pr3_gen_sort *) @@ -94,6 +100,9 @@ lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍⦃T⦄ → T = U. lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ qed-. +lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U. +/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-. + (* Basic_1: removed theorems 10: clear_pr3_trans pr3_cflat pr3_gen_bind pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12 diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma new file mode 100644 index 000000000..b7b0e1094 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr.ma". +include "basic_2/computation/tprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +definition ltprs: relation lenv ≝ TC … ltpr. + +interpretation + "context-free parallel computation (environment)" + 'PRedStar L1 L2 = (ltprs L1 L2). + +(* Basic eliminators ********************************************************) + +lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 → + (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) → + ∀L2. L1 ➡* L2 → R L2. +#L1 #R #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) // +qed-. + +lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 → + (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) → + ∀L1. L1 ➡* L2 → R L1. +#L2 #R #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) // +qed-. + +(* Basic properties *********************************************************) + +lemma ltprs_refl: reflexive … ltprs. +/2 width=1/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆. +#L2 #H @(ltprs_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 destruct +>(ltpr_inv_atom1 … HL2) -L2 // +qed-. + +lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 → + ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2. +#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/ +#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct +elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/ +qed-. + +lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆. +#L1 #H @(ltprs_ind_dx … H) -L1 // +#L1 #L #HL1 #_ #IHL2 destruct +>(ltpr_inv_atom2 … HL1) -L1 // +qed-. + +lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1. +#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/ +#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct +elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|. +#L1 #L2 #H @(ltprs_ind … H) -L2 // +#L #L2 #_ #HL2 #IHL1 +>IHL1 -L1 >(ltpr_fwd_length … HL2) -HL2 // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma new file mode 100644 index 000000000..7d532c973 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_alt.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +(* alternative definition of ltprs *) +definition ltprsa: relation lenv ≝ lpx tprs. + +interpretation + "context-free parallel computation (environment) alternative" + 'PRedStarAlt L1 L2 = (ltprsa L1 L2). + +(* Basic properties *********************************************************) + +lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2. +/2 width=1/ qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2. +/2 width=1/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.ma new file mode 100644 index 000000000..a7c320089 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ldrop.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/reducibility/ltpr_ldrop.ma". +include "basic_2/computation/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +lemma ltprs_ldrop_conf: dropable_sn ltprs. +/2 width=3/ qed. + +lemma ldrop_ltprs_trans: dedropable_sn ltprs. +/2 width=3/ qed. + +lemma ltprs_ldrop_trans_O1: dropable_dx ltprs. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.ma new file mode 100644 index 000000000..e529ee31a --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/ltprs_ltprs.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/reducibility/ltpr_ltpr.ma". +include "basic_2/computation/ltprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************) + +(* Advanced properties ******************************************************) + +lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 → + ∃∃L0. L1 ➡ L0 & L2 ➡* L0. +/3 width=3/ qed. + +(* Main properties **********************************************************) + +theorem ltprs_conf: Confluent … ltprs. +/3 width=3/ qed. + +theorem ltprs_trans: Transitive … ltprs. +/2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma new file mode 100644 index 000000000..b094e66c1 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Basic_1: includes: pr1_pr0 *) +definition tprs: relation term ≝ TC … tpr. + +interpretation "context-free parallel computation (term)" + 'PRedStar T1 T2 = (tprs T1 T2). + +(* Basic eliminators ********************************************************) + +lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 → + (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) → + ∀T2. T1 ➡* T2 → R T2. +#T1 #R #HT1 #IHT1 #T2 #HT12 +@(TC_star_ind … HT1 IHT1 … HT12) // +qed-. + +lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 → + (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) → + ∀T1. T1 ➡* T2 → R T1. +#T2 #R #HT2 #IHT2 #T1 #HT12 +@(TC_star_ind_dx … HT2 IHT2 … HT12) // +qed-. + +(* Basic properties *********************************************************) + +lemma tprs_refl: reflexive … tprs. +/2 width=1/ qed. + +lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2. +/2 width=3/ qed. + +lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2. +/2 width=3/ qed. + +(* Basic_1: was only: pr1_head_1 *) +lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2 +[1,3: /3 width=1/ +|2,4: #V #V2 #_ #HV2 #IHV1 + @(tprs_strap1 … IHV1) -IHV1 /2 width=1/ +] +qed. + +(* Basic_1: was only: pr1_head_2 *) +lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2 +[1,3: /3 width=1/ +|2,4: #T #T2 #_ #HT2 #IHT1 + @(tprs_strap1 … IHT1) -IHT1 /2 width=1/ +] +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k. +#U2 #k #H @(tprs_ind … H) -U2 // +#U #U2 #_ #HU2 #IHU1 destruct +>(tpr_inv_atom1 … HU2) -HU2 // +qed-. + +lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨ + ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2. +#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/ +#U #U2 #_ #HU2 * /3 width=3/ * +#W #T #HW1 #HT1 #H destruct +elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ * +#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma new file mode 100644 index 000000000..d0d173470 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_lift.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_lift.ma". +include "basic_2/computation/tprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Advanced inversion lemmas ************************************************) + +lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 → + ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2. +#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/ +#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct +elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/ +qed-. + +lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → + V1 ➡* V2 ∧ T1 ➡* T2. +#a #V1 #V2 #T1 #T2 #H +elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/ +qed-. + +(* Relocation properties ****************************************************) + +(* Note: this was missing in basic_1 *) +lemma tprs_lift: t_liftable tprs. +/3 width=7/ qed. + +(* Note: this was missing in basic_1 *) +lemma tprs_inv_lift1: t_deliftable_sn tprs. +/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma new file mode 100644 index 000000000..232244510 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/tprs_tprs.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/tpr_tpr.ma". +include "basic_2/computation/tprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************) + +(* Advanced properties ******************************************************) + +(* Basic_1: was: pr1_strip *) +lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 → + ∃∃T0. T1 ➡ T0 & T2 ➡* T0. +/3 width=3/ qed. + +(* Main propertis ***********************************************************) + +(* Basic_1: was: pr1_confluence *) +theorem tprs_conf: Confluent … tprs. +/3 width=3/ qed. + +(* Basic_1: was: pr1_t *) +theorem tprs_trans: Transitive … tprs. +/2 width=3/ qed. + +(* Basic_1: was: pr1_comp *) +lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 → + ②{I} V1. T1 ➡* ②{I} V2. T2. +#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/ +#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 +@(tprs_trans … (②{I}V.T2)) /2 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma index fd3034456..1b0c88e02 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_px.ma @@ -18,59 +18,53 @@ include "basic_2/grammar/lenv_length.ma". inductive lpx (R:relation term): relation lenv ≝ | lpx_stom: lpx R (⋆) (⋆) -| lpx_pair: ∀K1,K2,I,V1,V2. +| lpx_pair: ∀I,K1,K2,V1,V2. lpx R K1 K2 → R V1 V2 → lpx R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) . -(* Basic properties *********************************************************) - -lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). -#R #HR #L elim L -L // /2 width=1/ -qed. - (* Basic inversion lemmas ***************************************************) fact lpx_inv_atom1_aux: ∀R,L1,L2. lpx R L1 L2 → L1 = ⋆ → L2 = ⋆. #R #L1 #L2 * -L1 -L2 [ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct ] qed-. lemma lpx_inv_atom1: ∀R,L2. lpx R (⋆) L2 → L2 = ⋆. /2 width=4 by lpx_inv_atom1_aux/ qed-. -fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 → +fact lpx_inv_pair1_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. #R #L1 #L2 * -L1 -L2 -[ #K1 #I #V1 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/ +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ ] qed-. -lemma lpx_inv_pair1: ∀R,K1,I,V1,L2. lpx R (K1. ⓑ{I} V1) L2 → +lemma lpx_inv_pair1: ∀R,I,K1,V1,L2. lpx R (K1. ⓑ{I} V1) L2 → ∃∃K2,V2. lpx R K1 K2 & R V1 V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by lpx_inv_pair1_aux/ qed-. fact lpx_inv_atom2_aux: ∀R,L1,L2. lpx R L1 L2 → L2 = ⋆ → L1 = ⋆. #R #L1 #L2 * -L1 -L2 [ // -| #K1 #K2 #I #V1 #V2 #_ #_ #H destruct +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct ] qed-. lemma lpx_inv_atom2: ∀R,L1. lpx R L1 (⋆) → L1 = ⋆. /2 width=4 by lpx_inv_atom2_aux/ qed-. -fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 → +fact lpx_inv_pair2_aux: ∀R,L1,L2. lpx R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. #R #L1 #L2 * -L1 -L2 -[ #K2 #I #V2 #H destruct -| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/ +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ ] qed-. -lemma lpx_inv_pair2: ∀R,L1,K2,I,V2. lpx R L1 (K2. ⓑ{I} V2) → +lemma lpx_inv_pair2: ∀R,I,L1,K2,V2. lpx R L1 (K2. ⓑ{I} V2) → ∃∃K1,V1. lpx R K1 K2 & R V1 V2 & L1 = K1. ⓑ{I} V1. /2 width=3 by lpx_inv_pair2_aux/ qed-. @@ -79,3 +73,59 @@ lemma lpx_inv_pair2: ∀R,L1,K2,I,V2. lpx R L1 (K2. ⓑ{I} V2) → lemma lpx_fwd_length: ∀R,L1,L2. lpx R L1 L2 → |L1| = |L2|. #R #L1 #L2 #H elim H -L1 -L2 normalize // qed-. + +(* Basic properties *********************************************************) + +lemma lpx_refl: ∀R. reflexive ? R → reflexive … (lpx R). +#R #HR #L elim L -L // /2 width=1/ +qed. + +lemma lpx_trans: ∀R. Transitive ? R → Transitive … (lpx R). +#R #HR #L1 #L #H elim H -L // +#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H +elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ +qed. + +lemma lpx_conf: ∀R. Confluent ? R → Confluent … (lpx R). +#R #HR #L0 #L1 #H elim H -L1 +[ #X #H >(lpx_inv_atom1 … H) -X /2 width=3/ +| #I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #X #H + elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct + elim (IHK01 … HK02) -K0 #K #HK1 #HK2 + elim (HR … HV01 … HV02) -HR -V0 /3 width=5/ +] +qed. + +lemma lpx_TC_inj: ∀R,L1,L2. lpx R L1 L2 → lpx (TC … R) L1 L2. +#R #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ +qed. + +lemma lpx_TC_step: ∀R,L1,L. lpx (TC … R) L1 L → + ∀L2. lpx R L L2 → lpx (TC … R) L1 L2. +#R #L1 #L #H elim H -L /2 width=1/ +#I #K1 #K #V1 #V #_ #HV1 #IHK1 #X #H +elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK2 #HV2 #H destruct /3 width=3/ +qed. + +lemma TC_lpx_pair_dx: ∀R. reflexive ? R → + ∀I,K,V1,V2. TC … R V1 V2 → + TC … (lpx R) (K.ⓑ{I}V1) (K.ⓑ{I}V2). +#R #HR #I #K #V1 #V2 #H elim H -V2 +/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) +qed. + +lemma TC_lpx_pair_sn: ∀R. reflexive ? R → + ∀I,V,K1,K2. TC … (lpx R) K1 K2 → + TC … (lpx R) (K1.ⓑ{I}V) (K2.ⓑ{I}V). +#R #HR #I #V #K1 #K2 #H elim H -K2 +/4 width=5 by lpx_refl, lpx_pair, inj, step/ (**) (* too slow without trace *) +qed. + +lemma lpx_TC: ∀R,L1,L2. TC … (lpx R) L1 L2 → lpx (TC … R) L1 L2. +#R #L1 #L2 #H elim H -L2 /2 width=1/ /2 width=3/ +qed. + +lemma lpx_inv_TC: ∀R. reflexive ? R → + ∀L1,L2. lpx (TC … R) L1 L2 → TC … (lpx R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1/ /3 width=3/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index b396acf55..a115260b9 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -326,6 +326,10 @@ notation "hvbox( L ⊢ break term 46 T1 ➡* break term 46 T2 )" non associative with precedence 45 for @{ 'PRedStar $L $T1 $T2 }. +notation "hvbox( T1 ➡➡* break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRedStarAlt $T1 $T2 }. + notation "hvbox( L1 ⊢ ➡* break term 46 L2 )" non associative with precedence 45 for @{ 'CPRedStar $L1 $L2 }. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma index aaeb2064c..4a27a6e70 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ltpr.ma @@ -22,7 +22,7 @@ include "basic_2/reducibility/ltpr.ma". theorem ltpr_conf: ∀L0:lenv. ∀L1. L0 ➡ L1 → ∀L2. L0 ➡ L2 → ∃∃L. L1 ➡ L & L2 ➡ L. #L0 #L1 #H elim H -L0 -L1 /2 width=3/ -#K0 #K1 #I #V0 #V1 #_ #HV01 #IHK01 #L2 #H +#I #K0 #K1 #V0 #V1 #_ #HV01 #IHK01 #L2 #H elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK02 #HV02 #H destruct elim (IHK01 … HK02) -K0 #K #HK1 #HK2 elim (tpr_conf … HV01 HV02) -V0 /3 width=5/ diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma index e7353d7de..c93d3cd18 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma @@ -215,6 +215,34 @@ lemma ldrop_lsubs_ldrop2_abbr: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → ] qed. +lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (TC … R). +#R #HR #L1 #K1 #d #e #HLK1 #L2 #H elim H -L2 +[ #L2 #HL12 + elim (HR … HLK1 … HL12) -HR -L1 /3 width=3/ +| #L #L2 #_ #HL2 * #K #HK1 #HLK + elim (HR … HLK … HL2) -HR -L /3 width=3/ +] +qed. + +lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). +#R #HR #L1 #K1 #d #e #HLK1 #K2 #H elim H -K2 +[ #K2 #HK12 + elim (HR … HLK1 … HK12) -HR -K1 /3 width=3/ +| #K #K2 #_ #HK2 * #L #HL1 #HLK + elim (HR … HLK … HK2) -HR -K /3 width=3/ +] +qed. + +lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). +#R #HR #L1 #L2 #H elim H -L2 +[ #L2 #HL12 #K2 #e #HLK2 + elim (HR … HL12 … HLK2) -HR -L2 /3 width=3/ +| #L #L2 #_ #HL2 #IHL1 #K2 #e #HLK2 + elim (HR … HL2 … HLK2) -HR -L2 #K #HLK #HK2 + elim (IHL1 … HLK) -L /3 width=5/ +] +qed. + (* Basic forvard lemmas *****************************************************) (* Basic_1: was: drop_S *) diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma index 18f028acc..3517eff98 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma @@ -20,6 +20,13 @@ include "ground_2/notation.ma". definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). +definition Confluent: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 → + ∃∃a. R a1 a & R a2 a. + +definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. + definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & R1 a2 a. -- 2.39.2