From: Ferruccio Guidi Date: Tue, 14 Aug 2018 18:31:06 +0000 (+0200) Subject: severe bug found in parallel zeta X-Git-Tag: make_still_working~288 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7 severe bug found in parallel zeta the transition was not parallel, now it is. + partial commit: component "rt_transition" corrected and minor bugs ficed + some additions in static_2 to support the correction --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index 0ca16ee93..1ebd7f744 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -41,8 +41,8 @@ inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝ | cpg_cast : ∀cU,cT,G,L,U1,U2,T1,T2. Rt cU cT → cpg Rt h cU G L U1 U2 → cpg Rt h cT G L T1 T2 → cpg Rt h (cU∨cT) G L (ⓝU1.T1) (ⓝU2.T2) -| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg Rt h c G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2 +| cpg_zeta : ∀c,G,L,V,T1,T,T2. ⬆*[1] T ≘ T1 → cpg Rt h c G L T T2 → + cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2 | cpg_eps : ∀c,G,L,V,T1,T2. cpg Rt h c G L T1 T2 → cpg Rt h (c+𝟙𝟘) G L (ⓝV.T1) T2 | cpg_ee : ∀c,G,L,V1,V2,T. cpg Rt h c G L V1 V2 → cpg Rt h (c+𝟘𝟙) G L (ⓝV1.T) V2 | cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2. @@ -153,7 +153,7 @@ fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 & U2 = ⓑ{p,J}V2.T2 & c = ((↕*cV)∨cT) - | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≘ T & + | ∃∃cT,T. ⬆*[1] T ≘ U1 & ⦃G, L⦄ ⊢ T ⬈[Rt, cT, h] U2 & p = true & J = Abbr & c = cT+𝟙𝟘. #Rt #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #q #J #W #U1 #H destruct @@ -175,14 +175,14 @@ qed-. lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & U2 = ⓑ{p,I}V2.T2 & c = ((↕*cV)∨cT) - | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≘ T & + | ∃∃cT,T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ⬈[Rt, cT, h] U2 & p = true & I = Abbr & c = cT+𝟙𝟘. /2 width=3 by cpg_inv_bind1_aux/ qed-. lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & U2 = ⓓ{p}V2.T2 & c = ((↕*cV)∨cT) - | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≘ T & + | ∃∃cT,T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ⬈[Rt, cT, h] U2 & p = true & c = cT+𝟙𝟘. #Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * /3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index a98e061f3..37ac3fa83 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -115,10 +115,9 @@ lemma cpg_lifts_sn: ∀Rt. reflexive … Rt → elim (IH … HV12 … HLK … HVW1) -HV12 // elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] /3 width=5 by cpg_bind, lifts_bind, ex2_intro/ - | #cT #T2 #HT12 #HXT2 #H1 #H2 #H3 destruct - elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] #U2 #HTU2 #HU12 - lapply (lifts_trans … HXT2 … HTU2 ??) -T2 [3: |*: // ] #HXU2 - elim (lifts_split_trans … HXU2 f (𝐔❴↑O❵)) [2: /2 width=1 by after_uni_one_dx/ ] + | #cT #T2 #HT21 #HTX2 #H1 #H2 #H3 destruct + elim (lifts_trans4_one … HT21 … HTU1) -HTU1 #U2 #HTU2 #HU21 + elim (IH … HTX2 … HLK … HTU2) [| /3 width=1 by fqup_zeta/ ] -K -V1 -T1 -T2 /3 width=5 by cpg_zeta, ex2_intro/ ] | * #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct @@ -199,9 +198,10 @@ lemma cpg_inv_lifts_sn: ∀Rt. reflexive … Rt → elim (IH … HW12 … HLK … HVW1) -HW12 // elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] /3 width=5 by cpg_bind, lifts_bind, ex2_intro/ - | #cU #U2 #HU12 #HXU2 #H1 #H2 #H3 destruct - elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip, ext2_pair/ ] #T2 #HTU2 #HT12 - elim (lifts_div4_one … HTU2 … HXU2) -U2 /3 width=5 by cpg_zeta, ex2_intro/ + | #cU #U2 #HU21 #HUX2 #H1 #H2 #H3 destruct + elim (lifts_div4_one … HTU1 … HU21) -HTU1 #T2 #HT21 #HTU2 + elim (IH … HUX2 … HLK … HTU2) [| /3 width=1 by fqup_zeta/ ] -L -W1 -U1 -U2 + /3 width=5 by cpg_zeta, ex2_intro/ ] | * #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index 3649bada4..a8202b637 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -76,9 +76,10 @@ lemma cpm_cast: ∀n,h,G,L,U1,U2,T1,T2. qed. (* Basic_2A1: includes: cpr_zeta *) -lemma cpm_zeta: ∀n,h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → - ⬆*[1] T2 ≘ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[n, h] T2. -#n #h #G #L #V #T1 #T #T2 * +lemma cpm_zeta (n) (h) (G) (L): + ∀T1,T. ⬆*[1] T ≘ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[n,h] T2 → + ∀V. ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[n, h] T2. +#n #h #G #L #T1 #T #HT1 #T2 * /3 width=5 by cpg_zeta, isrt_plus_O2, ex2_intro/ qed. @@ -143,11 +144,11 @@ lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → qed-. lemma cpm_inv_sort1: ∀n,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[n,h] T2 → - ∨∨ T2 = ⋆s ∧ n = 0 - | T2 = ⋆(next h s) ∧ n = 1. -#n #h #G #L #T2 #s * #c #Hc #H elim (cpg_inv_sort1 … H) -H * -#H1 #H2 destruct -/4 width=1 by isrt_inv_01, isrt_inv_00, or_introl, or_intror, conj/ + ∧∧ T2 = ⋆(((next h)^n) s) & n ≤ 1. +#n #h #G #L #T2 #s * #c #Hc #H +elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct +[ lapply (isrt_inv_00 … Hc) | lapply (isrt_inv_01 … Hc) ] -Hc +#H destruct /2 width=1 by conj/ qed-. lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[n, h] T2 → @@ -185,15 +186,15 @@ qed-. lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 & U2 = ⓑ{p,I}V2.T2 - | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≘ T & + | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ➡[n, h] U2 & p = true & I = Abbr. #n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ -| #cT #T2 #HT12 #HUT2 #H1 #H2 #H3 destruct - /5 width=3 by isrt_inv_plus_O_dx, ex4_intro, ex2_intro, or_intror/ +| #cT #T2 #HT21 #HTU2 #H1 #H2 #H3 destruct + /5 width=5 by isrt_inv_plus_O_dx, ex4_intro, ex2_intro, or_intror/ ] qed-. @@ -202,14 +203,11 @@ qed-. lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T2 & U2 = ⓓ{p}V2.T2 - | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≘ T & p = true. -#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H * -[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct - elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct - elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct - /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ -| #cT #T2 #HT12 #HUT2 #H1 #H2 destruct - /5 width=3 by isrt_inv_plus_O_dx, ex3_intro, ex2_intro, or_intror/ + | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ➡[n, h] U2 & p = true. +#n #h #p #G #L #V1 #T1 #U2 #H +elim (cpm_inv_bind1 … H) -H +[ /3 width=1 by or_introl/ +| * /3 width=3 by ex3_intro, or_intror/ ] qed-. @@ -218,11 +216,11 @@ qed-. lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[n, h] U2 → ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡[n, h] T2 & U2 = ⓛ{p}V2.T2. -#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abst1 … H) -H -#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct -elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct -elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct -/3 width=5 by ex3_2_intro, ex2_intro/ +#n #h #p #G #L #V1 #T1 #U2 #H +elim (cpm_inv_bind1 … H) -H +[ /3 width=1 by or_introl/ +| * #T #_ #_ #_ #H destruct +] qed-. (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *) @@ -304,8 +302,8 @@ lemma cpm_ind (h): ∀Q:relation5 nat genv lenv term term. Q 0 G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓐV1.T1) (ⓐV2.T2) ) → (∀n,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → Q n G L V1 V2 → Q n G L T1 T2 → Q n G L (ⓝV1.T1) (ⓝV2.T2) - ) → (∀n,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → Q n G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → Q n G L (+ⓓV.T1) T2 + ) → (∀n,G,L,V,T1,T,T2. ⬆*[1] T ≘ T1 → ⦃G, L⦄ ⊢ T ➡[n, h] T2 → + Q n G L T T2 → Q n G L (+ⓓV.T1) T2 ) → (∀n,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → Q n G L T1 T2 → Q n G L (ⓝV.T1) T2 ) → (∀n,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → @@ -337,7 +335,7 @@ elim H -c -G -L -T1 -T2 | #cU #cT #G #L #U1 #U2 #T1 #T2 #HUT #HU12 #HT12 #IHU #IHT #n #H elim (isrt_inv_max_eq_t … H) -H // #HcV #HcT /3 width=3 by ex2_intro/ -| #c #G #L #V #T1 #T2 #T #HT12 #HT2 #IH #n #H +| #c #G #L #V #T1 #T #T2 #HT1 #HT2 #IH #n #H lapply (isrt_inv_plus_O_dx … H ?) -H // #Hc /3 width=4 by ex2_intro/ | #c #G #L #U #T1 #T2 #HT12 #IH #n #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma index 46a1e039d..beddc2697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -143,9 +143,9 @@ fact cpm_fwd_plus_aux (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → elim IHU [|*: // ] -IHU #U #HU1 #HU2 elim IHT [|*: // ] -IHT #T #HT1 #HT2 /3 width=5 by cpm_cast, ex2_intro/ -| #n #G #K #V #T1 #T2 #V2 #_ #IH #HVT2 #n1 #n2 #H destruct +| #n #G #K #V #U1 #T1 #T2 #HTU1 #_ #IH #n1 #n2 #H destruct elim IH [|*: // ] -IH #T #HT1 #HT2 - /3 width=6 by cpm_zeta, cpm_bind, ex2_intro/ + /3 width=3 by cpm_zeta, ex2_intro/ | #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct elim IH [|*: // ] -IH #T #HT1 #HT2 /3 width=3 by cpm_eps, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma new file mode 100644 index 000000000..0b15ef813 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/syntax/tdeq.ma". +include "basic_2/rt_transition/cpm_drops.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Inversion lemmas with degree-based equivalence for terms *****************) + +lemma cpm_tdeq_inv_lref (n) (h) (o) (G) (L) (i): + ∀X. ⦃G, L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X → + ∧∧ X = #i & n = 0. +#n #h #o #G #L #i #X #H1 #H2 +lapply (tdeq_inv_lref1 … H2) -H2 #H destruct +elim (cpm_inv_lref1_drops … H1) -H1 // * [| #m ] +#K #V1 #V2 #_ #_ #H -V1 +elim (lifts_inv_lref2_uni_lt … H) -H // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index a3cfa2c8c..fb1f479dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -50,7 +50,7 @@ qed-. (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *) lemma cpr_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h] T2 → T2 = ⋆s. -#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H * [ // ] #_ #H destruct +#h #G #L #T2 #s #H elim (cpm_inv_sort1 … H) -H // qed-. lemma cpr_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[h] T2 → @@ -113,8 +113,8 @@ lemma cpr_ind (h): ∀Q:relation4 genv lenv term term. Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) - ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → Q G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T,T2. ⬆*[1] T ≘ T1 → ⦃G, L⦄ ⊢ T ➡[h] T2 → + Q G L T T2 → Q G L (+ⓓV.T1) T2 ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → Q G L T1 T2 → Q G L (ⓝV.T1) T2 ) → (∀p,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index c66c7e94d..2e657b027 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -56,9 +56,10 @@ lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2. /3 width=5 by cpg_appl, cpg_cast, ex_intro/ qed. -lemma cpx_zeta: ∀h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → - ⬆*[1] T2 ≘ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈[h] T2. -#h #G #L #V #T1 #T #T2 * +lemma cpx_zeta (h) (G) (L): + ∀T1,T. ⬆*[1] T ≘ T1 → ∀T2. ⦃G, L⦄ ⊢ T ⬈[h] T2 → + ∀V. ⦃G, L⦄ ⊢ +ⓓV.T1 ⬈[h] T2. +#h #G #L #T1 #T #HT1 #T2 * /3 width=4 by cpg_zeta, ex_intro/ qed. @@ -140,7 +141,7 @@ qed-. lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 & U2 = ⓑ{p,I}V2.T2 - | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≘ T & + | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ⬈[h] U2 & p = true & I = Abbr. #h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H * /4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/ @@ -149,7 +150,7 @@ qed-. lemma cpx_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[h] U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T2 & U2 = ⓓ{p}V2.T2 - | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≘ T & p = true. + | ∃∃T. ⬆*[1] T ≘ T1 & ⦃G, L⦄ ⊢ T ⬈[h] U2 & p = true. #h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abbr1 … H) -H * /4 width=5 by ex3_2_intro, ex3_intro, ex_intro, or_introl, or_intror/ qed-. @@ -242,8 +243,8 @@ lemma cpx_ind: ∀h. ∀Q:relation4 genv lenv term term. Q G L V1 V2 → Q G (L.ⓑ{I}V1) T1 T2 → Q G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L V1 V2 → Q G L T1 T2 → Q G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) - ) → (∀G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T → Q G (L.ⓓV) T1 T → - ⬆*[1] T2 ≘ T → Q G L (+ⓓV.T1) T2 + ) → (∀G,L,V,T1,T,T2. ⬆*[1] T ≘ T1 → ⦃G, L⦄ ⊢ T ⬈[h] T2 → Q G L T T2 → + Q G L (+ⓓV.T1) T2 ) → (∀G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → Q G L T1 T2 → Q G L (ⓝV.T1) T2 ) → (∀G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → Q G L V1 V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma index a836bfbea..b0d2b9922 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_req.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "static_2/static/req.ma". +include "static_2/static/req_drops.ma". include "basic_2/rt_transition/rpx_fsle.ma". (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) @@ -32,8 +32,10 @@ lemma req_cpx_trans: ∀h,G. req_transitive (cpx h G). elim (req_inv_bind … H) -H /3 width=1 by cpx_bind/ | #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (req_inv_flat … H) -H /3 width=1 by cpx_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IH #L1 #H - elim (req_inv_bind … H) -H /3 width=3 by cpx_zeta/ +| #G #L2 #V2 #T1 #T #T2 #HT1 #_ #IH #L1 #H + elim (req_inv_bind … H) -H #HV2 #H + lapply (req_inv_lifts_bi … H (Ⓣ) … HT1) -H [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT + /3 width=3 by cpx_zeta/ | #G #L2 #W1 #T1 #T2 #_ #IH #L1 #H elim (req_inv_flat … H) -H /3 width=1 by cpx_eps/ | #G #L2 #W1 #W2 #T1 #_ #IH #L1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma index 3726639cd..7dedda628 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_lpr.ma @@ -20,6 +20,11 @@ include "basic_2/rt_transition/lpr_drops.ma". (* PARALLEL R-TRANSITION FOR FULL LOCAL ENVIRONMENTS ************************) +definition IH_cpr_conf_lpr (h): relation3 genv lenv term ≝ λG,L,T. + ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → + ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0. + (* Main properties with context-sensitive parallel reduction for terms ******) fact cpr_conf_lpr_atom_atom (h): @@ -27,16 +32,13 @@ fact cpr_conf_lpr_atom_atom (h): /2 width=3 by cpr_refl, ex2_intro/ qed-. fact cpr_conf_lpr_atom_delta (h): - ∀G,L0,i. ( - ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,i. ( + ∀G,L,T. ⦃G0, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → ∀K0,V0. ⬇*[i] L0 ≘ K0.ⓓV0 → - ∀V2. ⦃G, K0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ #i ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T. + ∀V2. ⦃G0, K0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ #i ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T. #h #G0 #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 elim (lpr_drops_conf … HLK0 … HL01) -HL01 // #X1 #H1 #HLK1 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct @@ -51,18 +53,15 @@ qed-. (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) fact cpr_conf_lpr_delta_delta (h): - ∀G,L0,i. ( - ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,i. ( + ∀G,L,T. ⦃G0, L0, #i⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → ∀K0,V0. ⬇*[i] L0 ≘ K0.ⓓV0 → - ∀V1. ⦃G, K0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⬆*[↑i] V1 ≘ T1 → + ∀V1. ⦃G0, K0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⬆*[↑i] V1 ≘ T1 → ∀KX,VX. ⬇*[i] L0 ≘ KX.ⓓVX → - ∀V2. ⦃G, KX⦄ ⊢ VX ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T. + ∀V2. ⦃G0, KX⦄ ⊢ VX ➡[h] V2 → ∀T2. ⬆*[↑i] V2 ≘ T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T. #h #G0 #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 #KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 lapply (drops_mono … H … HLK0) -H #H destruct @@ -79,16 +78,13 @@ elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -V1 -HLK1 #T #HVT #HT1 qed-. fact cpr_conf_lpr_bind_bind (h): - ∀p,I,G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓑ{p,I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀p,I,G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓑ{p,I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G0, L0.ⓑ{I}V0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[h] T. #h #p #I #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // @@ -97,54 +93,43 @@ elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH qed-. fact cpr_conf_lpr_bind_zeta (h): - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 → - ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T2 → ∀X2. ⬆*[1] X2 ≘ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ X2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 → + ∀T2. ⬆*[1]T2 ≘ T0 → ∀X2. ⦃G0, L0⦄ ⊢ T2 ➡[h] X2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ +ⓓV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ X2 ➡[h] T. #h #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 -#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2 -elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 -/3 width=3 by cpm_zeta, drops_refl, drops_drop, ex2_intro/ +#T2 #HT20 #X2 #HTX2 #L1 #HL01 #L2 #HL02 +elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01 [| /3 width=1 by drops_refl, drops_drop/ ] #T #HT1 #HT2 +elim (IH … HT2 … HTX2 … HL01 … HL02) [| /2 width=1 by fqup_zeta/ ] -L0 -V0 -T0 -T2 #T2 #HT2 #HXT2 +/3 width=3 by cpm_zeta, ex2_intro/ qed-. fact cpr_conf_lpr_zeta_zeta (h): - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T1 → ∀X1. ⬆*[1] X1 ≘ T1 → - ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡[h] T2 → ∀X2. ⬆*[1] X2 ≘ T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡[h] T & ⦃G, L2⦄ ⊢ X2 ➡[h] T. -#h #G0 #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 -#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 -elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2 -elim (cpm_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1 -elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2 -lapply (lifts_inj … HT2 … HT1) -T #H destruct + ∀T1. ⬆*[1] T1 ≘ T0 → ∀X1. ⦃G0, L0⦄ ⊢ T1 ➡[h] X1 → + ∀T2. ⬆*[1] T2 ≘ T0 → ∀X2. ⦃G0, L0⦄ ⊢ T2 ➡[h] X2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ X1 ➡[h] T & ⦃G0, L2⦄ ⊢ X2 ➡[h] T. +#h #G0 #L0 #V0 #T0 #IH #T1 #HT10 #X1 #HTX1 +#T2 #HT20 #X2 #HTX2 #L1 #HL01 #L2 #HL02 +lapply (lifts_inj … HT20 … HT10) -HT20 #H destruct +elim (IH … HTX1 … HTX2 … HL01 … HL02) [| /2 width=1 by fqup_zeta/ ] -L0 -V0 -T0 -T1 #X #HX1 #HX2 /2 width=3 by ex2_intro/ qed-. fact cpr_conf_lpr_flat_flat (h): - ∀I,G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓕ{I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀I,G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓕ{I}V0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓕ{I}V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓕ{I}V2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓕ{I}V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓕ{I}V2.T2 ➡[h] T. #h #I #G0 #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // @@ -153,15 +138,12 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // qed-. fact cpr_conf_lpr_flat_eps (h): - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1,T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T. + ∀V1,T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓝV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T. #h #G0 #L0 #V0 #T0 #IH #V1 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 @@ -169,15 +151,12 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 qed-. fact cpr_conf_lpr_eps_eps (h): - ∀G,L0,V0,T0. ( - ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀G0,L0,V0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓝV0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀T1. ⦃G, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T. + ∀T1. ⦃G0, L0⦄ ⊢ T0 ➡[h] T1 → ∀T2. ⦃G0, L0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ T1 ➡[h] T & ⦃G0, L2⦄ ⊢ T2 ➡[h] T. #h #G0 #L0 #V0 #T0 #IH #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 @@ -185,16 +164,13 @@ elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 qed-. fact cpr_conf_lpr_flat_beta (h): - ∀p,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀p,G0,L0,V0,W0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓛ{p}W0.T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ ⓛ{p}W0.T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T. #h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cpm_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct @@ -210,44 +186,38 @@ qed-. pr0_cong_upsilon_cong pr0_cong_upsilon_delta *) fact cpr_conf_lpr_flat_theta (h): - ∀p,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀p,G0,L0,V0,W0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓓ{p}W0.T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 → - ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀T1. ⦃G0, L0⦄ ⊢ ⓓ{p}W0.T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 → + ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓐV1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T. #h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 -elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2 elim (cpm_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct + elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=2 by drops_refl, drops_drop/ ] #U #HVU #HU2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 /4 width=7 by cpm_bind, cpm_appl, cpm_theta, ex2_intro/ -| #T1 #HT01 #HXT1 #H destruct - elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 - elim (cpm_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -HXT1 /3 width=2 by drops_refl, drops_drop/ - /4 width=9 by cpm_appl, cpm_zeta, lifts_flat, ex2_intro/ +| #X0 #HXT0 #HX0 #H destruct + elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=2 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02 + elim (IH … HX0 … HX02 … HL01 … HL02) [| /3 width=5 by fqup_strap1, fqu_drop/ ] -L0 -V0 -W0 -T0 #T #H1T #H2T + /4 width=8 by cpm_appl, cpm_zeta, lifts_flat, ex2_intro/ ] qed-. fact cpr_conf_lpr_beta_beta (h): - ∀p,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀p,G0,L0,V0,W0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓐV0.ⓛ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀W1. ⦃G, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀W1. ⦃G0, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓛW0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[h] T. #h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01 #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 @@ -260,18 +230,15 @@ qed-. (* Basic_1: was: pr0_upsilon_upsilon *) fact cpr_conf_lpr_theta_theta (h): - ∀p,G,L0,V0,W0,T0. ( - ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → - ∀T1. ⦃G, L⦄ ⊢ T ➡[h] T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡[h] T2 → - ∀L1. ⦃G, L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L⦄ ⊢ ➡[h] L2 → - ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡[h] T0 & ⦃G, L2⦄ ⊢ T2 ➡[h] T0 + ∀p,G0,L0,V0,W0,T0. ( + ∀G,L,T. ⦃G0, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ → IH_cpr_conf_lpr h G L T ) → - ∀V1. ⦃G, L0⦄ ⊢ V0 ➡[h] V1 → ∀U1. ⬆*[1] V1 ≘ U1 → - ∀W1. ⦃G, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T1 → - ∀V2. ⦃G, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 → - ∀W2. ⦃G, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 → - ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 → - ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡[h] T & ⦃G, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T. + ∀V1. ⦃G0, L0⦄ ⊢ V0 ➡[h] V1 → ∀U1. ⬆*[1] V1 ≘ U1 → + ∀W1. ⦃G0, L0⦄ ⊢ W0 ➡[h] W1 → ∀T1. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T1 → + ∀V2. ⦃G0, L0⦄ ⊢ V0 ➡[h] V2 → ∀U2. ⬆*[1] V2 ≘ U2 → + ∀W2. ⦃G0, L0⦄ ⊢ W0 ➡[h] W2 → ∀T2. ⦃G0, L0.ⓓW0⦄ ⊢ T0 ➡[h] T2 → + ∀L1. ⦃G0, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G0, L0⦄ ⊢ ➡[h] L2 → + ∃∃T. ⦃G0, L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡[h] T & ⦃G0, L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[h] T. #h #p #G0 #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 @@ -289,28 +256,28 @@ theorem cpr_conf_lpr (h): ∀G. lex_confluent (λL.cpm h G L 0) (λL.cpm h G L 0 elim (cpr_inv_atom1_drops … H1) -H1 elim (cpr_inv_atom1_drops … H2) -H2 [ #H2 #H1 destruct - /2 width=1 by cpr_conf_lpr_atom_atom/ + @cpr_conf_lpr_atom_atom | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct - /3 width=10 by cpr_conf_lpr_atom_delta/ + @(cpr_conf_lpr_atom_delta … IH) -IH /width=6 by/ | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct - /4 width=10 by ex2_commute, cpr_conf_lpr_atom_delta/ + @ex2_commute @(cpr_conf_lpr_atom_delta … IH) -IH /width=6 by/ | * #X #Y #V2 #z #H #HV02 #HVT2 #H2 * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct - /3 width=17 by cpr_conf_lpr_delta_delta/ + @(cpr_conf_lpr_delta_delta … IH) -IH /width=6 by/ ] | #p #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpm_inv_bind1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 - | #T1 #HT01 #HXT1 #H11 #H12 + | #T1 #HT10 #HTX1 #H11 #H12 ] elim (cpm_inv_bind1 … H2) -H2 * [1,3: #V2 #T2 #HV02 #HT02 #H2 - |2,4: #T2 #HT02 #HXT2 #H21 #H22 + |2,4: #T2 #HT20 #HTX2 #H21 #H22 ] destruct - [ /3 width=10 by cpr_conf_lpr_bind_bind/ - | /4 width=11 by ex2_commute, cpr_conf_lpr_bind_zeta/ - | /3 width=11 by cpr_conf_lpr_bind_zeta/ - | /3 width=12 by cpr_conf_lpr_zeta_zeta/ + [ @(cpr_conf_lpr_bind_bind … IH) -IH /width=1 by/ + | @ex2_commute @(cpr_conf_lpr_bind_zeta … IH) -IH /width=3 by/ + | @(cpr_conf_lpr_bind_zeta … IH) -IH /width=3 by/ + | @(cpr_conf_lpr_zeta_zeta … IH) -IH /width=3 by/ ] | #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_flat1 … H1) -H1 * @@ -325,16 +292,16 @@ theorem cpr_conf_lpr (h): ∀G. lex_confluent (λL.cpm h G L 0) (λL.cpm h G L 0 |3,7,11,15: #p2 #V2 #Y2 #W2 #Z2 #T2 #HV02 #HYW2 #HZT2 #H21 #H22 #H23 |4,8,12,16: #p2 #V2 #U2 #Y2 #W2 #Z2 #T2 #HV02 #HVU2 #HYW2 #HZT2 #H21 #H22 #H23 ] destruct - [ /3 width=10 by cpr_conf_lpr_flat_flat/ - | /4 width=8 by ex2_commute, cpr_conf_lpr_flat_eps/ - | /4 width=12 by ex2_commute, cpr_conf_lpr_flat_beta/ - | /4 width=14 by ex2_commute, cpr_conf_lpr_flat_theta/ - | /3 width=8 by cpr_conf_lpr_flat_eps/ - | /3 width=7 by cpr_conf_lpr_eps_eps/ - | /3 width=12 by cpr_conf_lpr_flat_beta/ - | /3 width=13 by cpr_conf_lpr_beta_beta/ - | /3 width=14 by cpr_conf_lpr_flat_theta/ - | /3 width=17 by cpr_conf_lpr_theta_theta/ + [ @(cpr_conf_lpr_flat_flat … IH) -IH /width=1 by/ + | @ex2_commute @(cpr_conf_lpr_flat_eps … IH) -IH /width=1 by/ + | @ex2_commute @(cpr_conf_lpr_flat_beta … IH) -IH /width=1 by/ + | @ex2_commute @(cpr_conf_lpr_flat_theta … IH) -IH /width=3 by/ + | @(cpr_conf_lpr_flat_eps … IH) -IH /width=1 by/ + | @(cpr_conf_lpr_eps_eps … IH) -IH /width=1 by/ + | @(cpr_conf_lpr_flat_beta … IH) -IH /width=1 by/ + | @(cpr_conf_lpr_beta_beta … IH) -IH /width=1 by/ + | @(cpr_conf_lpr_flat_theta … IH) -IH /width=3 by/ + | @(cpr_conf_lpr_theta_theta … IH) -IH /width=3 by/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma index aaa4e94e7..85ff65ecc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_aaa.ma @@ -45,8 +45,9 @@ lemma cpx_aaa_conf_lpx (h): ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → | #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_abbr1 … H) -H * [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2 by lpx_pair, aaa_abbr/ - | #T2 #HT12 #HT2 #H destruct -IHV1 - /4 width=8 by lpx_pair, aaa_inv_lifts, drops_refl, drops_drop/ + | #X1 #HXT1 #HX1 #H destruct -IHV1 + elim (cpx_lifts_sn … HX1 (Ⓣ) … (L1.ⓓV1) … HXT1) -X1 + /4 width=7 by lpx_pair, aaa_inv_lifts, drops_refl, drops_drop/ ] | #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma new file mode 100644 index 000000000..ea4d62114 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_drops.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/static/rex_drops.ma". +include "basic_2/rt_transition/cpx_drops.ma". +include "basic_2/rt_transition/rpx.ma". + +(* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********) + +(* Properties with generic slicing for local environments *******************) + +lemma rpx_lifts_sn (h) (G): f_dedropable_sn (cpx h G). +/3 width=6 by rex_liftable_dedropable_sn, cpx_lifts_sn/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +lemma rpx_inv_lifts_sn (h) (G): f_dropable_sn (cpx h G). +/2 width=5 by rex_dropable_sn/ qed-. + +lemma rpx_inv_lifts_dx (h) (G): f_dropable_dx (cpx h G). +/2 width=5 by rex_dropable_dx/ qed-. + +lemma rpx_inv_lifts_bi (h) (G): + ∀L1,L2,U. ⦃G,L1⦄ ⊢ ⬈[h,U] L2 → ∀b,f. 𝐔⦃f⦄ → + ∀K1,K2. ⬇*[b,f] L1 ≘ K1 → ⬇*[b,f] L2 ≘ K2 → + ∀T. ⬆*[f]T ≘ U → ⦃G,K1⦄ ⊢ ⬈[h,T] K2. +/2 width=10 by rex_inv_lifts_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma index d26a5d557..fd4ddc459 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma @@ -15,6 +15,7 @@ include "static_2/static/fsle_drops.ma". include "static_2/static/rex_fsle.ma". include "basic_2/rt_transition/rpx_length.ma". +include "basic_2/rt_transition/rpx_drops.ma". include "basic_2/rt_transition/rpx_fqup.ma". (* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********) @@ -72,9 +73,10 @@ lemma rpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → [ #V1 #T1 #HV01 #HT01 #H destruct lapply (rpx_fwd_length … HV0) #H0 /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/ - | #T #HT #HXT #H1 #H2 destruct + | #T #H2T0 #HTX #H1 #H2 destruct + lapply (rpx_inv_lifts_bi … HT0 (Ⓣ) … H2T0) -HT0 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT lapply (rpx_fwd_length … HV0) #H0 - /3 width=8 by fsle_inv_lifts_sn/ + /5 width=6 by fsle_bind_dx_dx, fsle_lifts_dx, fqup_zeta/ ] | #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct elim (rex_inv_flat … HY) -HY #HV0 #HX0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma index 42478e2b6..b43cbfd04 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_rdeq.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "static_2/static/rdeq_drops.ma". include "static_2/static/rdeq_fqup.ma". include "static_2/static/rdeq_rdeq.ma". include "basic_2/rt_transition/rpx_fsle.ma". @@ -75,13 +76,14 @@ lemma cpx_tdeq_conf_sex: ∀h,o,G. R_confluent2_rex … (cpx h G) (cdeq h o) (cp elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02 elim (IHT … HT02 … H1 … H2) -L0 -V0 -T0 /3 width=5 by cpx_flat, tdeq_pair, ex2_intro/ -| #G #L0 #V0 #T0 #T1 #U1 #_ #IH #HUT1 #X0 #H0 #L1 #H1 #L2 #H2 - elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct +| #G #L0 #V0 #U0 #T0 #T1 #HTU0 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2 + elim (tdeq_inv_pair1 … H0) -H0 #V2 #U2 #HV02 #HU02 #H destruct elim (rpx_inv_bind … H1) -H1 #HL01 #H1 elim (rdeq_inv_bind … H2) -H2 #HL02 #H2 - lapply (rdeq_bind_repl_dx … H2 (BPair Abbr V2) ?) -H2 /2 width=1 by ext2_pair/ -HV02 #H2 + lapply (rpx_inv_lifts_bi … H1 (Ⓣ) … HTU0) -H1 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H1 + lapply (rdeq_inv_lifts_bi … H2 (Ⓣ) … HTU0) -H2 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #H2 + elim (tdeq_inv_lifts_sn … HU02 … HTU0) -U0 #T2 #HTU2 #HT02 elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1 - elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1 /3 width=5 by cpx_zeta, ex2_intro/ | #G #L0 #V0 #T0 #T1 #_ #IH #X0 #H0 #L1 #H1 #L2 #H2 elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #_ #HT02 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index c58de1441..65ad7dd16 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -96,12 +96,12 @@ table { } ] [ { "t-bound context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] + [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_tdeq" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_aaa" + "cpm_cpx" * ] } ] [ { "unbound context-sensitive parallel rt-transition" * } { [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ] + [ [ "for lenvs on referred entries" ] "rpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "rpx_length" + "rpx_drops" + "rpx_fqup" + "rpx_fsle" + "rpx_rdeq" + "rpx_lpx" + "rpx_rpx" * ] [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" "lpx_length" + "lpx_drops" + "lpx_fquq" + "lpx_fsle" + "lpx_rdeq" + "lpx_aaa" * ] [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_req" + "cpx_rdeq" + "cpx_fdeq" * ] diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma index 41c641716..0581f6d1c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_lifts.ma @@ -86,6 +86,11 @@ theorem lifts_trans: ∀f1,T1,T. ⬆*[f1] T1 ≘ T → ∀f2,T2. ⬆*[f2] T ≘ ] qed-. +lemma lifts_trans4_one (f) (T1) (T2): + ∀T. ⬆*[1]T1 ≘ T → ⬆*[⫯f]T ≘ T2 → + ∃∃T0. ⬆*[f]T1 ≘ T0 & ⬆*[1]T0 ≘ T2. +/4 width=6 by lifts_trans, lifts_split_trans, after_uni_one_dx/ qed-. + (* Basic_2A1: includes: lift_conf_O1 lift_conf_be *) theorem lifts_conf: ∀f1,T,T1. ⬆*[f1] T ≘ T1 → ∀f,T2. ⬆*[f] T ≘ T2 → ∀f2. f2 ⊚ f1 ≘ f → ⬆*[f2] T1 ≘ T2. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma index 0b0dbf92f..fb5d8247f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_tdeq.ma @@ -64,3 +64,21 @@ qed-. lemma tdeq_inv_lifts_bi: ∀h,o. deliftable2_bi (tdeq h o). /3 width=6 by tdeq_inv_lifts_sn, deliftable2_sn_bi/ qed-. + +lemma tdeq_lifts_inv_pair_sn (h) (o) (I) (f:rtmap): + ∀X,T. ⬆*[f]X ≘ T → ∀V. ②{I}V.T ≛[h,o] X → ⊥. +#h #o #I #f #X #T #H elim H -f -X -T +[ #f #s #V #H + elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct +| #f #i #j #_ #V #H + elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct +| #f #l #V #H + elim (tdeq_inv_pair1 … H) -H #X1 #X2 #_ #_ #H destruct +| #f #p #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H + elim (tdeq_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct + /2 width=2 by/ +| #f #J #X1 #T1 #X2 #T2 #_ #_ #_ #IH2 #V #H + elim (tdeq_inv_pair1 … H) -H #Z1 #Z2 #_ #HZ2 #H destruct + /2 width=2 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma index 51c5afc6a..e3dae5bf4 100644 --- a/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma +++ b/matita/matita/contribs/lambdadelta/static_2/s_computation/fqup.ma @@ -83,4 +83,10 @@ lemma fqup_ind_dx: ∀b,G2,L2,T2. ∀Q:relation3 …. @(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) qed-. +(* Advanced properties ******************************************************) + +lemma fqup_zeta (b) (p) (I) (G) (K) (V): + ∀T1,T2. ⬆*[1]T2 ≘ T1 → ⦃G,K,ⓑ{p,I}V.T1⦄ ⊐+[b] ⦃G,K,T2⦄. +/4 width=5 by fqup_strap2, fqu_fqup, fqu_drop/ qed. + (* Basic_2A1: removed theorems 1: fqup_drop *) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma index 8375d521a..542d8b10e 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma @@ -29,6 +29,17 @@ lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf) @(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *) qed-. +lemma fsle_lifts_dx (L1) (L2): + |L1| ≤ |L2| → ∀T2,U2. ⬆*[1]T2 ≘ U2 → + ∀T1. ⦃L1,T1⦄ ⊆ ⦃L2,T2⦄ → ⦃L1,T1⦄ ⊆ ⦃L2.ⓧ,U2⦄. +#L1 #L2 #HL21 #T2 #U2 #HTU2 #T1 +* #n #m #f #g #Hf #Hg #H2L #Hfg +lapply (lveq_length_fwd_sn … H2L ?) // -HL21 #H destruct +lapply (frees_lifts_SO (Ⓣ) (L2.ⓧ) … HTU2 … Hg) +[ /3 width=4 by drops_refl, drops_drop/ ] -T2 #Hg +@(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_dx/ (**) (* explict constructor *) +qed-. + lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ → ∀W1. ⬆*[1] V1 ≘ W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄. #K1 #K2 #HK #V1 #V2 diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma index 6b9537f61..3a4448079 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/rdeq_drops.ma @@ -28,11 +28,9 @@ lemma rdeq_lifts_sn: ∀h,o. f_dedropable_sn (cdeq h o). lemma rdeq_inv_lifts_sn: ∀h,o. f_dropable_sn (cdeq h o). /2 width=5 by rex_dropable_sn/ qed-. -(* Note: missing in basic_2A1 *) lemma rdeq_inv_lifts_dx: ∀h,o. f_dropable_dx (cdeq h o). /2 width=5 by rex_dropable_dx/ qed-. -(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) lemma rdeq_inv_lifts_bi: ∀h,o,L1,L2,U. L1 ≛[h, o, U] L2 → ∀b,f. 𝐔⦃f⦄ → ∀K1,K2. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → ∀T. ⬆*[f] T ≘ U → K1 ≛[h, o, T] K2. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/req_drops.ma new file mode 100644 index 000000000..0eae38683 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/req_drops.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/static/rex_drops.ma". +include "static_2/static/req.ma". + +(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) + +(* Note: req_inv_lifts_dx missing in basic_2A1 *) + +(* Basic_2A1: uses: lleq_inv_lift_le lleq_inv_lift_be lleq_inv_lift_ge *) +lemma req_inv_lifts_bi: ∀L1,L2,U. L1 ≡[U] L2 → ∀b,f. 𝐔⦃f⦄ → + ∀K1,K2. ⬇*[b, f] L1 ≘ K1 → ⬇*[b, f] L2 ≘ K2 → + ∀T. ⬆*[f] T ≘ U → K1 ≡[T] K2. +/2 width=10 by rex_inv_lifts_bi/ qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 6a7a09101..4dcb17989 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -36,7 +36,7 @@ table { } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_fqup" + "req_fsle" * ] + [ [ "for lenvs on referred entries" ] "req" + "( ? ≡[?] ? )" "req_drops" + "req_fqup" + "req_fsle" * ] } ] [ { "generic extension of a context-sensitive relation" * } {