From bdff98417627c404aacec8ebb07812287783c500 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 30 Dec 2012 13:00:21 +0000 Subject: [PATCH] commit completed! some bugs fixed and some instances of auto resized --- .../basic_2/computation/ltprs_ltprs.ma | 2 +- .../basic_2/computation/tprs_tprs.ma | 2 +- .../contribs/lambdadelta/basic_2/notation.ma | 2 +- .../basic_2/reducibility/cfpr_cpr.ma | 2 +- .../lambdadelta/basic_2/reducibility/cpr.ma | 2 +- .../basic_2/reducibility/cpr_lift.ma | 9 +- .../basic_2/reducibility/ltpr_aaa.ma | 63 ++++---- .../basic_2/reducibility/tpr_tpr.ma | 138 ++++++++---------- .../lambdadelta/basic_2/static/aaa.ma | 14 ++ 9 files changed, 114 insertions(+), 120 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma index e529ee31a..aec82cd5a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ltprs_ltprs.ma @@ -25,7 +25,7 @@ lemma ltprs_strip: ∀L1. ∀L:term. L ➡* L1 → ∀L2. L ➡ L2 → (* Main properties **********************************************************) -theorem ltprs_conf: Confluent … ltprs. +theorem ltprs_conf: confluent … ltprs. /3 width=3/ qed. theorem ltprs_trans: Transitive … ltprs. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma index 232244510..ec3c9cc57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma @@ -27,7 +27,7 @@ lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 → (* Main propertis ***********************************************************) (* Basic_1: was: pr1_confluence *) -theorem tprs_conf: Confluent … tprs. +theorem tprs_conf: confluent … tprs. /3 width=3/ qed. (* Basic_1: was: pr1_t *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 3ff8f21e5..728647926 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -370,7 +370,7 @@ notation "hvbox( ⦃ term 46 L1 , term 46 T1 ⦄ ➡ ➡ * break ⦃ term 46 L2 non associative with precedence 45 for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }. -notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ Tterm 46 2 ⦄ )" +notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ term 46 T2 ⦄ )" non associative with precedence 45 for @{ 'PEval $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma index a46c9776b..b5ea1b77e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cfpr_cpr.ma @@ -50,7 +50,7 @@ lemma cfpr_inv_all: ∀L1,L2,L0,T1,T2. L0 ⊢ ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → elim (append_inj_dx … H ?) -H // -HX #_ #H destruct -X lapply (ltpss_sn_fwd_length … HL2) >append_length >append_length #H lapply (injective_plus_r … H) -H #H - @(ex3_1_intro … (⋆.ⓑ{I}V@@Y)) append_length H -H >commutative_plus /3 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma index 22fbfc148..fffaad098 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr.ma @@ -28,7 +28,7 @@ interpretation (* Basic properties *********************************************************) lemma cpr_intro: ∀L,T1,T,T2,d,e. T1 ➡ T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡ T2. -/4 width=3/ qed-. +/3 width=5/ qed-. (* Basic_1: was by definition: pr2_free *) lemma cpr_tpr: ∀T1,T2. T1 ➡ T2 → ∀L. L ⊢ T1 ➡ T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma index 9ff04b705..ae4617f80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/cpr_lift.ma @@ -157,10 +157,13 @@ lemma cpr_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K → #L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2 elim (tpr_inv_lift1 … HU1 … HTU1) -U1 #T #HTU #T1 elim (lt_or_ge (|L|) d) #HLd -[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK [ /5 width=4/ | /2 width=2/ ] +[ elim (tpss_inv_lift1_le … HU2 … HLK … HTU ?) -U -HLK /2 width=2/ + /3 width=7 by ex2_intro, cpr_intro/ | elim (lt_or_ge (|L|) (d + e)) #HLde - [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // [ /5 width=4/ | /2 width=2/ ] - | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // /5 width=4/ + [ elim (tpss_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -U -HLK // /2 width=2/ + /3 width=7 by ex2_intro, cpr_intro/ + | elim (tpss_inv_lift1_be … HU2 … HLK … HTU ? ?) -U -HLK // + /3 width=7 by ex2_intro, cpr_intro/ ] ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma index b45dbb99e..a8b117fec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ltpr_aaa.ma @@ -20,20 +20,23 @@ include "basic_2/reducibility/ltpr_ldrop.ma". (* Properties about atomic arity assignment on terms ************************) -fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A. -#L #T @(fw_ind … L T) -L -T #L #T #IH -#L1 #T1 #A * -L1 -T1 -A -[ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct - >(tpr_inv_atom1 … H) -H // -| #I #L1 #K1 #V1 #B #i #HLK1 #HK1 #H1 #H2 #L2 #HL12 #T2 #H destruct - >(tpr_inv_atom1 … H) -T2 +lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 → + ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A. +#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * * +[1,2,3: + #i #Hn #X #H1 #L2 #HL12 #Y #H2 destruct + >(tpr_inv_atom1 … H2) -Y +|4,5: [ #a ] * #V1 #T1 #Hn #X #H1 #L2 #HL12 #Y #H2 destruct +] +[ >(aaa_inv_sort … H1) -X // +| elim (aaa_inv_lref … H1) #I #K1 #V1 #HLK1 #HA lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 + elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #Y #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (IH … HKV1 … HK1 … HK12 … HV12) // -L1 -K1 -V1 /2 width=5/ -| #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_abbr1 … H) -H * + lapply (IH … HKV1 … HA … HK12 … HV12) -L1 -K1 -V1 /2 width=5/ +| elim (aaa_inv_gref … H1) +| elim (aaa_inv_abbr … H1) -H1 #B #HB #HA + elim (tpr_inv_abbr1 … H2) -H2 * [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct lapply (tps_lsubs_trans … HT2 (L2.ⓓV2) ?) -HT2 /2 width=1/ #HT2 lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB @@ -42,30 +45,30 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T lapply (IH … HA … (L2.ⓓV1) … HT1) /width=5/ -T1 /2 width=1/ -L1 #HA @(aaa_inv_lift … HA … HXT) /2 width=1/ ] -| #a #L1 #V1 #T1 #B #A #HB #HA #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct +| elim (aaa_inv_abst … H1) -H1 #B #A #HB #HA #H destruct + elim (tpr_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HT12 #H destruct lapply (IH … HB … HL12 … HV12) -HB /width=5/ #HB lapply (IH … HA … (L2.ⓛV2) … HT12) -IH -HA -HT12 /width=5/ -T1 /2 width=1/ -| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_appl1 … H) -H * +| elim (aaa_inv_appl … H1) -H1 #B #HB #HA + elim (tpr_inv_appl1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB - lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/ - | #a #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct - elim (aaa_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct - lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB + lapply (IH … HB … HL12 … HV12) -HB -HV12 /width=5/ #HB + lapply (IH … HA … HL12 … HT12) -IH -HA -HL12 -HT12 /width=5/ /2 width=3/ + | #b #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct + elim (aaa_inv_abst … HA) -HA #B0 #A0 #HB0 #HA0 #H destruct + lapply (IH … HB … HL12 … HV12) -HB -HV12 /width=5/ #HB lapply (IH … HB0 … HL12 W2 ?) -HB0 /width=5/ #HB0 - lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -T0 -L1 -V1 /4 width=7/ - | #a #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct - elim (aaa_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0 + lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 // /2 width=1/ -T0 -L1 -V1 /4 width=7/ + | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct + elim (aaa_inv_abbr … HA) -HA #B0 #HW0 #HT0 lapply (IH … HW0 … HL12 … HW02) -HW0 /width=5/ #HW2 - lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0 - lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 [2,4: // |3,5: skip ] /2 width=1/ -V1 -T0 -L1 -W0 #HT2 + lapply (IH … HB … HL12 … HV10) -HB -HV10 /width=5/ #HV0 + lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 // /2 width=1/ -V1 -T0 -L1 -W0 #HT2 @(aaa_abbr … HW2) -HW2 @(aaa_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *) ] -| #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct - elim (tpr_inv_cast1 … H) -H +| elim (aaa_inv_cast … H1) -H1 #HV1 #HT1 + elim (tpr_inv_cast1 … H2) -H2 [ * #V2 #T2 #HV12 #HT12 #H destruct lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2 lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/ @@ -75,10 +78,6 @@ fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T ] qed. -lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 → - ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A. -/2 width=9/ qed. - lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ⁝ A. /2 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma index a4bda6daf..cf82cfc37 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma @@ -196,88 +196,66 @@ qed. (* Confluence ***************************************************************) -fact tpr_conf_aux: - ∀Y0:term. ( - ∀X0:term. #{X0} < #{Y0} → - ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → - ∃∃X. X1 ➡ X & X2 ➡ X - ) → - ∀X0,X1,X2. X0 ➡ X1 → X0 ➡ X2 → X0 = Y0 → - ∃∃X. X1 ➡ X & X2 ➡ X. -#Y0 #IH #X0 #X1 #X2 * -X0 -X1 -[ #I1 #H1 #H2 destruct - lapply (tpr_inv_atom1 … H1) -H1 +(* Basic_1: was: pr0_confluence *) +theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → + ∃∃T. T1 ➡ T & T2 ➡ T. +#T0 @(f_ind … tw … T0) -T0 #n #IH * +[ #I #_ #X1 #X2 #H1 #H2 -n + >(tpr_inv_atom1 … H1) -X1 + >(tpr_inv_atom1 … H2) -X2 (* case 1: atom, atom *) - #H1 destruct // -| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct - elim (tpr_inv_flat1 … H1) -H1 * -(* case 2: flat, flat *) - [ #V2 #T2 #HV02 #HT02 #H destruct - /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) -(* case 3: flat, beta *) - | #b #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct - /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) -(* case 4: flat, theta *) - | #b #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct - /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) -(* case 5: flat, tau *) - | #HT02 #H destruct - /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) - ] -| #a #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct - elim (tpr_inv_appl1 … H1) -H1 * -(* case 6: beta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct - @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/ -(* case 7: beta, beta *) - | #b #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct - /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) -(* case 8, beta, theta (excluded) *) - | #b #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct - ] -| #a #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct - elim (tpr_inv_bind1 … H1) -H1 * -(* case 9: delta, delta *) - [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct - /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) -(* case 10: delta, zeta *) - | #T2 #HT20 #HTX2 #H1 #H2 destruct - /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) - ] -| #a #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct - elim (tpr_inv_appl1 … H1) -H1 * -(* case 11: theta, flat (repeated) *) - [ #V2 #T2 #HV02 #HT02 #H destruct - @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/ -(* case 12: theta, beta (repeated) *) - | #b #V2 #WW0 #TT0 #T2 #_ #_ #H destruct + // +| * [ #a ] #I #V0 #T0 #Hn #X1 #X2 #H1 #H2 + [ elim (tpr_inv_bind1 … H1) -H1 * + [ #V1 #T1 #U1 #HV01 #HT01 #HTU1 #H1 + | #T1 #HT01 #HXT1 #H11 #H12 + ] + elim (tpr_inv_bind1 … H2) -H2 * + [1,3: #V2 #T2 #U2 #HV02 #HT02 #HTU2 #H2 + |2,4: #T2 #HT02 #HXT2 #H21 #H22 + ] destruct +(* case 2: delta, delta *) + [ /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *) +(* case 3: zeta, delta (repeated) *) + | @ex2_commute /3 width=10 by tpr_conf_delta_zeta/ +(* case 4: delta, zeta *) + | /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *) +(* case 5: zeta, zeta *) + | /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) + ] + | elim (tpr_inv_flat1 … H1) -H1 * + [ #V1 #T1 #HV01 #HT01 #H1 + | #b1 #V1 #W1 #U1 #T1 #HV01 #HUT1 #H11 #H12 #H13 + | #b1 #V1 #Y1 #W1 #Z1 #U1 #T1 #HV01 #HWZ1 #HUT1 #HVY1 #H11 #H12 #H13 + | #HX1 #H1 + ] + elim (tpr_inv_flat1 … H2) -H2 * + [1,5,9,13: #V2 #T2 #HV02 #HT02 #H2 + |2,6,10,14: #b2 #V2 #W2 #U2 #T2 #HV02 #HUT2 #H21 #H22 #H23 + |3,7,11,15: #b2 #V2 #Y2 #W2 #Z2 #U2 #T2 #HV02 #HWZ2 #HUT2 #HVY2 #H21 #H22 #H23 + |4,8,12,16: #HX2 #H2 + ] destruct +(* case 6: flat, flat *) + [ /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *) +(* case 7: beta, flat (repeated) *) + | @ex2_commute /3 width=8 by tpr_conf_flat_beta/ +(* case 8: theta, flat (repeated) *) + | @ex2_commute /3 width=11 by tpr_conf_flat_theta/ +(* case 9: tau, flat (repeated) *) + | @ex2_commute /3 width=6 by tpr_conf_flat_cast/ +(* case 10: flat, beta *) + | /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *) +(* case 11: beta, beta *) + | /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *) +(* case 12: flat, theta *) + | /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *) (* case 13: theta, theta *) - | #b #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct - /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) - ] -| #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct - elim (tpr_inv_abbr1 … H1) -H1 * -(* case 14: zeta, delta (repeated) *) - [ #V2 #TT2 #T2 #HV02 #HTT02 #HTT2 #H destruct - @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/ -(* case 15: zeta, zeta *) - | #TT2 #HTT02 #HXTT2 - /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *) - ] -| #V0 #T0 #T1 #HT01 #H1 #H2 destruct - elim (tpr_inv_cast1 … H1) -H1 -(* case 16: tau, flat (repeated) *) - [ * #V2 #T2 #HV02 #HT02 #H destruct - @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/ -(* case 17: tau, tau *) - | #HT02 - /3 width=5 by tpr_conf_tau_tau/ + | /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *) +(* case 14: flat, tau *) + | /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *) +(* case 15: tau, tau *) + | /3 width=5 by tpr_conf_tau_tau/ + ] ] ] qed. - -(* Basic_1: was: pr0_confluence *) -theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 → - ∃∃T. T1 ➡ T & T2 ➡ T. -#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma index 7b4813491..b5f416344 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma @@ -63,6 +63,20 @@ lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ⁝ A → ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A. /2 width=3/ qed-. +fact aaa_inv_gref_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀p. T = §p → ⊥. +#L #T #A * -L -T -A +[ #L #k #q #H destruct +| #I #L #K #V #B #i #HLK #HB #q #H destruct +| #a #L #V #T #B #A #_ #_ #q #H destruct +| #a #L #V #T #B #A #_ #_ #q #H destruct +| #L #V #T #B #A #_ #_ #q #H destruct +| #L #V #T #A #_ #_ #q #H destruct +] +qed. + +lemma aaa_inv_gref: ∀L,A,p. L ⊢ §p ⁝ A → ⊥. +/2 width=6/ qed-. + fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U → ∃∃B. L ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A. #L #T #A * -L -T -A -- 2.39.2