From: Ferruccio Guidi Date: Sat, 27 Oct 2018 16:53:07 +0000 (+0200) Subject: update in basic_2 X-Git-Tag: make_still_working~273 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=de3a41b9a4e51dc1b09adce800273adf5ffa1215 update in basic_2 the restricted type rules are justified --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma new file mode 100644 index 000000000..cdcb23adf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma @@ -0,0 +1,160 @@ + +include "basic_2/rt_computation/cpms_lpr.ma". +(* +lemma cpm_lsubr_trans (h) (n) (G) (L1) (T1): + ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[↑n,h] T2 → ∀L2. L1 ⫃ L2 → + ∃∃T0. ⦃G,L2⦄ ⊢ T1 ➡[↑n,h] T0 & ⦃G,L2⦄ ⊢ T0 ➡*[h] T2. +#h #m #G #L1 #T1 #T2 +@(insert_eq_0 … (↑m)) #n #H +@(cpm_ind … H) -n -G -L1 -T1 -T2 +[ +| +| #n #G #K1 #V1 #V2 #W2 #_ #IH #HVW2 #Hm #L2 #H destruct + elim (lsubr_inv_bind1 … H) -H * + [ #K2 #HK #H destruct + elim (IH … HK) -K1 [| // ] #V0 #HV10 #HV02 + elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0 + lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K2.ⓓV1) … HVW0 … HVW2) -V2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HW02 + /3 width=3 by cpm_delta, ex2_intro/ + | #K2 #VX #WX #HK #H1 #H2 destruct + elim (IH … HK) -K1 [| // ] #X0 #H1 #H2 + elim (cpm_inv_cast1 … H1) -H1 [ * || * ] + [ #W0 #V0 #HW0 #HV0 #H destruct + @(ex2_intro … (#0)) [ // | + | #I1 #I2 #K2 #VX #HK #H1 #H2 destruct + +| +| +| #n #p #I #G #L1 #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #L2 #HL + elim (IHV … HL) -IHV #V0 #HV01 #HV02 + elim (IHT (L2.ⓑ{I}V1)) [| /2 width=1 by lsubr_bind/ ] -L1 #T0 #HT10 #HT02 + @(ex2_intro … (ⓑ{p,I}V1.T0)) /3 width=3 by cprs_step_sn, cpms_bind, cpm_bind/ (**) (* full auto a bit slow *) +| +| +| // +*) +(* +lemma cpr_cpm_trans_swap_lsubr_lpr (h) (G) (L1) (T1): + ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L. L ⫃ L1 → + ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 → + ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[h] T2. +#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1 +#G0 #L0 #T0 #IH #G #L1 * [| * [| * ]] +[ (* + #I #HG #HL #HT #X #H1 #L2 #HL12 #m2 #X2 #H2 destruct + elim (cpr_inv_atom1 … H1) -H1 [|*: * ] + [ #H destruct + elim (cpm_inv_atom1 … H2) -H2 * + [ #H1 #H2 destruct /3 width=3 by cpm_cpms, ex2_intro/ + | #s #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ + | #K2 #V #V2 #HV2 #HVT2 #H1 #H2 destruct + elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #V1 #HK12 #HV1 #H destruct + elim (IH … HV1 … HK12 … HV2) -K2 -V -IH + [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02 + elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0 + lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HT02 + /3 width=3 by cpm_delta, ex2_intro/ + | #n2 #K2 #W #W2 #HW2 #HWT2 #H1 #H2 #H3 destruct + elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #W1 #HK12 #HW1 #H destruct + elim (IH … HW1 … HK12 … HW2) -K2 -W -IH + [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #W0 #HW10 #HW02 + elim (lifts_total W0 (𝐔❴1❵)) #T0 #HWT0 + lapply (cpms_lifts_bi … HW02 (Ⓣ) … (K1.ⓛW1) … HWT0 … HWT2) -W2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HT02 + /3 width=3 by cpm_ell, ex2_intro/ + | #I2 #K2 #T2 #i #HT2 #HTU2 #H1 #H2 destruct + elim (lpr_inv_bind_dx … HL12) -HL12 #I1 #K1 #HK12 #_ #H destruct + elim (IH … (#i) … HK12 … HT2) -I2 -K2 -IH + [|*: /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02 + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HU02 + /3 width=3 by cpm_lref, ex2_intro/ + ] + | #K1 #V1 #V #HV1 #HVT #H1 #H2 destruct + elim (lpr_inv_pair_sn … HL12) -HL12 #K2 #V0 #HK12 #_ #H destruct + elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HVT) -X + [|*: /3 width=2 by drops_refl, drops_drop/ ] -V0 #V2 #HVT2 #HV2 + elim (IH … HV1 … HK12 … HV2) -K2 -V -IH + [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02 + elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0 + lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HT02 + /3 width=3 by cpm_delta, ex2_intro/ + | #I1 #K1 #T #i #HT1 #HTU #H1 #H2 destruct + elim (lpr_inv_bind_sn … HL12) -HL12 #I2 #K2 #HK12 #_ #H destruct + elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HTU) -X + [|*: /3 width=2 by drops_refl, drops_drop/ ] -I2 #T2 #HTU2 #HT2 + elim (IH … HT1 … HK12 … HT2) -K2 -T -IH + [| /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02 + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2 + [ /3 width=2 by drops_refl, drops_drop/ ] #HU02 + /3 width=3 by cpm_lref, ex2_intro/ + ] +*) +| (* + #p #I #V1 #T1 #HG #HL #HT #X #H1 #L2 #HL12 #n2 #X2 #H2 + elim (cpm_inv_bind1 … H1) -H1 * + [ #V #T #HV1 #HT1 #H destruct + elim (cpm_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct + elim (IH … HT1 … HT2) -T + [|*: /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02 + elim (IH … HV1 … HL12 … HV2) -L2 -V -IH + [| // ] #V0 #HV10 #HV02 + /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/ + | #X #HXT #HX2 #H1 #H2 destruct + elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2 + [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2 + elim (IH … HT1 … HT2) -HT2 -IH + [|*: /2 width=1 by lpr_pair/ ] -L2 #T0 #HT10 #HT02 + /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/ + ] + | #X1 #HXT1 #HX1 #H1 #H2 destruct + elim (IH … HX1 … HL12 … H2) -L2 -X -IH + [| /2 width=1 by fqup_zeta/ ] #X0 #HX10 #HX02 + /3 width=3 by cpm_zeta, ex2_intro/ + ] +*) +| #V1 #T1 #HG #HL #HT #X #H1 #L #HL1 #L2 #HL2 #m2 #X2 #H2 destruct + elim (cpm_inv_appl1 … H1) -H1 * + [ (* + #V #T #HV1 #HT1 #H destruct + elim (cpm_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV2 #HT2 #H destruct + elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02 + elim (IH … HT1 … HL12 … HT2) -L2 -T -IH [| // ] #T0 #HT10 #HT02 + /3 width=5 by cpms_appl, cpm_appl, ex2_intro/ + | #q #V2 #WX #W2 #TX #T2 #HV2 #HW2 #HT2 #H1 #H2 destruct + elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02 + elim (IH … HT1 … HL12 m2 (ⓛ{q}W2.T2)) -IH -HT1 + [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02 + /4 width=9 by cprs_step_dx, cpms_appl, cpm_beta, cpm_appl, ex2_intro/ + | #q #V2 #U2 #WX #W2 #TX #T2 #HV2 #HVU2 #HW2 #HT2 #H1 #H2 destruct + elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02 + elim (IH … HT1 … HL12 m2 (ⓓ{q}W2.T2)) -IH -HT1 + [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02 + /4 width=11 by cprs_step_dx, cpms_appl, cpm_theta, cpm_appl, ex2_intro/ + ] + *) + | #p #V #W1 #W #TX1 #T #HV1 #HW1 #HT1 #H1 #H3 destruct + elim (cpm_inv_abbr1 … H2) -H2 * + [ #X3 #T2 #H2 #HT2 #H destruct + elim (cpr_inv_cast1 … H2) -H2 [ * ] + [ #W2 #V2 #HW2 #HV2 #H destruct + elim (IH … HT1 (L.ⓓⓝW1.V1) … HT2) -T + [|*: /4 width=3 by lsubr_beta, lpr_pair, cpm_cast, lsubr_cpm_trans/ ] #T0 #HT10 #HT02 + elim (IH … HV1 … HL1 … HL2 … HV2) -V [| // ] #V0 #HV10 #HV02 + elim (IH … HW1 … HL1 … HL2 … HW2) -L2 -W -IH [| // ] #W0 #HW10 #HW02 + @(ex2_intro … (ⓓ{p}ⓝW1.V1.T0)) + [ @cpm_beta // + + /2 width=1 by cpm_beta/ + | /3 width=7 by cprs_step_dx, cpms_appl, cpm_beta/ + + @cprs_step_dx [| @(cpms_appl … HT02 … HV02) | /2 width=1 by cpm_beta/ + @cpms_beta +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt index f4fa2049e..833421329 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/notes.txt @@ -1,10 +1,11 @@ D I sort * * -lref ldef * -lref ldec * -lref lref * -lref ldef drops * -lref ldec drops * +lref ldef * * +lref ldec * * +lref lref * * +lref ldef drops * * +lref ldec drops * * +gref * bind * * appl appl * * appl beta * diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma index 194211191..5b83675b3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -66,6 +66,15 @@ elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12 /3 width=3 by cnv_cast, cpms_eps/ qed. +(* Basic inversion lemmas ***************************************************) + +lemma nta_inv_gref_sn (a) (h) (G) (L): + ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥. +#a #h #G #L #X2 #l #H +elim (cnv_inv_cast … H) -H #X #_ #H #_ #_ +elim (cnv_inv_gref … H) +qed-. + (* Basic_forward lemmas *****************************************************) lemma nta_fwd_cnv_sn (a) (h) (G) (L): diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma index 0dd3441f2..100d6317b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma @@ -44,9 +44,26 @@ qed-. (* Basic_1: was: ty3_gen_sort *) (* Basic_2A1: was: nta_inv_sort1 *) lemma nta_inv_sort_sn (a) (h) (G) (L) (X2): - ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 → ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2. + ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 → + ∧∧ ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]. #a #h #G #L #X2 #s #H elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H lapply (cpms_inv_sort1 … H) -H #H destruct -/2 width=1 by cpcs_cprs_sn/ +/3 width=1 by cpcs_cprs_sn, conj/ +qed-. + +lemma nta_inv_ldec_sn_cnv (a) (h) (G) (K) (V): + ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[a,h] X2 → + ∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⬆*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![a,h]. +#a #h #G #Y #X #X2 #H +elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 +elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct +elim (cpms_inv_ell_sn … H2) -H2 * +[ #_ #H destruct +| #m #W #HVW #HWX1 #H destruct + elim (lifts_total V (𝐔❴1❵)) #U #HVU + lapply (cpms_lifts_bi … HVW (Ⓣ) … (K.ⓛV) … HVU … HWX1) -W + [ /3 width=1 by drops_refl, drops_drop/ ] #HUX1 + /3 width=5 by cprs_div, ex4_intro/ +] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma index 0701dcf8b..320ec675c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_etc.ma @@ -1,57 +1,8 @@ (* -(* Advanced inversion lemmas ************************************************) - - -(* Basic_1: was ty3_gen_lref *) -lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U → - (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W & - ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U - ) ∨ - (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V & - ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U - ). -/2 width=3/ qed-. - (* Advanced forvard lemmas **************************************************) lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U → ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U. /2 width=3/ qed-. -lemma nta_ind_alt: ∀h. ∀R:lenv→relation term. - (∀L,k. R L ⋆k ⋆(next h k)) → - (∀L,K,V,W,U,i. - ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U → - R K V W → R L (#i) U - ) → - (∀L,K,W,V,U,i. - ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U → - R K W V → R L (#i) U - ) → - (∀I,L,V,W,T,U. - ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U → - R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U) - ) → - (∀L,V,W,T,U. - ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) → - R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U) - ) → - (∀L,V,W,T,U. - ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W → - R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U) - ) → - (∀L,T,U,W. - ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → - R L T U → R L U W → R L (ⓝU.T) U - ) → - (∀L,T,U1,U2,V2. - ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 → - R L T U1 →R L U2 V2 →R L T U2 - ) → - ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U. -#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U -// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/ -/3 width=7 by ntaa_nta/ -qed-. - *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma new file mode 100644 index 000000000..2e655049e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma @@ -0,0 +1,79 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/nta_drops.ma". +include "basic_2/dynamic/nta_cpms.ma". +include "basic_2/dynamic/nta_cpcs.ma". +include "basic_2/dynamic/nta_preserve.ma". + +(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************) + +(* Advanced eliminators *****************************************************) + +lemma nta_ind_rest_cnv (h) (Q:relation4 …): + (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀G,K,V,W,U. + ⦃G,K⦄ ⊢ V :[h] W → ⬆*[1] W ≘ U → + Q G K V W → Q G (K.ⓓV) (#0) U + ) → + (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) → + (∀I,G,K,W,U,i. + ⦃G,K⦄ ⊢ #i :[h] W → ⬆*[1] W ≘ U → + Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U + ) → + (∀p,I,G,K,V,T,U. + ⦃G,K⦄ ⊢ V ![h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :[h] U → + Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U) + ) → + (∀p,G,L,V,W,T,U. + ⦃G,L⦄ ⊢ V :[h] W → ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U → + Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U) + ) → + (∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U → Q G L (ⓝU.T) U + ) → + (∀G,L,T,U1,U2. + ⦃G,L⦄ ⊢ T :[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![h] → + Q G L T U1 → Q G L T U2 + ) → + ∀G,L,T,U. ⦃G,L⦄ ⊢ T :[h] U → Q G L T U. +#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #G #L #T +@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] +[ #s #HG #HL #HT #X #H destruct -IH + elim (nta_inv_sort_sn … H) -H #HUX #HX + /2 width=4 by/ +| * [| #i ] #HG #HL #HT #X #H destruct + [ elim (nta_inv_lref_sn_drops_cnv … H) -H * + [ #K #V #W #U #H #HVW #HWU #HUX #HX + lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct + /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/ + | #K #W #U #H #HW #HWU #HUX #HX + lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct + /3 width=4 by nta_ldec_cnv/ + ] + | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct + /5 width=7 by nta_lref, fqu_fqup/ + ] +| #l #HG #HL #HT #U #H destruct -IH + elim (nta_inv_gref_sn … H) +| #p #I #V #T #HG #HL #HT #X #H destruct + elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX + /4 width=5 by nta_bind_cnv/ +| #V #T #HG #HL #HT #X #H destruct + elim (nta_inv_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX + /4 width=9 by nta_appl/ +| #U #T #HG #HL #HT #X #H destruct + elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX + /4 width=4 by nta_cast/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma index 464e8603a..e6dd70e65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma @@ -58,6 +58,53 @@ qed. (* Inversion lemmas based on preservation ***********************************) +lemma nta_inv_ldef_sn (a) (h) (G) (K) (V): + ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] X2 → + ∃∃W,U. ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[1] W ≘ U & ⦃G,K.ⓓV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓓV⦄ ⊢ X2 ![a,h]. +#a #h #G #Y #X #X2 #H +elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 +elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct +elim (cpms_inv_delta_sn … H2) -H2 * +[ #_ #H destruct +| #W #HVW #HWX1 + /3 width=5 by cnv_cpms_nta, cpcs_cprs_sn, ex4_2_intro/ +] +qed-. + +lemma nta_inv_lref_sn (a) (h) (G) (L): + ∀X2,i. ⦃G,L⦄ ⊢ #↑i :[a,h] X2 → + ∃∃I,K,T2,U2. ⦃G,K⦄ ⊢ #i :[a,h] T2 & ⬆*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![a,h] & L = K.ⓘ{I}. +#a #h #G #L #X2 #i #H +elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 +elim (cnv_inv_lref … H1) -H1 #I #K #Hi #H destruct +elim (cpms_inv_lref_sn … H2) -H2 * +[ #_ #H destruct +| #X #HX #HX1 + /3 width=9 by cnv_cpms_nta, cpcs_cprs_sn, ex5_4_intro/ +] +qed-. + +lemma nta_inv_lref_sn_drops_cnv (a) (h) (G) (L): + ∀X2, i. ⦃G,L⦄ ⊢ #i :[a,h] X2 → + ∨∨ ∃∃K,V,W,U. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h] + | ∃∃K,W,U. ⬇*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![a,h] & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]. +#a #h #G #L #X2 #i #H +elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2 +elim (cnv_inv_lref_drops … H1) -H1 #I #K #V #HLK #HV +elim (cpms_inv_lref1_drops … H2) -H2 * +[ #_ #H destruct +| #Y #X #W #H #HVW #HUX1 + lapply (drops_mono … H … HLK) -H #H destruct + /4 width=8 by cnv_cpms_nta, cpcs_cprs_sn, ex5_4_intro, or_introl/ +| #n #Y #X #U #H #HVU #HUX1 #H0 destruct + lapply (drops_mono … H … HLK) -H #H destruct + elim (lifts_total V (𝐔❴↑i❵)) #W #HVW + lapply (cpms_lifts_bi … HVU (Ⓣ) … L … HVW … HUX1) -U + [ /2 width=2 by drops_isuni_fwd_drop2/ ] #HWX1 + /4 width=9 by cprs_div, ex5_3_intro, or_intror/ +] +qed-. + lemma nta_inv_bind_sn_cnv (a) (h) (p) (I) (G) (K) (X2): ∀V,T. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] X2 → ∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U & ⦃G,K⦄ ⊢ ⓑ{p,I}V.U ⬌*[h] X2 & ⦃G,K⦄ ⊢ X2 ![a,h]. @@ -93,6 +140,29 @@ elim (cnv_cpms_conf … H1 … H2 … HVTU) -H1 -H2 -HVTU