From 0466f6387b02f1d0644fb74eacca237e30589111 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 6 Sep 2011 16:30:41 +0000 Subject: [PATCH] - confluence of context-free reduction on terms (tpr) closed! - substitution lemma for tpr closed! - so-called "substitution lemma" closed! - some annotating --- .../contribs/lambda-delta/Basic-2/Basic-1.txt | 3 + .../lambda-delta/Basic-2/reduction/tpr.ma | 38 ++++--------- .../Basic-2/reduction/tpr_lift.ma | 3 + .../lambda-delta/Basic-2/reduction/tpr_tpr.ma | 7 +++ .../lambda-delta/Basic-2/reduction/tpr_tps.ma | 56 ++++++++++++------- .../Basic-2/substitution/ltps_drop.ma | 2 +- .../Basic-2/substitution/ltps_tps.ma | 50 +++++++++++++++-- .../lambda-delta/Basic-2/substitution/tps.ma | 4 +- .../Basic-2/substitution/tps_tps.ma | 24 ++++++++ matita/matita/contribs/lambda-delta/Makefile | 2 +- 10 files changed, 134 insertions(+), 55 deletions(-) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt index f308d157b..c68d0701f 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt +++ b/matita/matita/contribs/lambda-delta/Basic-2/Basic-1.txt @@ -252,7 +252,10 @@ pc3/subst1 pc3_gen_cabbr pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux pc3/wcpr0 pc3_wcpr0_t pc3/wcpr0 pc3_wcpr0 +pr0/fwd pr0_gen_void pr0/dec nf0_dec +pr0/subst1 pr0_subst1_back +pr0/subst1 pr0_subst1_fwd pr1/pr1 pr1_strip pr1/pr1 pr1_confluence pr1/props pr1_pr0 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 fdfc4f08b..6f90fd907 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma @@ -16,6 +16,7 @@ include "Basic-2/substitution/tps.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) +(* Basic-1: includes: pr0_delta1 *) inductive tpr: term → term → Prop ≝ | tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I}) | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 → @@ -44,6 +45,7 @@ lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 → 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2. /2/ qed. +(* Basic-1: was by definition: pr0_refl *) lemma tpr_refl: ∀T. T ⇒ T. #T elim T -T // #I elim I -I /2/ @@ -63,6 +65,7 @@ fact tpr_inv_atom1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒 ] qed. +(* Basic-1: was: pr0_gen_sort pr0_gen_lref *) lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}. /2/ qed. @@ -91,6 +94,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 → ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr. /2/ qed. +(* Basic-1: was pr0_gen_abbr *) lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 → (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 & ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T & @@ -139,6 +143,7 @@ lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 → | (U0 ⇒ U2 ∧ I = Cast). /2/ qed. +(* Basic-1: was pr0_gen_appl *) lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 & U2 = 𝕔{Appl} V2. T2 @@ -153,6 +158,7 @@ lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 → elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct qed. +(* Basic-1: was: pr0_gen_cast *) lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 → (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2) ∨ T1 ⇒ U2. @@ -185,30 +191,8 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i → T1 = 𝕔{Abbr} V. T | ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T. /2/ qed. -(* -pr0/fwd pr0_gen_sort -pr0/fwd pr0_gen_lref -pr0/fwd pr0_gen_abst -pr0/fwd pr0_gen_appl -pr0/fwd pr0_gen_cast -pr0/fwd pr0_gen_abbr -pr0/fwd pr0_gen_void -pr0/fwd pr0_gen_lift -pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl -pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong -pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta -pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta -pr0/pr0 pr0_confluence__pr0_cong_delta -pr0/pr0 pr0_confluence__pr0_upsilon_upsilon -pr0/pr0 pr0_confluence__pr0_delta_delta -pr0/pr0 pr0_confluence__pr0_delta_tau -pr0/pr0 pr0_confluence -pr0/props pr0_lift -pr0/props pr0_subst0_back -pr0/props pr0_subst0_fwd -pr0/props pr0_subst0 -pr0/subst1 pr0_delta1 -pr0/subst1 pr0_subst1_back -pr0/subst1 pr0_subst1_fwd -pr0/subst1 pr0_subst1 -*) \ No newline at end of file + +(* Basic-1: removed theorems 3: + pr0_subst0_back pr0_subst0_fwd pr0_subst0 + Basic-1: removed local theorems: 1: pr0_delta_tau +*) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma index 412a0a2ed..f06d8980a 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma @@ -17,6 +17,7 @@ include "Basic-2/reduction/tpr.ma". (* Relocation properties ****************************************************) +(* Basic-1: was: pr0_lift *) lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2. #T1 #T2 #H elim H -H T1 T2 @@ -52,6 +53,7 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 → ] qed. +(* Basic-1: was: pr0_gen_lift *) lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 → ∀d,e,U1. ↑[d, e] U1 ≡ T1 → ∃∃U2. ↑[d, e] U2 ≡ T2 & U1 ⇒ U2. @@ -109,6 +111,7 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 ] qed. +(* Basic-1: was pr0_gen_abst *) lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 → ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2. /2/ qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma index 43c48d0f2..ac09a41ef 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma @@ -49,6 +49,10 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2 elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/ qed. +(* basic-1: was: + pr0_cong_upsilon_refl pr0_cong_upsilon_zeta + pr0_cong_upsilon_cong pr0_cong_upsilon_delta +*) fact tpr_conf_flat_theta: ∀V0,V1,T1,V2,V,W0,W2,U0,U2. ( ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 → @@ -111,6 +115,7 @@ elim (IH … HV01 … HV02) -HV01 HV02 // elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/ qed. +(* Basic-1: was: pr0_cong_delta pr0_delta_delta *) fact tpr_conf_delta_delta: ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. ( ∀X0:term. #[X0] < #[V0] + #[T0] + 1 → @@ -146,6 +151,7 @@ lapply (tw_lift … HTT20) -HTT20 #HTT20 elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/ qed. +(* Basic-1: was: pr0_upsilon_upsilon *) fact tpr_conf_theta_theta: ∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. ( ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 → @@ -274,6 +280,7 @@ fact tpr_conf_aux: ] qed. +(* Basic-1: was: pr0_confluence *) theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ⇒ T1 → T0 ⇒ T2 → ∃∃T. T1 ⇒ T & T2 ⇒ T. #T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/ 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 af61e0a3f..b7284718a 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 @@ -13,17 +13,19 @@ (**************************************************************************) include "Basic-2/substitution/tps_tps.ma". +include "Basic-2/substitution/ltps_tps.ma". include "Basic-2/reduction/ltpr_drop.ma". (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************) -axiom tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → - ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 → +(* 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 → ∀L2. L1 ⇒ L2 → - ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2. -(* + ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, 1] ≫ U2. #T1 #T2 #H elim H -H T1 T2 -[ #I #L1 #d #e #X #H +[ #I #L1 #d #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,28 +35,44 @@ axiom tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 → lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12 @ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *) ] -| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #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 #e #X #H #L2 #HL12 +| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #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} W) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 - lapply (tps_leq_repl … HTT2 (L2. 𝕓{Abbr} V2) ?) -HTT2 /3 width=5/ -| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12 + 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 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} V2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2 -(*lapply (tps_leq_repl … HTT2 (L2. 𝕓{I} VV2) ?) -HTT2 /2/ #HTT2 *) - elim (tps_conf_neq … HTU2 … HTT2 ?) -HTU2 HTT2 T2 /2/ #T2 #HUT2 #HTT2 - @ex2_1_intro - [2: @tpr_delta [4: @HVV12 |5: @HTT12 |1,2: skip |6: ] (*|6: ]1,2: skip ]*) - |1: skip - |3: @tps_bind [@HVV2 | @HUT2 ] - ] -*) + 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 + 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 (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 + 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 - (u1,u:?; i:?) (subst0 i u u1 u2) -> - (EX t | (subst0 j u1 t1 t) & (subst0 (S (plus i j)) u t t2)). -*) \ No newline at end of file +lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → + ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 → + L1 ⊢ T2 [d2, e2] ≫ U2. +#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2 +[ // +| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2 + lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2 + lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2 + @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *) +| /3/ +] +qed. + +lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 → + ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → + ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T & + L0 ⊢ T [d1, e1] ≫ U2. +#L0 #T2 #U2 #d2 #e2 #H elim H -H L0 T2 U2 d2 e2 +[ /2/ +| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 + elim (lt_or_ge i2 d1) #Hi2d1 + [ elim (ltps_drop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1 + elim (ltps_inv_tps12 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; + lapply (drop_fwd_drop2 … HLK0) -HLK0 #H + elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 + lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // >arith_a2 /3/ + | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2 + [ elim (ltps_drop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1 + elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X; + lapply (drop_fwd_drop2 … HLK0) -HLK0 #H + elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1 + lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // normalize #HW01 + lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 // + | lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/ + ] + ] +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2 + elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 [2: /2/ ] -HL10 /3 width=5/ +| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 + elim (IHVW2 … HL10) -IHVW2; + elim (IHTU2 … HL10) -IHTU2 HL10 /3 width=5/ +] +qed. diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma index 0acbc3d4f..d197da9e8 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma @@ -201,9 +201,9 @@ lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2. (* Basic-1: removed theorems 23: subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans - subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s + subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt - subst0_confluence_neq subst0_confluence_eq subst0_tlt_head + subst0_confluence_neq subst0_confluence_eq subst0_tlt_head subst0_confluence_lift subst0_tlt subst1_head subst1_gen_head *) diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma index 3daf6fbe2..10102eca5 100644 --- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma +++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_tps.ma @@ -83,6 +83,30 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫ T1 → ] qed. +(* Note: the constant 1 comes from tps_subst *) +theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ≫ T0 → + ∀T2. L ⊢ T0 [d, 1] ≫ T2 → 1 ≤ e → + L ⊢ T1 [d, e] ≫ T2. +#L #T1 #T0 #d #e #H elim H -L T1 T0 d e +[ #L #I #d #e #T2 #H #He + elim (tps_inv_atom1 … H) -H + [ #H destruct -T2 // + | * #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct -I; + lapply (lt_to_le_to_lt … (d + e) Hide2 ?) /2/ + ] +| #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He + lapply (tps_weak … HVT2 0 (i +1) ? ?) -HVT2 /2/ #HVT2 + <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2/ +| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He + elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X; + lapply (tps_leq_repl_dx … HT02 (L. 𝕓{I} V0) ?) -HT02 /2/ #HT02 + lapply (IHT10 … HT02 He) -IHT10 HT02 #HT12 + lapply (tps_leq_repl_dx … HT12 (L. 𝕓{I} V2) ?) -HT12 /3/ +| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He + elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct -X /3/ +] +qed. + theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫ T0 → ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 → ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫ T2. diff --git a/matita/matita/contribs/lambda-delta/Makefile b/matita/matita/contribs/lambda-delta/Makefile index 6bf2516d4..77f49615d 100644 --- a/matita/matita/contribs/lambda-delta/Makefile +++ b/matita/matita/contribs/lambda-delta/Makefile @@ -54,7 +54,7 @@ stats: $(PACKAGES:%=%.stats) @printf '\e[0m\n' @printf '\e[1;40;31m' @printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l` - @printf ' %-8s %5i' Comments `grep "(\*[^*]*$$" $(MAS) | wc -l` + @printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l` @printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l` @printf ' %-10s' '' @printf '\e[0m\n' -- 2.39.2