X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freducibility%2Ftpr_tpr.ma;h=a733345bf49dd003641a55192206773466a81c44;hb=eb4b3b1b307fc392c36f0be253e6a111553259bc;hp=a4bda6daf852e8c81a4e6d64d5018997b77350c2;hpb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;p=helm.git 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..a733345bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reducibility/tpr_tpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reducibility/tpr_tpss.ma". +include "basic_2/reducibility/ltpr_tpss.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -23,7 +23,7 @@ fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X. fact tpr_conf_flat_flat: ∀I,V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -36,7 +36,7 @@ qed. fact tpr_conf_flat_beta: ∀a,V0,V1,T1,V2,W0,U0,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -55,7 +55,7 @@ qed. *) fact tpr_conf_flat_theta: ∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{U0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -71,7 +71,7 @@ elim (tpr_inv_abbr1 … H) -H * [ -HV2 -HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct elim (IH … HW02 … HWW2) -HW02 -HWW2 /2 width=1/ #W #HW02 #HWW2 elim (IH … HU02 … HUU02) -HU02 -HUU02 -IH /2 width=1/ #U #HU2 #HUUU2 - elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 + elim (tpr_tps_conf_bind … HWW2 HUUU2 … HUU2) -UU2 #UUU #HUUU2 #HUUU1 @ex2_intro [2: @tpr_theta [6: @HVV |7: @HWW2 |8: @HUUU2 |1,2,3,4: skip | // ] |1:skip @@ -87,7 +87,7 @@ qed. fact tpr_conf_flat_cast: ∀X2,V0,V1,T0,T1. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -99,7 +99,7 @@ qed. fact tpr_conf_beta_beta: ∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -113,7 +113,7 @@ qed. (* Basic_1: was: pr0_cong_delta pr0_delta_delta *) fact tpr_conf_delta_delta: ∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -124,15 +124,15 @@ fact tpr_conf_delta_delta: #a #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2 elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2 -elim (tpr_tps_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1 -elim (tpr_tps_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2 +elim (tpr_tps_conf_bind … HV1 HT1 … HTT1) -T1 #U1 #TTU1 #HTU1 +elim (tpr_tps_conf_bind … HV2 HT2 … HTT2) -T2 #U2 #TTU2 #HTU2 elim (tps_conf_eq … HTU1 … HTU2) -T #U #HU1 #HU2 @ex2_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *) qed. fact tpr_conf_delta_zeta: ∀X2,V0,V1,T0,T1,TT1,T2. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -141,7 +141,7 @@ fact tpr_conf_delta_zeta: ∃∃X. +ⓓV1. TT1 ➡ X & X2 ➡ X. #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HT02 #HXT2 elim (IH … HT01 … HT02) -IH -HT01 -HT02 // -V0 -T0 #T #HT1 #HT2 -elim (tpr_tps_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT +elim (tpr_tps_conf_bind ? ? V1 … HT1 HTT1) -T1 // #TT #HTT1 #HTT elim (tpr_inv_lift1 … HT2 … HXT2) -T2 #X #HXT #HX2 lapply (tps_inv_lift1_eq … HTT … HXT) -HTT #H destruct /3 width=3/ qed. @@ -149,7 +149,7 @@ qed. (* Basic_1: was: pr0_upsilon_upsilon *) fact tpr_conf_theta_theta: ∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( - ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + (♯{W0} + ♯{T0} + 1) + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -168,7 +168,7 @@ qed. fact tpr_conf_zeta_zeta: ∀V0:term. ∀X2,TT0,T0,T1,TT2. ( - ∀X0:term. #{X0} < #{V0} + #{TT0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{TT0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -184,7 +184,7 @@ qed. fact tpr_conf_tau_tau: ∀V0,T0:term. ∀X2,T1. ( - ∀X0:term. #{X0} < #{V0} + #{T0} + 1 → + ∀X0:term. ♯{X0} < ♯{V0} + ♯{T0} + 1 → ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 → ∃∃X. X1 ➡ X & X2 ➡ X ) → @@ -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. +qed-.