From: Ferruccio Guidi Date: Sun, 24 Jul 2011 18:50:58 +0000 (+0000) Subject: - some renaming X-Git-Tag: make_still_working~2352 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dd88a8fa58d50833118cadd96ba8e3bcf70340a4;p=helm.git - some renaming - first third of confluence (tpr) closed --- diff --git a/matita/matita/lib/lambda-delta/reduction/pr_lift.ma b/matita/matita/lib/lambda-delta/reduction/pr_lift.ma deleted file mode 100644 index f5b4e0a37..000000000 --- a/matita/matita/lib/lambda-delta/reduction/pr_lift.ma +++ /dev/null @@ -1,126 +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 "lambda-delta/substitution/lift_fun.ma". -include "lambda-delta/substitution/lift_main.ma". -include "lambda-delta/substitution/drop_main.ma". -include "lambda-delta/reduction/pr_defs.ma". - -lemma pr_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀d,e,K. ↑[d,e] L ≡ K → - ∀U1. ↑[d,e] T1 ≡ U1 → ∀U2. ↑[d,e] T2 ≡ U2 → K ⊢ U1 ⇒ U2. -#L #T1 #T2 #H elim H -H L T1 T2 -[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // -| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2 - lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; - lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 - /5 width=5/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; - elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 - /3 width=5/ -| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 - /5 width=5/ -| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03 - lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X; - [ -HV12; - elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03 - elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0 - elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L; - @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *) - | -IHV12; - lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23 - lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0 - @pr_delta /width=6/ - ] -| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 - elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; - elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; - elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; - lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3 - @pr_theta /3 width=5/ -| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20 - elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; - lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3 - @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *) -| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2 - elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X; - @pr_tau /2 width=5/ -] -qed. - -lemma pr_inv_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → - ∀d,e,K. ↑[d,e] K ≡ L → ∀U1. ↑[d,e] U1 ≡ T1 → - ∃∃U2. ↑[d,e] U2 ≡ T2 & K ⊢ U1 ⇒ U2. -#L #T1 #T2 #H elim H -H L T1 T2 -[ #L #k #d #e #K #_ #U1 #HU1 - lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ -| #L #i #d #e #K #_ #U1 #HU1 - lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HLK … HV01) -IHV12 #V3 #HV32 #HV03 - elim (IHT12 … HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/ -| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; - elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHT12 … HLK … HT01) -IHT12 HT01 HLK /3 width=5/ -| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHT12 … HT01) -IHT12 HT01 - [3: -HV32 HV03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *) - -HLK HW01 - /3 width=5/ -| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX - lapply (lift_inv_lref2 … HX) -HX * * #Hid #HX destruct -X; - [ -HV12; - elim (drop_conf_lt … HLK … HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31 - elim (IHV12 … HK0L … HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34 - elim (lift_trans_le … HV42 … HV20 ?) -HV42 HV20 V2 // #V2 #HV42 - >arith5 // -Hid #HV20 - @(ex2_1_intro … V2) /2 width=6/ (**) (* /3 width=8/ is slow *) - | -IHV12; - lapply (drop_conf_ge … HLK … HLK0 Hid) -HLK HLK0 L #HK - elim (lift_free … HV20 d (i - e + 1) ? ? ?) -HV20 /2/ - >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *) - ] -| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; - elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; - elim (IHV12 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03 - elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03 - elim (IHT12 … HT01) -IHT12 HT01 - [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3/ is too slow *) - -HLK HW01 #T3 #HT32 #HT03 - elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 - @(ex2_1_intro … (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *) -| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; - elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 - elim (IHT12 … HLK … HT1) -IHT12 HLK HT1 /3 width=5/ -| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX - elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; - elim (IHT12 … HLK … HT01) -IHT12 HLK HT01 /3/ -] -qed. diff --git a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma b/matita/matita/lib/lambda-delta/reduction/pr_pr.ma deleted file mode 100644 index c8942bea2..000000000 --- a/matita/matita/lib/lambda-delta/reduction/pr_pr.ma +++ /dev/null @@ -1,115 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/syntax/weight.ma". -include "lambda-delta/reduction/pr_lift.ma". - -(* SINGLE STEP PARALLEL REDUCTION ON TERMS **********************************) - -(* Confluence lemmas ********************************************************) - -lemma pr_conf_sort_sort: ∀L,k1. ∃∃T0. L ⊢ (⋆k1) ⇒ T0 & L ⊢ (⋆k1) ⇒ T0. -/2/ qed. - -lemma pr_conf_lref_lref: ∀L,i1. ∃∃T0. L ⊢ (#i1) ⇒ T0 & L ⊢ (#i1) ⇒ T0. -/2/ qed. - -lemma pr_conf_bind_bind: - ∀L,I1,V11,V12,T11,T12,V22,T22. ( - ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) → - ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 → - ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0 - ) → - L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 → - L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 → - ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0. -#L #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 -elim (IH … HV1 … HV2) [2: /2/ ] #V #HV1 #HV2 -elim (IH … HT1 … HT2) [2: normalize // ] -HT1 HT2 T11 IH #T #HT1 #HT2 -@ex2_1_intro [2: @pr_bind [3: @HV1 |1: skip |4: - -(* Confluence ***************************************************************) - -lemma pr_conf_aux: - ∀L,T. ( - ∀L1,T1. #[L1, T1] < #[L, T] → - ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 → - ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0 - ) → - ∀K1,U1,T1,K2,U2,T2. K1 ⊢ U1 ⇒ T1 → K2 ⊢ U2 ⇒ T2 → - K1 = L → U1 = T → K2 = L → U2 = T → - ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0. -#L #T #IH #K1 #U1 #T1 #K2 #U2 #T2 -* -K1 U1 T1 -[ #K1 #k1 * -K2 U2 T2 -(* case 1: sort, sort *) - [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -K1 K2 T k2 // -(* case 2: sort, lref (excluded) *) - | #K2 #i2 #H1 #H2 #H3 #H4 destruct -(* case 3: sort, bind (excluded) *) - | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 4: sort, flat (excluded) *) - | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 5: sort, beta (excluded) *) - | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 6: sort, delta (excluded) *) - | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 7: sort, theta (excluded) *) - | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 8: sort, zeta (excluded) *) - | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 9: sort, tau (excluded) *) - | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct - ] -| #K1 #i1 * -K2 U2 T2 -(* case 10: lref, sort (excluded) broken *) - [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -(* case 11: lref, sort (excluded) *) - | #K2 #i2 #H1 #H2 #H3 #H4 destruct -K1 K2 T i2 // -(* case 12: lref, bind (excluded) *) - | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 13: lref, flat (excluded) *) - | #K2 #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 14: lref, beta (excluded) *) - | #K2 #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 15: lref, delta (excluded) *) - | #K2 #K22 #V21 #V22 #V2 #i2 #_ #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 16: lref, theta (excluded) *) - | #K2 #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 17: lref, zeta (excluded) *) - | #K2 #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 #H3 #H4 destruct -(* case 18: lref, tau (excluded) *) - | #K2 #V2 #T21 #T22 #_ #H1 #H2 #H3 #H4 destruct - ] -| #K1 #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -K2 U2 T2 -(* case 19: bind, sort (excluded) broken *) - [ #K2 #k2 #H1 #H2 #H3 #H4 destruct -(* case 20: bind, lref (excluded) *) - | #K2 #i2 #H1 #H2 #H3 #H4 destruct -(* case 21: bind, bind *) - | #K2 #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 #H3 #H4 - destruct -T K1 K2 I2 V21 T21; - - -theorem pr_conf: ∀L,T,T1,T2. L ⊢ T ⇒ T1 → L ⊢ T ⇒ T2 → - ∃∃T0. L ⊢ T1 ⇒ T0 & L ⊢ T2 ⇒ T0. -#L #T @(cw_wf_ind … L T) -L T /3 width=12/ -qed. - -lemma pr_conf_bind_bind: - ∀L,I1,V11,V12,T11,T12,V22,T22. ( - ∀L1,T1. #L1 + #T1 < #L + (#V11 + #T11 + 1) → - ∀T3,T4. L1 ⊢ T1 ⇒ T3 → L1 ⊢ T1 ⇒ T4 → - ∃∃T0. L1 ⊢ T3 ⇒ T0 & L1 ⊢ T4 ⇒ T0 - ) → - L ⊢ V11 ⇒ V12 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T12 → - L ⊢ V11 ⇒ V22 → L. 𝕓{I1} V11 ⊢ T11 ⇒ T22 → - ∃∃T0. L ⊢ 𝕓{I1} V12. T12 ⇒ T0 & L ⊢ 𝕓{I1} V22. T22 ⇒ T0. diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma index 29f8ae4e7..bddd93017 100644 --- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma @@ -9,7 +9,7 @@ \ / V_______________________________________________________________ *) -include "lambda-delta/substitution/subst_defs.ma". +include "lambda-delta/substitution/ps_defs.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) @@ -23,9 +23,8 @@ inductive tpr: term → term → Prop ≝ | tpr_beta : ∀V1,V2,W,T1,T2. tpr V1 V2 → tpr T1 T2 → tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2) -| tpr_delta: ∀V1,V2,T1,T2,T0,T. - tpr V1 V2 → tpr T1 T2 → - ⋆. 𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T → +| tpr_delta: ∀V1,V2,T1,T2,T. + tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T → tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T) | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2. tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 → @@ -37,7 +36,7 @@ inductive tpr: term → term → Prop ≝ interpretation "context-free parallel reduction (term)" - 'PR T1 T2 = (tpr T1 T2). + 'PRed T1 T2 = (tpr T1 T2). (* Basic properties *********************************************************) @@ -59,7 +58,7 @@ lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i → | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct -| #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct +| #V1 #V2 #T1 #T2 #T #_ #_ #_ #_ #_ #i #H destruct | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct | #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/ | #V #T1 #T2 #HT12 #_ #i #H destruct /3/ diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_main.ma b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma new file mode 100644 index 000000000..ec4551f9a --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma @@ -0,0 +1,131 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/substitution/lift_fun.ma". +include "lambda-delta/substitution/lift_main.ma". +include "lambda-delta/substitution/drop_main.ma". +*) +include "lambda-delta/reduction/tpr_defs.ma". + +axiom tpr_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. +(* +#L #T1 #T2 #H elim H -H L T1 T2 +[ #L #k #d #e #K #_ #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; + lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 // +| #L #i #d #e #K #_ #U1 #HU1 #U2 #HU2 + lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; + lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 // +| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 + elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 + /5 width=5/ +| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1; + elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 + /3 width=5/ +| #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 + /5 width=5/ +| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HKL #X #HX #V3 #HV03 + lapply (lift_inv_lref1 … HX) -HX * * #Hid #H destruct -X; + [ -HV12; + elim (lift_trans_ge … HV20 … HV03 ?) -HV20 HV03 V0 // #V0 #HV20 #HV03 + elim (drop_trans_le … HKL … HLK0 ?) -HKL HLK0 L /2/ #L #HKL #HLK0 + elim (drop_inv_skip2 … HLK0 ?) -HLK0 /2/ #K1 #V #HK10 #HV #H destruct -L; + @pr_delta [4,6: // |1,2,3: skip |5: /2 width=5/] (**) (* /2 width=5/ *) + | -IHV12; + lapply (lift_trans_be … HV20 … HV03 ? ?) -HV20 HV03 V0 /2/ #HV23 + lapply (drop_trans_ge … HKL … HLK0 ?) -HKL HLK0 L // -Hid #HKK0 + @pr_delta /width=6/ + ] +| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HKL #X1 #HX1 #X2 #HX2 + elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1; + elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X; + elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct -X2; + elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct -X; + lapply (lift_trans_ge … HV2 … HV3 ?) -HV2 HV3 V // * #V #HV2 #HV3 + @pr_theta /3 width=5/ +| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HKL #X #HX #T0 #HT20 + elim (lift_inv_bind1 … HX) -HX #V3 #T3 #_ #HT3 #HX destruct -X; + lapply (lift_trans_ge … HT1 … HT3 ?) -HT1 HT3 T // * #T #HT1 #HT3 + @pr_zeta [2: // |1:skip | /2 width=5/] (**) (* /2 width=5/ *) +| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HKL #X #HX #T #HT2 + elim (lift_inv_flat1 … HX) -HX #V0 #T0 #_ #HT0 #HX destruct -X; + @pr_tau /2 width=5/ +] +qed. +*) +axiom tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → + ∀d,e,U1. ↑[d, e] U1 ≡ T1 → + ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. +(* +#L #T1 #T2 #H elim H -H L T1 T2 +[ #L #k #d #e #K #_ #U1 #HU1 + lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/ +| #L #i #d #e #K #_ #U1 #HU1 + lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/ +| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; + elim (IHV12 … HLK … HV01) -IHV12 #V3 #HV32 #HV03 + elim (IHT12 … HT01) -IHT12 HT01 [2,3: -HV32 HV03 /3/] -HLK HV01 /3 width=5/ +| #L #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X; + elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 + elim (IHT12 … HLK … HT01) -IHT12 HT01 HLK /3 width=5/ +| #L #V1 #V2 #W1 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 … HLK … HV01) -IHV12 HV01 #V3 #HV32 #HV03 + elim (IHT12 … HT01) -IHT12 HT01 + [3: -HV32 HV03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3 width=5/ is too slow *) + -HLK HW01 + /3 width=5/ +| #L #K0 #V1 #V2 #V0 #i #HLK0 #HV12 #HV20 #IHV12 #d #e #K #HLK #X #HX + lapply (lift_inv_lref2 … HX) -HX * * #Hid #HX destruct -X; + [ -HV12; + elim (drop_conf_lt … HLK … HLK0 Hid) -HLK HLK0 L #L #V3 #HKL #HK0L #HV31 + elim (IHV12 … HK0L … HV31) -IHV12 HK0L HV31 #V4 #HV42 #HV34 + elim (lift_trans_le … HV42 … HV20 ?) -HV42 HV20 V2 // #V2 #HV42 + >arith5 // -Hid #HV20 + @(ex2_1_intro … V2) /2 width=6/ (**) (* /3 width=8/ is slow *) + | -IHV12; + lapply (drop_conf_ge … HLK … HLK0 Hid) -HLK HLK0 L #HK + elim (lift_free … HV20 d (i - e + 1) ? ? ?) -HV20 /2/ + >arith3 /2/ -Hid /3 width=8/ (**) (* just /3 width=8/ is a bit slow *) + ] +| #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct -X; + elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y; + elim (IHV12 ? ? ? HLK ? HV01) -IHV12 HV01 #V3 #HV32 #HV03 + elim (IHW12 ? ? ? HLK ? HW01) -IHW12 #W3 #HW32 #HW03 + elim (IHT12 … HT01) -IHT12 HT01 + [3: -HV2 HV32 HV03 HW32 HW03 @(drop_skip … HLK) /2/ |2: skip ] (**) (* /3/ is too slow *) + -HLK HW01 #T3 #HT32 #HT03 + elim (lift_trans_le … HV32 … HV2 ?) -HV32 HV2 V2 // #V2 #HV32 #HV2 + @(ex2_1_intro … (𝕓{Abbr}W3.𝕗{Appl}V2.T3)) /3/ (**) (* /4/ loops *) +| #L #V #T #T1 #T2 #HT1 #_ #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_bind2 … HX) -HX #V0 #T0 #_ #HT0 #H destruct -X; + elim (lift_div_le … HT1 … HT0 ?) -HT1 HT0 T // #T #HT0 #HT1 + elim (IHT12 … HLK … HT1) -IHT12 HLK HT1 /3 width=5/ +| #L #V #T1 #T2 #_ #IHT12 #d #e #K #HLK #X #HX + elim (lift_inv_flat2 … HX) -HX #V0 #T0 #_ #HT01 #H destruct -X; + elim (IHT12 … HLK … HT01) -IHT12 HLK HT01 /3/ +] +qed. +*) \ No newline at end of file diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma new file mode 100644 index 000000000..4451ec892 --- /dev/null +++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma @@ -0,0 +1,160 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/substitution/lift_weight.ma". +include "lambda-delta/reduction/tpr_main.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) + +(* Confluence lemmas ********************************************************) + +lemma tpr_conf_sort_sort: ∀k1. ∃∃T0. ⋆k1 ⇒ T0 & ⋆k1 ⇒ T0. +/2/ qed. + +lemma tpr_conf_lref_lref: ∀i1. ∃∃T0. #i1 ⇒ T0 & #i1 ⇒ T0. +/2/ qed. + +lemma tpr_conf_bind_bind: + ∀I1,V11,V12,T11,T12,V22,T22. ( + ∀T1. #T1 < #V11 + #T11 + 1 → + ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → + ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ) → + V11 ⇒ V12 → T11 ⇒ T12 → + V11 ⇒ V22 → T11 ⇒ T22 → + ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0. +#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 +elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2 +elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2 +/3 width=5/ +qed. + +lemma tpr_conf_bind_zeta: + ∀V11,V12,T11,T12,T22,T20. ( + ∀T1. #T1 < #V11 + #T11 +1 → + ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → + ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ) → + V11 ⇒ V12 → T22 ⇒ T20 → T11 ⇒ T12 → ↑[O, 1] T22 ≡ T11 → + ∃∃T0. 𝕓{Abbr} V12. T12 ⇒ T0 & T20 ⇒ T0. +#V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT +elim (tpr_inv_lift … HT112 … HT) -HT112 #T #HT12 #HT22 +lapply (tw_lift … HT) -HT #HT +elim (IH … HT202 … HT22) -HT202 HT22 IH /3/ +qed. + +lemma tpr_conf_flat_flat: + ∀I1,V11,V12,T11,T12,V22,T22. ( + ∀T1. #T1 < #V11 + #T11 + 1 → + ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → + ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ) → + V11 ⇒ V12 → T11 ⇒ T12 → + V11 ⇒ V22 → T11 ⇒ T22 → + ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0. +#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2 +elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2 +elim (IH … HT1 … HT2) -HT1 HT2 // #T #HT1 #HT2 +/3 width=5/ +qed. + +(* Confluence ***************************************************************) + +lemma tpr_conf_aux: + ∀T. ( + ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 → + ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0 + ) → + ∀U1,T1,U2,T2. U1 ⇒ T1 → U2 ⇒ T2 → + U1 = T → U2 = T → + ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0. +#T #IH #U1 #T1 #U2 #T2 +* -U1 T1 +[ #k1 * -U2 T2 +(* case 1: sort, sort *) + [ #k2 #H1 #H2 destruct -T k2 // +(* case 2: sort, lref (excluded) *) + | #i2 #H1 #H2 destruct +(* case 3: sort, bind (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 4: sort, flat (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 5: sort, beta (excluded) *) + | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 6: sort, delta (excluded) *) + | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct +(* case 7: sort, theta (excluded) *) + | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct +(* case 8: sort, zeta (excluded) *) + | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct +(* case 9: sort, tau (excluded) *) + | #V2 #T21 #T22 #_ #H1 #H2 destruct + ] +| #i1 * -U2 T2 +(* case 10: lref, sort (excluded) broken *) + [ #k2 #H1 #H2 destruct +(* case 11: lref, sort (excluded) *) + | #i2 #H1 #H2 destruct -T i2 // +(* case 12: lref, bind (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 13: lref, flat (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 14: lref, beta (excluded) *) + | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 15: lref, delta (excluded) *) + | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct +(* case 16: lref, theta (excluded) *) + | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct +(* case 17: lref, zeta (excluded) *) + | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct +(* case 18: lref, tau (excluded) *) + | #V2 #T21 #T22 #_ #H1 #H2 destruct + ] +| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2 +(* case 19: bind, sort (excluded) *) + [ #k2 #H1 #H2 destruct +(* case 20: bind, lref (excluded) *) + | #i2 #H1 #H2 destruct +(* case 21: bind, bind *) + | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 + destruct -T I2 V21 T21 /3 width=7/ +(* case 22: bind, flat (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 23: bind, beta (excluded) *) + | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 24: bind, delta (excluded) *) + | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct +(* case 25: bind, theta (excluded) *) + | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct +(* case 26: bind, zeta *) + | #V2 #T21 #T22 #T20 #HT212 #HT220 #H1 #H2 + destruct -I1 V2 T21 T /3 width=8/ +(* case 27: bind, tau (excluded) *) + | #V2 #T21 #T22 #_ #H1 #H2 destruct + ] +| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2 +(* case 28: flat, sort (excluded) *) + [ #k2 #H1 #H2 destruct +(* case 29: flat, lref (excluded) *) + | #i2 #H1 #H2 destruct +(* case 30: flat, bind (excluded) *) + | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct +(* case 31: flat, flat *) + | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2 + destruct -T I2 V21 T21 /3 width=7/ +(* case 32: flat, beta *) + | #V21 #V22 #W2 #T21 #T22 #HV212 #HT212 #H1 #H2 + destruct -I1 V21 T11 T; + +theorem pr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 → + ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0. +#T @(tw_wf_ind … T) -T /3 width=8/ +qed. diff --git a/matita/matita/lib/lambda-delta/substitution/lift_weight.ma b/matita/matita/lib/lambda-delta/substitution/lift_weight.ma new file mode 100644 index 000000000..73812d071 --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/lift_weight.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "lambda-delta/syntax/weight.ma". +include "lambda-delta/substitution/lift_defs.ma". + +(* RELOCATION ***************************************************************) + +lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2. +#d #e #T1 #T2 #H elim H -d e T1 T2 normalize // +qed. diff --git a/matita/matita/lib/lambda-delta/substitution/ps_defs.ma b/matita/matita/lib/lambda-delta/substitution/ps_defs.ma new file mode 100644 index 000000000..514e0ad2e --- /dev/null +++ b/matita/matita/lib/lambda-delta/substitution/ps_defs.ma @@ -0,0 +1,78 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department of the University of Bologna, Italy. + ||I|| + ||T|| + ||A|| This file is distributed under the terms of the + \ / GNU General Public License Version 2 + \ / + V_______________________________________________________________ *) + +include "lambda-delta/substitution/drop_defs.ma". + +(* PARALLEL SUBSTITUTION ****************************************************) + +inductive ps: lenv → term → nat → nat → term → Prop ≝ +| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k) +| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i) +| ps_subst: ∀L,K,V,U1,U2,i,d,e. + d ≤ i → i < d + e → + ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 → + ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2 +| ps_bind : ∀L,I,V1,V2,T1,T2,d,e. + ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 → + ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) +| ps_flat : ∀L,I,V1,V2,T1,T2,d,e. + ps L V1 d e V2 → ps L T1 d e T2 → + ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) +. + +interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2). + +(* Basic properties *********************************************************) + +lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. +#T elim T -T // +#I elim I -I /2/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & + L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & + U2 = 𝕓{I} V2. T2. +#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 +[ #L #k #d #e #I #V1 #T1 #H destruct +| #L #i #d #e #I #V1 #T1 #H destruct +| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ +| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct +] +qed. + +lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & + L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & + U2 = 𝕓{I} V2. T2. +/2/ qed. + +lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → + ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & + U2 = 𝕗{I} V2. T2. +#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 +[ #L #k #d #e #I #V1 #T1 #H destruct +| #L #i #d #e #I #V1 #T1 #H destruct +| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct +| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ +] +qed. + +lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 → + ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & + U2 = 𝕗{I} V2. T2. +/2/ qed. diff --git a/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma b/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma deleted file mode 100644 index 514e0ad2e..000000000 --- a/matita/matita/lib/lambda-delta/substitution/psubst_defs.ma +++ /dev/null @@ -1,78 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department of the University of Bologna, Italy. - ||I|| - ||T|| - ||A|| This file is distributed under the terms of the - \ / GNU General Public License Version 2 - \ / - V_______________________________________________________________ *) - -include "lambda-delta/substitution/drop_defs.ma". - -(* PARALLEL SUBSTITUTION ****************************************************) - -inductive ps: lenv → term → nat → nat → term → Prop ≝ -| ps_sort : ∀L,k,d,e. ps L (⋆k) d e (⋆k) -| ps_lref : ∀L,i,d,e. ps L (#i) d e (#i) -| ps_subst: ∀L,K,V,U1,U2,i,d,e. - d ≤ i → i < d + e → - ↓[0, i] L ≡ K. 𝕓{Abbr} V → ps K V 0 (d + e - i - 1) U1 → - ↑[0, i + 1] U1 ≡ U2 → ps L (#i) d e U2 -| ps_bind : ∀L,I,V1,V2,T1,T2,d,e. - ps L V1 d e V2 → ps (L. 𝕓{I} V1) T1 (d + 1) e T2 → - ps L (𝕓{I} V1. T1) d e (𝕓{I} V2. T2) -| ps_flat : ∀L,I,V1,V2,T1,T2,d,e. - ps L V1 d e V2 → ps L T1 d e T2 → - ps L (𝕗{I} V1. T1) d e (𝕗{I} V2. T2) -. - -interpretation "parallel substritution" 'PSubst L T1 d e T2 = (ps L T1 d e T2). - -(* Basic properties *********************************************************) - -lemma subst_refl: ∀T,L,d,e. L ⊢ T [d, e] ≫ T. -#T elim T -T // -#I elim I -I /2/ -qed. - -(* Basic inversion lemmas ***************************************************) - -lemma ps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → - ∀I,V1,T1. U1 = 𝕓{I} V1. T1 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & - L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & - U2 = 𝕓{I} V2. T2. -#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 -[ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #I #V1 #T1 #H destruct -| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct -] -qed. - -lemma subst_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫ U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & - L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 & - U2 = 𝕓{I} V2. T2. -/2/ qed. - -lemma subst_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 → - ∀I,V1,T1. U1 = 𝕗{I} V1. T1 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & - U2 = 𝕗{I} V2. T2. -#d #e #L #U1 #U2 #H elim H -H d e L U1 U2 -[ #L #k #d #e #I #V1 #T1 #H destruct -| #L #i #d #e #I #V1 #T1 #H destruct -| #L #K #V #U1 #U2 #i #d #e #_ #_ #_ #_ #_ #_ #I #V1 #T1 #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #I #V #T #H destruct -| #L #J #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #I #V #T #H destruct /2 width=5/ -] -qed. - -lemma subst_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫ U2 → - ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 & - U2 = 𝕗{I} V2. T2. -/2/ qed. diff --git a/matita/matita/lib/lambda-delta/syntax/weight.ma b/matita/matita/lib/lambda-delta/syntax/weight.ma index 8d5ed6835..d076dea9d 100644 --- a/matita/matita/lib/lambda-delta/syntax/weight.ma +++ b/matita/matita/lib/lambda-delta/syntax/weight.ma @@ -35,6 +35,10 @@ definition cw: lenv → term → ? ≝ λL,T. #L + #T. interpretation "weight (closure)" 'Weight L T = (cw L T). +axiom tw_wf_ind: ∀P:term→Prop. + (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) → + ∀T. P T. + axiom cw_wf_ind: ∀P:lenv→term→Prop. (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) → ∀L,T. P L T.