From dd88a8fa58d50833118cadd96ba8e3bcf70340a4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 24 Jul 2011 18:50:58 +0000 Subject: [PATCH] - some renaming - first third of confluence (tpr) closed --- .../lib/lambda-delta/reduction/pr_pr.ma | 115 ------------- .../lib/lambda-delta/reduction/tpr_defs.ma | 11 +- .../reduction/{pr_lift.ma => tpr_main.ma} | 19 ++- .../lib/lambda-delta/reduction/tpr_tpr.ma | 160 ++++++++++++++++++ .../lambda-delta/substitution/lift_weight.ma | 22 +++ .../{psubst_defs.ma => ps_defs.ma} | 0 .../matita/lib/lambda-delta/syntax/weight.ma | 4 + 7 files changed, 203 insertions(+), 128 deletions(-) delete mode 100644 matita/matita/lib/lambda-delta/reduction/pr_pr.ma rename matita/matita/lib/lambda-delta/reduction/{pr_lift.ma => tpr_main.ma} (94%) create mode 100644 matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma create mode 100644 matita/matita/lib/lambda-delta/substitution/lift_weight.ma rename matita/matita/lib/lambda-delta/substitution/{psubst_defs.ma => ps_defs.ma} (100%) 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/pr_lift.ma b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma similarity index 94% rename from matita/matita/lib/lambda-delta/reduction/pr_lift.ma rename to matita/matita/lib/lambda-delta/reduction/tpr_main.ma index f5b4e0a37..ec4551f9a 100644 --- a/matita/matita/lib/lambda-delta/reduction/pr_lift.ma +++ b/matita/matita/lib/lambda-delta/reduction/tpr_main.ma @@ -12,13 +12,16 @@ (* *) (**************************************************************************) +(* 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". +*) +include "lambda-delta/reduction/tpr_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. +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; @@ -67,10 +70,11 @@ lemma pr_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → ∀d,e,K. ↑[d,e] L ≡ K → @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. +*) +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/ @@ -124,3 +128,4 @@ lemma pr_inv_lift: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → 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/psubst_defs.ma b/matita/matita/lib/lambda-delta/substitution/ps_defs.ma similarity index 100% rename from matita/matita/lib/lambda-delta/substitution/psubst_defs.ma rename to matita/matita/lib/lambda-delta/substitution/ps_defs.ma 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. -- 2.39.2