From 95fe49b9bd546ee4f0d27dce7267d7285eb81b01 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 22 Sep 2011 12:25:07 +0000 Subject: [PATCH] - the confluence of context-senstitive parallel reduction (cpr) is closed! - the theory of partial unfold on local environments (ltpss) is set up --- .../lambda-delta/Basic-2/grammar/item.ma | 1 + .../lambda-delta/Basic-2/reduction/cpr.ma | 53 +----- .../lambda-delta/Basic-2/reduction/cpr_cpr.ma | 34 +++- .../Basic-2/reduction/cpr_lift.ma | 32 +++- .../lambda-delta/Basic-2/reduction/tpr.ma | 4 +- .../lambda-delta/Basic-2/reduction/tpr_tps.ma | 56 +++--- .../lambda-delta/Basic-2/unfold/ltpss.ma | 107 +++++++++++ .../Basic-2/unfold/ltpss_ltpss.ma | 55 ++++++ .../lambda-delta/Basic-2/unfold/ltpss_tpss.ma | 169 ++++++++++++++++++ .../lambda-delta/Basic-2/unfold/tpss_tpss.ma | 6 + 10 files changed, 441 insertions(+), 76 deletions(-) create mode 100644 matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss.ma create mode 100644 matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma create mode 100644 matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma index 43b2174d9..ead47b546 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma @@ -14,6 +14,7 @@ (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES * Specification started: 2011 April 17 + * Confluence of context-sensitive parallel reduction closed: 2011 September 21 * Confluence of context-free parallel reduction closed: 2011 September 6 * - Patience on me so that I gain peace and perfection! - * [ suggested invocation to start formal specifications with ] diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma index f4b175925..0e123f64c 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma @@ -13,13 +13,14 @@ (**************************************************************************) include "Basic-2/grammar/cl_shift.ma". +include "Basic-2/unfold/tpss.ma". include "Basic-2/reduction/tpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) (* Basic-1: includes: pr2_delta1 *) definition cpr: lenv → relation term ≝ - λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2. + λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2. interpretation "context-sensitive parallel reduction (term)" @@ -31,26 +32,12 @@ interpretation lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2. /2/ qed. -lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2. +lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2. /3 width=5/ qed. lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T. /2/ qed. -lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → - L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 * /3 width=5/ -qed. - -(* Basic-1: was only: pr2_gen_cbind *) -lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → - L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. -#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 -elim (tps_split_up … HT2 1 ? ?) -HT2 // #T0 (tpr_inv_atom1 … H) -H #H ->(tps_inv_sort1 … H) -H // -qed. - -(* Basic-1: was: pr2_gen_lref *) -lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 → - T2 = #i ∨ - ∃∃K,T. ↓[0, i] L ≡ K. 𝕓{Abbr} T & ↑[0, i + 1] T ≡ T2 & - i < |L|. -#L #T2 #i * #X #H ->(tpr_inv_atom1 … H) -H #H -elim (tps_inv_lref1 … H) -H /2/ -* #K #T #_ #Hi #HLK #HTT2 /3/ +>(tpss_inv_sort1 … H) -H // qed. (* (* Basic-1: was: pr2_gen_cast *) @@ -104,26 +75,16 @@ elim (tpr_inv_cast1 … H) -H /3/ * #V #T #HV1 #HT1 #H whd (* >H in HU2; *) destruct -X; elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H *) -(* Basic forward lemmas *****************************************************) - -lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2. -#L elim L -L -[ /2/ -| normalize /3/ -]. -qed. (* Basic-1: removed theorems 5: pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans + Basic-1: removed local theorems 3: + pr2_free_free pr2_free_delta pr2_delta_delta *) (* pr2/fwd pr2_gen_appl pr2/fwd pr2_gen_abbr -pr2/pr2 pr2_confluence__pr2_free_free -pr2/pr2 pr2_confluence__pr2_free_delta -pr2/pr2 pr2_confluence__pr2_delta_delta -pr2/pr2 pr2_confluence pr2/props pr2_change pr2/subst1 pr2_subst1 pr2/subst1 pr2_gen_cabbr diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma index d544918ac..086209007 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma @@ -17,12 +17,42 @@ include "Basic-2/reduction/cpr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************) +(* Advanced properties ******************************************************) + +lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 → + L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 +@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *) +qed. + +(* Basic-1: was only: pr2_gen_cbind *) +lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 → + L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. +#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2 +elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 (tpr_inv_atom1 … H) -H #H +elim (tpss_inv_lref1 … H) -H /2/ +* /3 width=6/ +qed. + (* Basic-1: was: pr2_gen_abst *) lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. /2/ qed. + +(* Relocation properties ****************************************************) + +(* Basic-1: was: pr2_lift *) + +(* Basic-1: was: pr2_gen_lift *) + diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma index 756527958..fce71d15a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -91,7 +91,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T & U2 = 𝕓{I} V2. T ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr. + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr. /2/ qed. (* Basic-1: was pr0_gen_abbr *) @@ -100,7 +100,7 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & U2 = 𝕓{Abbr} V2. T ) ∨ - ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2. + ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2. #V1 #T1 #U2 #H elim (tpr_inv_bind1 … H) -H * /3 width=7/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma index b7284718a..ac2112c7a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma @@ -12,20 +12,18 @@ (* *) (**************************************************************************) -include "Basic-2/substitution/tps_tps.ma". -include "Basic-2/substitution/ltps_tps.ma". +include "Basic-2/unfold/ltpss_ltpss.ma". include "Basic-2/reduction/ltpr_drop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) -(* Note: the constant 1 comes from tps_subst *) (* Basic-1: was: pr0_subst1 *) lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → - ∀L1,d,U1. L1 ⊢ T1 [d, 1] ≫ U1 → + ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → ∀L2. L1 ⇒ L2 → - ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, 1] ≫ U2. + ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2. #T1 #T2 #H elim H -H T1 T2 -[ #I #L1 #d #X #H +[ #I #L1 #d #e #X #H elim (tps_inv_atom1 … H) -H [ #H destruct -X /2/ | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I; @@ -33,42 +31,43 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X; elim (lift_total V2 0 (i+1)) #U2 #HVU2 lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 - @ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *) + @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *) ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12 +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X; elim (IHV12 … HVW1 … HL12) -IHV12 HVW1; elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/ -| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12 +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y; elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/ -| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12 + lapply (tpss_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/ +| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X; elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - elim (tps_conf_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2 + elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2 lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2 - elim (ltps_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) 1 ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 - lapply (tps_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2 - lapply (tps_trans_ge … HUT2 … HTW2 ?) -HUT2 HTW2 // #HUW2 - /3 width=5/ -| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #X #H #L2 #HL12 + elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 + lapply (tpss_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2 + lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2 + lapply (tpss_leq_repl_dx … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2 + lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/ +| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12 elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X; elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y; elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2 elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2 elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 elim (lift_total VV2 0 1) #VV #H2VV - lapply (tps_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 H2VV ?) -HVV2 HV2 /2/ #HVV - @ex2_1_intro [2: @tpr_theta |1: skip |3: @tps_bind [2: @tps_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) -| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #X #H #L2 #HL12 + lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV + @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *) +| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12 elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X; elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2 elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 (ltps_inv_atom1 … HL2) -HL2 // +qed. +(* +fact ltps_inv_atom2_aux: ∀d,e,L1,L2. + L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆. +#d #e #L1 #L2 * -d e L1 L2 +[ // +| #L #I #V #H destruct +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct +] +qed. + +lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆. +/2 width=5/ qed. + +fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e → + ∀K2,I,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & + K2 ⊢ V1 [0, e - 1] ≫ V2 & + L1 = K1. 𝕓{I} V1. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #_ #K1 #I #V1 #H destruct +| #L1 #I #V #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/ +| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H) +] +qed. + +lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ≫ K2. 𝕓{I} V2 → 0 < e → + ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 & + L1 = K1. 𝕓{I} V1. +/2 width=5/ qed. + +fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d → + ∀I,K2,V2. L2 = K2. 𝕓{I} V2 → + ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & + K2 ⊢ V1 [d - 1, e] ≫ V2 & + L1 = K1. 𝕓{I} V1. +#d #e #L1 #L2 * -d e L1 L2 +[ #d #e #_ #I #K2 #V2 #H destruct +| #L #I #V #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H) +| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2 + /2 width=5/ +] +qed. + +lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d → + ∃∃K1,V1. K1 [d - 1, e] ≫ K2 & + K2 ⊢ V1 [d - 1, e] ≫ V2 & + L1 = K1. 𝕓{I} V1. +/2/ qed. + +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma new file mode 100644 index 000000000..0bf94ae76 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma @@ -0,0 +1,55 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/ltpss_tpss.ma". + +(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) + +(* Main properties **********************************************************) + +theorem ltpss_trans_eq: ∀L1,L,L2,d,e. + L1 [d, e] ≫* L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2. +/2/ qed. + +lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e. + L1 [0, e] ≫* L2 → L2 ⊢ V1 [0, e] ≫* V2 → + L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2 +[ /2/ +| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/ +] +qed. + +lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e. + L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫* V2 → + 0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) /2/ +qed. + +lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e. + L1 [d, e] ≫* L2 → L2 ⊢ V1 [d, e] ≫* V2 → + L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2 +[ /2/ +| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/ +] +qed. + +lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫* V2 → + 0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) /2/ +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma new file mode 100644 index 000000000..b8e425e63 --- /dev/null +++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma @@ -0,0 +1,169 @@ +(**************************************************************************) +(* ___ *) +(* ||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/unfold/tpss_ltps.ma". +include "Basic-2/unfold/ltpss.ma". + +(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************) + +(* Properties concerning partial unfold on terms ****************************) + +lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → + ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫* U2 → + d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2. +#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // +#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 +lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 HTU2 /2/ +qed. + +lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 → + ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → + d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2. +#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2 +@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2/ (**) (* /3 width=6/ is too slow *) +qed. + +lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 → + ∀T2,U2. L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2. +#L0 #L1 #d #e #H @(ltpss_ind … H) -L1 +[ /2/ +| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2 + lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 HTU2 /2/ +] +qed. + +lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 → + ∀T2,U2. L1 ⊢ T2 [d, e] ≫ U2 → L0 ⊢ T2 [d, e] ≫* U2. +/3/ qed. + +lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → + L0 ⊢ T2 [d2, e2] ≫* U2 → L0 [d1, e1] ≫* L1 → + L1 ⊢ T2 [d2, e2] ≫* U2. +#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1 +[ // +| -HTU2 #L #L1 #_ #HL1 #IHL + lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 IHL // +] +qed. + +lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → + L0 ⊢ T2 [d2, e2] ≫ U2 → L0 [d1, e1] ≫* L1 → + L1 ⊢ T2 [d2, e2] ≫* U2. +#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01 +@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2/ (**) (* /3 width=6/ is too slow *) +qed. + +lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e. + L0 ⊢ T2 [d, e] ≫* U2 → L0 [d, e] ≫* L1 → + ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T. +#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1 +[ /2/ +| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2 + elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T + elim (ltps_tpss_conf … HL1 HUW2) -HL1 HUW2 #U #HU2 #HW2U + elim (tpss_conf_eq … HW2T … HW2U) -HW2T HW2U #V #HTV #HUV + lapply (tpss_trans_eq … HT2 … HTV) -T; + lapply (tpss_trans_eq … HU2 … HUV) -U /2/ +] +qed. + +lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e. + L0 ⊢ T2 [d, e] ≫ U2 → L0 [d, e] ≫* L1 → + ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T. +/3/ qed. + +lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 → + ∀L2,ds,es. L1 [ds, es] ≫* L2 → + ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T. +#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2 +[ /3/ +| #L #L2 #HL1 #HL2 * #T #HT1 #HT2 + elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0 + lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 HT0 #HT0 + lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 HT0 #HT0 + lapply (tpss_trans_eq … HT2 … HT0) -T /2/ +] +qed. + +lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 → + ∀L2,ds,es. L1 [ds, es] ≫* L2 → + ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T. +/3/ qed. + +(* Advanced properties ******************************************************) + +lemma ltpss_tps2: ∀L1,L2,I,e. + L1 [0, e] ≫* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ≫ V2 → + L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #e #H @(ltpss_ind … H) -L2 +[ /3/ +| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 + elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 + lapply (IHL … HV1) -IHL HV1 #HL1 + @step /2 width=5/ (**) (* /3 width=5/ is too slow *) +] +qed. + +lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e. + L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 → + 0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He +>(plus_minus_m_m e 1) /2/ +qed. + +lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 → + ∀V1,V2. L2 ⊢ V1 [d, e] ≫ V2 → + L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2 +[ /3/ +| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12 + elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2 + lapply (IHL … HV1) -IHL HV1 #HL1 + @step /2 width=5/ (**) (* /3 width=5/ is too slow *) +] +qed. + +lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e. + L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 → + 0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2. +#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd +>(plus_minus_m_m d 1) /2/ +qed. + +(* Advanced forward lemmas **************************************************) + +lemma ltpss_fwd_tpsa21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 → + ∃∃K2,V2. K1 [0, e - 1] ≫* K2 & K1 ⊢ V1 [0, e - 1] ≫* V2 & + L2 = K2. 𝕓{I} V2. +#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2 +[ /2 width=5/ +| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L; + elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H + lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 + lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ +] +qed. + +lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫* L2 → + ∃∃K2,V2. K1 [d - 1, e] ≫* K2 & + K1 ⊢ V1 [d - 1, e] ≫* V2 & + L2 = K2. 𝕓{I} V2. +#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2 +[ /2 width=5/ +| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L; + elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H + lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2 + lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma index 5cc6b38b7..a84928453 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma @@ -19,6 +19,12 @@ include "Basic-2/unfold/tpss_lift.ma". (* Advanced properties ******************************************************) +lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2. +#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 // +#T #T2 #_ #HT2 #IHT1 +lapply (tps_trans_ge … IHT1 … HT2 ?) // +qed. + lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 → ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫* T. -- 2.39.2