From: Ferruccio Guidi Date: Sat, 27 Oct 2012 13:34:28 +0000 (+0000) Subject: - some additions and corrections X-Git-Tag: make_still_working~1488 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a04bfe6d381b281db15e8b432f6f221576aad439;p=helm.git - some additions and corrections --- diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma index bf429672a..61c720754 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma @@ -21,6 +21,18 @@ definition fprs: bi_relation lenv term ≝ bi_TC … fpr. interpretation "context-free parallel computation (closure)" 'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2). +(* Basic eliminators ********************************************************) + +lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + (* Basic properties *********************************************************) lemma fprs_refl: bi_reflexive … fprs. diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma new file mode 100644 index 000000000..4e7a633c3 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_cprs.ma @@ -0,0 +1,70 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpr_cpr.ma". +include "basic_2/computation/cprs.ma". +include "basic_2/computation/fprs.ma". + +(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************) + +(* Properties on context-sensitive parallel computation for terms ***********) + +lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄. +#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/ +qed. +(* +(* Advanced propertis *******************************************************) + +lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → + ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄. +#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I +elim (fpr_inv_all … H) /3 width=4/ +qed. + +(* Advanced forward lemmas **************************************************) + +lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2. + ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ → + ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2. +* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H +elim (fpr_inv_all … H) -H #L #HL1 #H #HL2 +[ elim (cpr_inv_abbr1 … H) -H * + [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/ + | #T #_ #_ #H destruct + ] +| elim (cpr_inv_abst1 … H Abst V2) -H + #V #T #HV1 #_ #H destruct /3 width=4/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lamma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ → + ∃∃K2,V2. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L2 = K2.ⓑ{I}V2. +#I1 #K1 #X #V1 #T1 #T2 #H +elim (fpr_fwd_pair1 … H) -H #I2 #K2 #V2 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/ +qed-. + +lamma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ → + ∃∃K1,V1. ⦃K1, V1⦄ ➡ ⦃K2, V2⦄ & + ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ & + L1 = K1.ⓑ{I}V1. +#I2 #X #K2 #V2 #T1 #T2 #H +elim (fpr_fwd_pair3 … H) -H #I1 #K1 #V1 #HT12 #H destruct +elim (fpr_fwd_shift_bind_minus … HT12) #HV12 #H destruct /2 width=5/ +qed-. +*) diff --git a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma index ed64873ef..5fb614a8c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma @@ -25,13 +25,15 @@ interpretation (* Basic properties *********************************************************) -lemma cpc_refl: ∀L,T. L ⊢ T ⬌ T. +lemma cpc_refl: ∀L. reflexive … (cpc L). /2 width=1/ qed. -lemma cpc_sym: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → L ⊢ T2 ⬌ T1. +lemma cpc_sym: ∀L. symmetric … (cpc L). #L #T1 #T2 * /2 width=1/ qed. -lemma cpc_cpr: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T. +(* Basic forward lemmas *****************************************************) + +lemma cpc_fwd_cpr: ∀L,T1,T2. L ⊢ T1 ⬌ T2 → ∃∃T. L ⊢ T1 ➡ T & L ⊢ T2 ➡ T. #L #T1 #T2 * /2 width=3/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma index 25b85269e..223dba7ee 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv.ma @@ -26,7 +26,7 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → - ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) + ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ W ⬌* U → snv h g L (ⓝW.T) . interpretation "stratified native validity (term)" @@ -34,8 +34,23 @@ interpretation "stratified native validity (term)" (* Basic inversion lemmas ***************************************************) -lemma snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → - ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. +fact snv_inv_lref_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀i. X = #i → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g]. +#h #g #L #X * -L -X +[ #L #k #i #H destruct +| #I #L #K #V #i0 #HLK #HV #i #H destruct /2 width=5/ +| #a #I #L #V #T #_ #_ #i #H destruct +| #a #L #V #W #W0 #T #U #l #_ #_ #_ #_ #_ #i #H destruct +| #L #W #T #U #l #_ #_ #_ #_ #i #H destruct +] +qed. + +lemma snv_inv_lref: ∀h,g,L,i. ⦃h, L⦄ ⊩ #i :[g] → + ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊩ V :[g]. +/2 width=3/ qed-. + +fact snv_inv_bind_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀a,I,V,T. X = ⓑ{a,I}V.T → + ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. #h #g #L #X * -L -X [ #L #k #a #I #V #T #H destruct | #I0 #L #K #V0 #i #_ #_ #a #I #V #T #H destruct @@ -49,10 +64,10 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → ⦃h, L⦄ ⊩ V :[g] ∧ ⦃h, L.ⓑ{I}V⦄ ⊩ T :[g]. /2 width=4/ qed-. -lemma snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → - ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & - ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & - ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. +fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → + ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & + ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & + ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X [ #L #k #V #T #H destruct | #I #L #K #V0 #i #_ #_ #V #T #H destruct @@ -67,3 +82,20 @@ lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & ⦃h, L⦄ ⊢ T ➸*[g] ⓛ{a}W0.U. /2 width=3/ qed-. + +fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → + ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & + L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U. +#h #g #L #X * -L -X +[ #L #k #W #T #H destruct +| #I #L #K #V #i #_ #_ #W #T #H destruct +| #a #I #L #V #T0 #_ #_ #W #T #H destruct +| #a #L #V #W0 #W00 #T0 #U #l #_ #_ #_ #_ #_ #W #T #H destruct +| #L #W0 #T0 #U0 #l #HW0 #HT0 #HTU0 #HWU0 #W #T #H destruct /2 width=4/ +] +qed. + +lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] → + ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & + L ⊢ W ⬌* U & ⦃h, L⦄ ⊢ T •[g, l + 1] U. +/2 width=3/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma index fd6645538..fdef6d003 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_aaa.ma @@ -33,8 +33,8 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. lapply (xprs_aaa … HT … HTU) -HTU #H elim (aaa_inv_abst … H) -H #B0 #A #H1 #HU #H2 destruct lapply (aaa_mono … H1 … HW0) -W0 #H destruct /3 width=4/ -| #L #W #T #U #l #_ #_ #HTU #HUW * #B #HW * #A #HT - lapply (aaa_cpcs_mono … HUW A … HW) -HUW /2 width=7/ -HTU #H destruct /3 width=3/ +| #L #W #T #U #l #_ #_ #HTU #HWU * #B #HW * #A #HT + lapply (aaa_cpcs_mono … HWU … HW A ?) -HWU /2 width=7/ -HTU #H destruct /3 width=3/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma index 6d79ef571..67ab751c0 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/snv_lift.ma @@ -74,6 +74,6 @@ lemma snv_inv_lift: ∀h,g,L,U. ⦃h, L⦄ ⊩ U :[g] → ∀K,d,e. ⇩[d, e] L | #L #W0 #U #W #l #_ #_ #HUW #HW0 #IHW0 #IHU #K #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct elim (ssta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HTV #HVW - lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/ + lapply (cpcs_inv_lift … HLK … HVW0 … HVW ?) // -W /3 width=4/ ] qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma index 346189f92..9d9ceb942 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma @@ -40,10 +40,11 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was: pc3_refl *) -lemma cpcs_refl: ∀L,T. L ⊢ T ⬌* T. +lemma cpcs_refl: ∀L. reflexive … (cpcs L). /2 width=1/ qed. -lemma cpcs_sym: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1. +(* Basic_1: was: pc3_s *) +lemma cpcs_sym: ∀L. symmetric … (cpcs L). /3 width=1/ qed. lemma cpcs_strap1: ∀L,T1,T,T2. L ⊢ T1 ⬌* T → L ⊢ T ⬌ T2 → L ⊢ T1 ⬌* T2. @@ -56,10 +57,16 @@ lemma cpcs_strap2: ∀L,T1,T,T2. L ⊢ T1 ⬌ T → L ⊢ T ⬌* T2 → L ⊢ T1 lemma cpcs_cpr_dx: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ⬌* T2. /3 width=1/ qed. +lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2. +/3 width=1/ qed. + (* Basic_1: was: pc3_pr2_x *) lemma cpcs_cpr_sn: ∀L,T1,T2. L ⊢ T2 ➡ T1 → L ⊢ T1 ⬌* T2. /3 width=1/ qed. +lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2. +/3 width=1/ qed. + lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2. /3 width=3/ qed. @@ -70,15 +77,13 @@ lemma cpcs_cpr_strap2: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T ⬌* T2 → lemma cpcs_cpr_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2. /3 width=3/ qed. +lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2. +/3 width=3/ qed-. + (* Basic_1: was: pc3_pr2_u2 *) lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. /3 width=3/ qed. -(* Basic_1: was: pc3_s *) -lemma cprs_comm: ∀L,T1,T2. L ⊢ T1 ⬌* T2 → L ⊢ T2 ⬌* T1. -#L #T1 #T2 #H @(cpcs_ind … H) -T2 // /3 width=3/ -qed. - (* Basic_1: removed theorems 9: clear_pc3_trans pc3_ind_left pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21 diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma index 04c071f20..cf0b9030c 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma @@ -187,10 +187,10 @@ theorem cpcs_trans: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ⬌* T2 → L /2 width=3/ qed. theorem cpcs_canc_sn: ∀L,T,T1,T2. L ⊢ T ⬌* T1 → L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cprs_comm/ qed. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) theorem cpcs_canc_dx: ∀L,T,T1,T2. L ⊢ T1 ⬌* T → L ⊢ T2 ⬌* T → L ⊢ T1 ⬌* T2. -/3 width=3 by cpcs_trans, cprs_comm/ qed. (**) (* /3 width=3/ is too slow *) +/3 width=3 by cpcs_trans, cpcs_sym/ qed. (**) (* /3 width=3/ is too slow *) lemma cpcs_abbr1: ∀a,L,V1,V2. L ⊢ V1 ⬌* V2 → ∀T1,T2. L.ⓓV1 ⊢ T1 ⬌* T2 → L ⊢ ⓓ{a}V1. T1 ⬌* ⓓ{a}V2. T2. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma index c2911e1c8..cb1f5d76a 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cprs.ma @@ -24,46 +24,28 @@ lemma cpcs_cprs_dx: ∀L,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /3 width=3/ qed. -lemma cpcs_tpr_dx: ∀L,T1,T2. T1 ➡ T2 → L ⊢ T1 ⬌* T2. -/3 width=1/ qed. - (* Basic_1: was: pc3_pr3_x *) lemma cpcs_cprs_sn: ∀L,T1,T2. L ⊢ T2 ➡* T1 → L ⊢ T1 ⬌* T2. #L #T1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /3 width=3/ qed. -lemma cpcs_tpr_sn: ∀L,T1,T2. T2 ➡ T1 → L ⊢ T1 ⬌* T2. -/3 width=1/ qed. - lemma cpcs_cprs_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T #HT1 #T2 #H @(cprs_ind … H) -T2 /width=1/ /2 width=3/ qed. -lemma cpcs_cpr_strap1: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T ➡ T2 → L ⊢ T1 ⬌* T2. -/3 width=3/ qed-. - lemma cpcs_cprs_strap2: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T #H #T2 #HT2 @(cprs_ind_dx … H) -T1 /width=1/ /2 width=3/ qed. -lemma cpcs_cpr_strap2: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/3 width=3/ qed-. - lemma cpcs_cprs_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2. #L #T1 #T #HT1 #T2 #H @(cprs_ind_dx … H) -T2 /width=1/ /2 width=3/ qed. -lemma cpcs_cpr_div: ∀L,T1,T. L ⊢ T1 ⬌* T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2. -/3 width=3/ qed-. - (* Basic_1: was: pc3_pr3_conf *) lemma cpcs_cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. #L #T1 #T #H #T2 #HT2 @(cprs_ind … H) -T1 /width=1/ /2 width=3/ qed. -lemma cpcs_cpr_conf: ∀L,T1,T. L ⊢ T ➡ T1 → ∀T2. L ⊢ T ⬌* T2 → L ⊢ T1 ⬌* T2. -/3 width=3/ qed-. - (* Basic_1: was: pc3_pr3_t *) (* Basic_1: note: pc3_pr3_t should be renamed *) lemma cprs_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2. @@ -75,6 +57,3 @@ lemma cprs_cpr_div: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T2 ➡ T → L lemma cpr_cprs_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡* T → L ⊢ T1 ⬌* T2. /3 width=3 by step, cprs_div/ qed-. - -lemma cpr_div: ∀L,T1,T. L ⊢ T1 ➡ T → ∀T2. L ⊢ T2 ➡ T → L ⊢ T1 ⬌* T2. -/3 width=5 by step, cprs_div/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma index c3cbf6c01..fded17bd1 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs.ma @@ -38,9 +38,12 @@ qed-. (* Basic properties *********************************************************) -lemma lfpcs_refl: ∀L. ⦃L⦄ ⬌* ⦃L⦄. +lemma lfpcs_refl: reflexive … lfpcs. /2 width=1/ qed. +lemma lfprs_sym: symmetric … lfpcs. +/3 width=1/ qed. + lemma lfpcs_strap1: ∀L1,L,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L⦄ ⬌ ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. /2 width=3/ qed. @@ -64,7 +67,3 @@ lemma lfpcs_lfpr_div: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L2⦄ ➡ ⦃ lemma lfpcs_lfpr_conf: ∀L1,L. ⦃L⦄ ➡ ⦃L1⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. /3 width=3/ qed. - -lemma lfprs_comm: ∀L1,L2. ⦃L1⦄ ⬌* ⦃L2⦄ → ⦃L2⦄ ⬌* ⦃L1⦄. -#L1 #L2 #H @(lfpcs_ind … H) -L2 // /3 width=3/ -qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma index fcbeb9b8a..434068e4f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/lfpcs_lfpcs.ma @@ -44,7 +44,7 @@ theorem lfpcs_trans: ∀L1,L. ⦃L1⦄ ⬌* ⦃L⦄ → ∀L2. ⦃L⦄ ⬌* ⦃L /2 width=3/ qed. theorem lfpcs_canc_sn: ∀L,L1,L2. ⦃L⦄ ⬌* ⦃L1⦄ → ⦃L⦄ ⬌* ⦃L2⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/3 width=3 by lfpcs_trans, lfprs_comm/ qed. +/3 width=3 by lfpcs_trans, lfprs_sym/ qed. theorem lfpcs_canc_dx: ∀L,L1,L2. ⦃L1⦄ ⬌* ⦃L⦄ → ⦃L2⦄ ⬌* ⦃L⦄ → ⦃L1⦄ ⬌* ⦃L2⦄. -/3 width=3 by lfpcs_trans, lfprs_comm/ qed. +/3 width=3 by lfpcs_trans, lfprs_sym/ qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc new file mode 100644 index 000000000..d815739fb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "hvbox( L1 ⊢ ⬌* break term 46 L2 )" + non associative with precedence 45 + for @{ 'CPConvStar $L1 $L2 }. + +include "basic_2/grammar/lenv_px_sn.ma". +include "basic_2/equivalence/cpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) + +definition lcpcs: relation lenv ≝ lpx_sn … cpcs. + +interpretation "context-sensitive parallel equivalence (local environment)" + 'CPConvStar L1 L2 = (lcpcs L1 L2). + +(* Basic inversion lemmas ***************************************************) + +lemma lcpcs_inv_atom1: ∀L2. ⋆ ⊢ ⬌* L2 → L2 = ⋆. +/2 width=2 by lpx_sn_inv_atom1/ qed-. + +lemma lcpcs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ⬌* L2 → + ∃∃K2,V2. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L2 = K2. ⓑ{I} V2. +/2 width=1 by lpx_sn_inv_pair1/ qed-. + +lemma lcpcs_inv_atom2: ∀L1. L1 ⊢ ⬌* ⋆ → L1 = ⋆. +/2 width=2 by lpx_sn_inv_atom2/ qed-. + +lemma lcpcs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ⬌* K2. ⓑ{I} V2 → + ∃∃K1,V1. K1 ⊢ ⬌* K2 & K1 ⊢ V1 ⬌* V2 & L1 = K1. ⓑ{I} V1. +/2 width=1 by lpx_sn_inv_pair2/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lcpcs_fwd_length: ∀L1,L2. L1 ⊢ ⬌* L2 → |L1| = |L2|. +/2 width=2 by lpx_sn_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc new file mode 100644 index 000000000..ecc6be867 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lcpcs_ltpr.etc @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/equivalence/lcpcs.ma". + +(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON LOCAL ENVIRONMENTS *************) + +(* Properties on context-free parallel reduction for local environments *****) + +lemma ltpr_lcpcs: ∀L1,L2. L1 ➡ L2 → L1 ⊢ ⬌* L2. +#L1 #L2 #H elim H -L1 -L2 // /4 width=1/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc new file mode 100644 index 000000000..fddab0332 --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/etc/lenv_px/lenv_px_sn.etc @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **********) + +inductive lpx_sn (R:lenv→relation term): relation lenv ≝ +| lpx_sn_stom: lpx_sn R (⋆) (⋆) +| lpx_sn_pair: ∀I,K1,K2,V1,V2. + lpx_sn R K1 K2 → R K1 V1 V2 → lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) +. + +(* Basic inversion lemmas ***************************************************) + +fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. +/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. + +fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #L1 #L2 * -L1 -L2 +[ #J #K1 #V1 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. + +fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. +#R #L1 #L2 * -L1 -L2 +[ // +| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct +] +qed-. + +lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. +/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. + +fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #L1 #L2 * -L1 -L2 +[ #J #K2 #V2 #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/ +] +qed-. + +lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L1 -L2 normalize // +qed-. diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index 4e67f393a..78838bc9d 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -246,6 +246,10 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break [ g , break non associative with precedence 45 for @{ 'StaticType $h $g $l $L $T1 $T2 }. +notation "hvbox( h ⊢ break term 46 L1 • ≃ [ g ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'CCongS $h $g $L1 $L2 }. + notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ g ] break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqS $h $g $L1 $L2 }. @@ -396,23 +400,43 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" non associative with precedence 45 for @{ 'PConv $L $T1 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ ⦃ L2 ⦄ )" +notation "hvbox( ⦃ L1 ⦄ ⬌ break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConv $L1 $L2 }. +notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPConv $L1 $T1 $L2 $T2 }. + +notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ break ⦃ L2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPConvAlt $L1 $L2 }. + +notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPConvAlt $L1 $T1 $L2 $T2 }. + (* Equivalence **************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )" +notation "hvbox( ⦃ L1 ⦄ ⬌ * break ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStar $L1 $L2 }. -notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )" +notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ * break ⦃ L2 , break T2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPConvStar $L1 $T1 $L2 $T2 }. + +notation "hvbox( ⦃ L1 ⦄ ⬌ ⬌ * break ⦃ L2 ⦄ )" + non associative with precedence 45 + for @{ 'FocalizedPConvStarAlt $L1 $L2 }. + +notation "hvbox( ⦃ L1 , break T1 ⦄ ⬌ ⬌ * break ⦃ L2 , break T2 ⦄ )" non associative with precedence 45 - for @{ 'CPConvStar $L1 $L2 }. + for @{ 'FocalizedPConvStarAlt $L1 $T1 $L2 $T2 }. (* Dynamic typing ***********************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma index f893a5c14..4c9b8ac97 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_aaa.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/aaa_ltpss_sn.ma". -include "basic_2/reducibility/ltpr_aaa.ma". include "basic_2/reducibility/cpr_aaa.ma". include "basic_2/reducibility/cfpr_cpr.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma index f37cb5159..a46c9776b 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cpr.ma @@ -13,7 +13,6 @@ (**************************************************************************) include "basic_2/unfold/ltpss_sn_alt.ma". -include "basic_2/reducibility/ltpr.ma". include "basic_2/reducibility/cpr_tpss.ma". include "basic_2/reducibility/cpr_cpr.ma". include "basic_2/reducibility/cfpr_ltpss.ma". diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma index 7abd3f22f..0de0b98f5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma @@ -16,6 +16,11 @@ include "basic_2/reducibility/cfpr_cpr.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) +(* Properties on context-sensitive parallel reduction for terms *************) + +lemma cpr_fpr: ∀L,T1,T2. L ⊢ T1 ➡ T2 → ⦃L, T1⦄ ➡ ⦃L, T2⦄. +/2 width=4/ qed. + (* Advanced propertis *******************************************************) lemma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 → diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma index e8bff44cd..342a839d5 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ltpss_sn.ma @@ -15,7 +15,7 @@ include "basic_2/unfold/ltpss_sn_alt.ma". include "basic_2/static/ssta_ltpss_dx.ma". -(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) +(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************) (* Properties about sn parallel unfold **************************************) diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index d74380de4..f469ddca2 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -167,6 +167,9 @@ definition bi_relation: Type[0] → Type[0] → Type[0] definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop ≝ λA,B,R. ∀x,y. R x y x y. +definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. + ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2. + definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. ∀a1,a,b1,b. R a1 b1 a b → ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2. diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index d8d08d09a..2e3b775e4 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -196,7 +196,7 @@ lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A. P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) → ∀a2. TC … R a1 a2 → P a2. #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/ -qed. +qed-. inductive TC_dx (A:Type[0]) (R:relation A): A → A → Prop ≝ |inj_dx: ∀a,c. R a c → TC_dx A R a c @@ -255,17 +255,65 @@ lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R). #A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/ qed. -inductive bi_TC (A,B:Type[0]) (R:bi_relation A B) (a:A) (b:B): A → B → Prop ≝ +inductive bi_TC (A,B:Type[0]) (R:bi_relation A B) (a:A) (b:B): relation2 A B ≝ |bi_inj : ∀c,d. R a b c d → bi_TC A B R a b c d |bi_step: ∀c,d,e,f. bi_TC A B R a b c d → R c d e f → bi_TC A B R a b e f. +lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2. + R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2. +#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/ +qed. + lemma bi_TC_reflexive: ∀A,B,R. bi_reflexive A B R → bi_reflexive A B (bi_TC … R). /2 width=1/ qed. -lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2. - R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2. -#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/ +inductive bi_TC_dx (A,B:Type[0]) (R:bi_relation A B): bi_relation A B ≝ + |bi_inj_dx : ∀a1,a2,b1,b2. R a1 b1 a2 b2 → bi_TC_dx A B R a1 b1 a2 b2 + |bi_step_dx : ∀a1,a,a2,b1,b,b2. R a1 b1 a b → bi_TC_dx A B R a b a2 b2 → + bi_TC_dx A B R a1 b1 a2 b2. + +lemma bi_TC_dx_strap: ∀A,B. ∀R: bi_relation A B. + ∀a1,a,a2,b1,b,b2. bi_TC_dx A B R a1 b1 a b → + R a b a2 b2 → bi_TC_dx A B R a1 b1 a2 b2. +#A #B #R #a1 #a #a2 #b1 #b #b2 #H1 elim H1 -a -b /3 width=4/ +qed. + +lemma bi_TC_to_bi_TC_dx: ∀A,B. ∀R: bi_relation A B. + ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → + bi_TC_dx … R a1 b1 a2 b2. +#A #B #R #a1 #a2 #b1 #b2 #H12 elim H12 -a2 -b2 /2 width=4/ +qed. + +lemma bi_TC_dx_to_bi_TC: ∀A,B. ∀R: bi_relation A B. + ∀a1,a2,b1,b2. bi_TC_dx … R a1 b1 a2 b2 → + bi_TC … R a1 b1 a2 b2. +#A #b #R #a1 #a2 #b1 #b2 #H12 elim H12 -a1 -a2 -b1 -b2 /2 width=4/ +qed. + +fact bi_TC_ind_dx_aux: ∀A,B,R,a2,b2. ∀P:relation2 A B. + (∀a1,b1. R a1 b1 a2 b2 → P a1 b1) → + (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) → + ∀a1,a,b1,b. bi_TC … R a1 b1 a b → a = a2 → b = b2 → P a1 b1. +#A #B #R #a2 #b2 #P #H1 #H2 #a1 #a #b1 #b #H1 +elim (bi_TC_to_bi_TC_dx ??????? H1) -a1 -a -b1 -b +[ #a1 #x #b1 #y #H1 #Hx #Hy destruct /2 width=1/ +| #a1 #a #x #b1 #b #y #H1 #H #IH #Hx #Hy destruct /3 width=5/ +] +qed-. + +lemma bi_TC_ind_dx: ∀A,B,R,a2,b2. ∀P:relation2 A B. + (∀a1,b1. R a1 b1 a2 b2 → P a1 b1) → + (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) → + ∀a1,b1. bi_TC … R a1 b1 a2 b2 → P a1 b1. +#A #B #R #a2 #b2 #P #H1 #H2 #a1 #b1 #H12 +@(bi_TC_ind_dx_aux ?????? H1 H2 … H12) // +qed-. + +lemma bi_TC_symmetric: ∀A,B,R. bi_symmetric A B R → + bi_symmetric A B (bi_TC … R). +#A #B #R #HR #a1 #a2 #b1 #b2 #H21 +@(bi_TC_ind_dx ?????????? H21) -a2 -b2 /3 width=1/ /3 width=4/ qed. lemma bi_TC_transitive: ∀A,B,R. bi_transitive A B (bi_TC … R). @@ -278,3 +326,17 @@ definition bi_Conf3: ∀A,B,C. relation3 A B C → bi_relation A B → Prop ≝ lemma bi_TC_Conf3: ∀A,B,C,S,R. bi_Conf3 A B C S R → bi_Conf3 A B C S (bi_TC … R). #A #B #C #S #R #HSR #c #a1 #b1 #Hab1 #a2 #b2 #H elim H -a2 -b2 /2 width=4/ qed. + +lemma bi_TC_star_ind: ∀A,B,R. bi_reflexive A B R → ∀a1,b1. ∀P:relation2 A B. + P a1 b1 → (∀a,a2,b,b2. bi_TC … R a1 b1 a b → R a b a2 b2 → P a b → P a2 b2) → + ∀a2,b2. bi_TC … R a1 b1 a2 b2 → P a2 b2. +#A #B #R #HR #a1 #b1 #P #H1 #IH #a2 #b2 #H12 elim H12 -a2 -b2 /3 width=5/ +qed-. + +lemma bi_TC_star_ind_dx: ∀A,B,R. bi_reflexive A B R → + ∀a2,b2. ∀P:relation2 A B. P a2 b2 → + (∀a1,a,b1,b. R a1 b1 a b → bi_TC … R a b a2 b2 → P a b → P a1 b1) → + ∀a1,b1. bi_TC … R a1 b1 a2 b2 → P a1 b1. +#A #B #R #HR #a2 #b2 #P #H2 #IH #a1 #b1 #H12 +@(bi_TC_ind_dx … P ? IH … H12) /3 width=5/ +qed-.