From f38fd769279794d0ca73c8945eac30e8b42e59be Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 3 Oct 2019 17:14:08 +0200 Subject: [PATCH] update in ground_2 and basic_2 + rules for cpt justified + cpt is an instance of cpm --- .../lambdadelta/basic_2/etc/cpt/cpt.etc | 54 +++++++++ .../lambdadelta/basic_2/etc/cpt/cpt_cpm.etc | 108 ++++++++++++++++++ .../lambdadelta/basic_2/etc/cpt/cpt_cpt.etc | 62 ++++++++++ .../lambdadelta/basic_2/rt_transition/cpt.ma | 76 ++++++++++-- .../basic_2/rt_transition/cpt_cpm.ma | 53 ++------- .../basic_2/rt_transition/cpt_fqu.ma | 63 ++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../lambdadelta/ground_2/steps/rtc_ist.ma | 4 + .../ground_2/steps/rtc_ist_plus.ma | 6 + 9 files changed, 374 insertions(+), 54 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpm.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt_fqu.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt.etc new file mode 100644 index 000000000..e9e1cd8e9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt.etc @@ -0,0 +1,54 @@ +(* Advanced inversion lemmas ************************************************) + +lemma cpt_inv_sort_sn (h) (n) (G) (L) (s): + ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 → + ∨∨ ∧∧ X2 = ⋆s & n = 0 + | ∧∧ X2 = ⋆(⫯[h]s) & n =1. +#h #n #G #L #s #X2 * #c #Hc #H +elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct +/3 width=1 by or_introl, or_intror, conj/ +qed-. + +lemma cpt_inv_zero_sn (h) (n) (G) (L): + ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 → + ∨∨ ∧∧ X2 = #0 & n = 0 + | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1 + | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m. +#h #n #G #L #X2 * #c #Hc #H +elim (cpg_inv_zero1 … H) -H * +[ #H1 #H2 destruct /3 width=1 by 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 (ist_inv_plus_SO_dx … H2) -H2 [| // ] #m #Hc #H destruct + /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/ +] +qed-. + +lemma cpt_inv_lref_sn (h) (n) (G) (L) (i): + ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 → + ∨∨ ∧∧ X2 = #(↑i) & n = 0 + | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}. +#h #n #G #L #i #X2 * #c #Hc #H +elim (cpg_inv_lref1 … H) -H * +[ #H1 #H2 destruct /3 width=1 by or_introl, conj/ +| #I #K #V2 #HV2 #HVT2 #H destruct + /4 width=6 by ex3_3_intro, ex2_intro, or_intror/ +] +qed-. + +lemma cpt_inv_gref_sn (h) (n) (G) (L) (l): + ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0. +#h #n #G #L #l #X2 * #c #Hc #H +elim (cpg_inv_gref1 … H) -H #H1 #H2 destruct +/2 width=1 by conj/ +qed-. + + +lemma cpt_inv_sort_sn_iter (h) (n) (G) (L) (s): + ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 → + ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1. +#h #n #G #L #s #X2 #H +elim (cpt_inv_sort_sn … H) -H * #H1 #H2 destruct +/2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpm.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpm.etc new file mode 100644 index 000000000..ccb459081 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpm.etc @@ -0,0 +1,108 @@ +(* Properties with t-bound rt-transition for terms **************************) + +axiom cpt_total (h) (n) (G) (L) (T): + ∃U. ⦃G,L⦄ ⊢ T ⬆[h,n] U. + +lemma pippo (h) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 → ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 → + ∃∃T. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T & ⦃G,L⦄ ⊢ T ➡[h] T2. +#h #G #L #T0 #T1 #H +@(cpr_ind … H) -G -L -T0 -T1 +[ #I #G #L #n #T2 #HT2 + /2 width=3 by ex2_intro/ +| #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2 + elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0 + [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02 + elim (IH … HV02) -V0 #V0 #HV10 #HV02 +| +| +| +| +| +| #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX + elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct + elim (cpt_inv_cast_sn … HX) -HX * + [ #W2 #V2 #HW02 #HV02 #H destruct + elim (cpt_total h n G (L.ⓛW1) T0) #T3 #HT03 + elim (IHV … HV02) -V0 #V0 #HV10 #HV02 + elim (IHW … HW02) -W0 #W0 #HW10 #HW02 + elim (IHT … HT02) -T0 #T0 #HT10 #HT02 + @(ex2_intro … (ⓐV0.ⓛ{p}W0.T0)) + [ /3 width=1 by cpt_appl, cpt_bind/ + | @(cpm_beta … HV02 HW02) + + | #m #_ #H destruct + ] + +lemma cpm_cpt_cpr (h) (n) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 & ⦃G,L⦄ ⊢ T0 ➡[h] T2. +#h #n #G #L #T1 #T2 #H +@(cpm_ind … H) -n -G -L -T1 -T2 +[ #I #G #L /2 width=3 by ex2_intro/ +| #G #L #s /3 width=3 by cpm_sort, ex2_intro/ +| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2 + elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0 + lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVW0 … HVW2) -HVW2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02 + /3 width=3 by cpt_delta, ex2_intro/ +| #n #G #K #V1 #V2 #W2 #_ * #V0 #HV10 #HV02 #HVW2 + elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0 + lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓛV1) … HVW0 … HVW2) -HVW2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HV02 #HW02 + /3 width=3 by cpt_ell, ex2_intro/ +| #n #I #G #K #T2 #U2 #i #_ * #T0 #HT0 #HT02 #HTU2 + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -HTU2 + [ /3 width=1 by drops_refl, drops_drop/ ] -HT02 #HU02 + /3 width=3 by cpt_lref, ex2_intro/ +| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02 + /3 width=5 by cpt_bind, cpm_bind, ex2_intro/ +| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ * #T0 #HT10 #HT02 + /3 width=5 by cpt_appl, cpm_appl, ex2_intro/ +| #n #G #L #V1 #V2 #T1 #T2 #_ #_ * #V0 #HV10 #HV02 * #T0 #HT10 #HT02 + /3 width=5 by cpt_cast, cpm_cast, ex2_intro/ +| #n #G #L #V #U1 #T1 #T2 #HTU1 #_ * #T0 #HT10 #HT02 + elim (cpt_lifts_sn … HT10 (Ⓣ) … (L.ⓓV) … HTU1) -T1 + [| /3 width=1 by drops_refl, drops_drop/ ] #U0 #HTU0 #HU10 + /3 width=6 by cpt_bind, cpm_zeta, ex2_intro/ +| #n #G #L #U #T1 #T2 #_ * #T0 #HT10 #HT02 +| #n #G #L #U1 #U2 #T #_ * #U0 #HU10 #HU02 + /3 width=3 by cpt_ee, ex2_intro/ +| #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 + /4 width=7 by cpt_appl, cpt_bind, cpm_beta, ex2_intro/ +| #n #p #G #L #V1 #V2 #V0 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ * #T0 #HT10 #HT02 #HV20 + /4 width=9 by cpt_appl, cpt_bind, cpm_theta, ex2_intro/ +] + +(* Forward lemmas with t-bound rt-transition for terms **********************) + +lemma pippo (h) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T1 ➡[h] T0 → + ∀n,T2. ⦃G,L⦄ ⊢ T0 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ T1 ➡[n,h] T2. +#h #G #L #T0 #T1 #H +@(cpr_ind … H) -G -L -T0 -T1 +[ #I #G #L #n #T2 #HT2 + /2 width=1 by cpt_fwd_cpm/ +| #G #K #V1 #V0 #W0 #_ #IH #HVW0 #n #T2 #HT2 + elim (cpt_inv_lifts_sn … HT2 (Ⓣ) … K … HVW0) -W0 + [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV02 + lapply (IH … HV02) -V0 #HV12 + /2 width=3 by cpm_delta/ +| +| +| +| +| +| #p #G #L #V1 #V0 #W1 #W0 #T1 #T0 #_ #_ #_ #IHV #IHW #IHT #n #X #HX + elim (cpt_inv_bind_sn … HX) -HX #X0 #T2 #HX #HT02 #H destruct + elim (cpt_inv_cast_sn … HX) -HX * + [ #W2 #V2 #HW02 #HV02 #H destruct + elim (cpt_total h n G (L.ⓛW1) T0) #T2 #HT02 + lapply (IHV … HV02) -V0 #HV12 + lapply (IHW … HW02) -W0 #HW12 + lapply (IHT … HT02) -T0 #HT12 + @(cpm_beta … HV12 HW12) // + + | #m #_ #H destruct + ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpt.etc new file mode 100644 index 000000000..ae5bb2bb5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpt.etc @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cpt_drops.ma". +include "basic_2/rt_transition/cpt_fqu.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************) + +(* Main properties **********************************************************) + +theorem cpt_n_O_trans (h) (n) (G) (L) (T0): + ∀T1. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 → + ∀T2. ⦃G,L⦄ ⊢ T0 ⬆[h,0] T2 → ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2. +#h #n #G #L #T0 #T1 #H +@(cpt_ind … H) -H +[ #I #G #L #X2 #HX2 // +| #G #L #s #X2 #HX2 + elim (cpt_inv_sort_sn_iter … HX2) -HX2 #H #_ destruct // +| #n #G #K #V1 #V0 #W0 #_ #IH #HVW0 #W2 #HW02 + elim (cpt_inv_lifts_sn … HW02 (Ⓣ) … K … HVW0) -W0 + [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVW2 #HV02 + /3 width=3 by cpt_delta/ +| #n #G #K #W1 #W0 #V0 #_ #IH #HWV0 #V2 #HV02 + elim (cpt_inv_lifts_sn … HV02 (Ⓣ) … K … HWV0) -V0 + [| /3 width=1 by drops_refl, drops_drop/ ] #W2 #HWV2 #HW02 + /3 width=3 by cpt_ell/ +| #n #I #G #K #T0 #U0 #i #_ #IH #HTU0 #U2 #HU02 + elim (cpt_inv_lifts_sn … HU02 (Ⓣ) … K … HTU0) -U0 + [| /3 width=1 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT02 + /3 width=3 by cpt_lref/ +| #n #p #I #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2 + elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct + @cpt_bind + [ /2 width=1 by/ + | @IHT + ] +| #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2 + elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct + /3 width=1 by cpt_appl/ +| #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2 + elim (cpt_inv_cast_sn … HX2) -HX2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpt_cast/ + | #m #_ #H destruct + ] +| #n #G #L #V1 #V0 #T1 #_ #IH #V2 #HV02 + /3 width=1 by cpt_ee/ +] + + + + \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma index 0ccb505e6..229c32a96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma @@ -86,10 +86,72 @@ qed. lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0). /3 width=3 by cpg_refl, ex2_intro/ qed. -(* Advanced properties ******************************************************) - -lemma cpt_sort (h) (G) (L): - ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((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 cpt_inv_atom_sn (h) (n) (J) (G) (L): + ∀X2. ⦃G,L⦄ ⊢ ⓪{J} ⬆[h,n] X2 → + ∨∨ ∧∧ X2 = ⓪{J} & n = 0 + | ∃∃s. X2 = ⋆(⫯[h]s) & J = Sort s & n =1 + | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1 & J = LRef 0 + | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & J = LRef 0 & n = ↑m + | ∃∃I,K,T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I} & J = LRef (↑i). +#h #n #J #G #L #X2 * #c #Hc #H +elim (cpg_inv_atom1 … H) -H * +[ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/ +| #s #H1 #H2 #H3 destruct /3 width=3 by or5_intro1, ex3_intro/ +| #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 (ist_inv_plus_SO_dx … H3) -H3 [| // ] #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/ +] +qed-. + +lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1): + ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 → + ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 + & X2 = ⓑ{p,I}V2.T2. +#h #n #p #I #G #L #V1 #T1 #X2 * #c #Hc #H +elim (cpg_inv_bind1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct + elim (ist_inv_shift … HcV) -HcV #HcV #H destruct + /3 width=5 by ex3_2_intro, ex2_intro/ +| #cT #T2 #_ #_ #_ #_ #H destruct + elim (ist_inv_plus_10_dx … H) +] +qed-. + +lemma cpt_inv_appl_sn (h) (n) (G) (L) (V1) (T1): + ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] X2 → + ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓐV2.T2. +#h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct + elim (ist_inv_shift … HcV) -HcV #HcV #H destruct + /3 width=5 by ex3_2_intro, ex2_intro/ +| #cV #cW #cU #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #H destruct + elim (ist_inv_plus_10_dx … H) +| #cV #cW #cU #p #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #_ #H destruct + elim (ist_inv_plus_10_dx … H) +] +qed-. + +lemma cpt_inv_cast_sn (h) (n) (G) (L) (V1) (T1): + ∀X2. ⦃G,L⦄ ⊢ ⓝV1.T1 ⬆[h,n] X2 → + ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓝV2.T2 + | ∃∃m. ⦃G,L⦄ ⊢ V1 ⬆[h,m] X2 & n = ↑m. +#h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct + elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct +