X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpm.ma;h=341ecee8cfde5b23e00b615b04c4d3ef40673cc7;hp=31dad2da9f9b8bc9daa951985bd94787d4ec0bd1;hb=5c92c318030a05c766b3f6070dbd23589cbdee04;hpb=8f5533bd34e93eee2a14cdcfd0595be65651bfa7 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 31dad2da9..341ecee8c 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. @@ -118,6 +119,14 @@ qed. lemma cpr_refl: ∀h,G,L. reflexive … (cpm h G L 0). /3 width=3 by cpg_refl, ex2_intro/ qed. +(* Advanced properties ******************************************************) + +lemma cpm_sort (h) (G) (L): + ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ➡[n,h] ⋆((next h)^n s). +#h #G #L * // +#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/ +qed. + (* Basic inversion lemmas ***************************************************) lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → @@ -125,8 +134,8 @@ lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → | ∃∃s. T2 = ⋆(next h s) & J = Sort s & n = 1 | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 - | ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≘ T2 & - L = K.ⓛV1 & J = LRef 0 & n = ↑k + | ∃∃m,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[m, h] V2 & ⬆*[1] V2 ≘ T2 & + L = K.ⓛV1 & J = LRef 0 & n = ↑m | ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I} & J = LRef (↑i). #n #h #J #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1 … H) -H * @@ -135,7 +144,7 @@ lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/ | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct - elim (isrt_inv_plus_SO_dx … Hc) -Hc // #k #Hc #H destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/ | #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/ @@ -143,25 +152,25 @@ 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 → ∨∨ T2 = #0 ∧ n = 0 | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓓV1 - | ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≘ T2 & - L = K.ⓛV1 & n = ↑k. + | ∃∃m,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[m, h] V2 & ⬆*[1] V2 ≘ T2 & + L = K.ⓛV1 & n = ↑m. #n #h #G #L #T2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H * [ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/ | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/ | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct - elim (isrt_inv_plus_SO_dx … Hc) -Hc // #k #Hc #H destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/ ] qed-. @@ -185,15 +194,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 +211,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 +224,18 @@ 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-. + +lemma cpm_inv_abst_bi: ∀n,h,p1,p2,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ ⓛ{p1}V1.T1 ➡[n,h] ⓛ{p2}V2.T2 → + ∧∧ ⦃G,L⦄ ⊢ V1 ➡[h] V2 & ⦃G,L.ⓛV1⦄ ⊢ T1 ➡[n,h] T2 & p1 = p2. +#n #h #p1 #p2 #G #L #V1 #V2 #T1 #T2 #H +elim (cpm_inv_abst1 … H) -H #XV #XT #HV #HT #H destruct +/2 width=1 by and3_intro/ qed-. (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *) @@ -262,7 +275,7 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 & U2 = ⓝV2.T2 | ⦃G, L⦄ ⊢ U1 ➡[n, h] U2 - | ∃∃k. ⦃G, L⦄ ⊢ V1 ➡[k, h] U2 & n = ↑k. + | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ↑m. #n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct @@ -272,7 +285,7 @@ lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 | #cU #U12 #H destruct /4 width=3 by isrt_inv_plus_O_dx, or3_intro1, ex2_intro/ | #cU #H12 #H destruct - elim (isrt_inv_plus_SO_dx … Hc) -Hc // #k #Hc #H destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct /4 width=3 by or3_intro2, ex2_intro/ ] qed-. @@ -289,53 +302,36 @@ qed-. (* Basic eliminators ********************************************************) -lemma isrt_inv_max_shift_sn: ∀n,c1,c2. 𝐑𝐓⦃n, ↕*c1 ∨ c2⦄ → - ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃n, c2⦄. -#n #c1 #c2 #H -elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct -elim (isrt_inv_shift … Hc1) -Hc1 #Hc1 * -n1 -/2 width=1 by conj/ -qed-. - -lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → eq_t c1 c2 → - ∧∧ 𝐑𝐓⦃n, c1⦄ & 𝐑𝐓⦃n, c2⦄. -#n #c1 #c2 #H #Hc12 -elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct -lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H -<(isrt_inj … H … Hc2) -Hc2 -