From 6b4da5fa47d474dcf2f203ec7f5ed36938739c9b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 29 May 2019 21:52:30 +0200 Subject: [PATCH] update in basic_2 + totality for fixed cpce + Makefile: bug fixed --- matita/matita/contribs/lambdadelta/Makefile | 2 +- .../lambdadelta/basic_2/dynamic/cnv.ma | 8 ++ .../lambdadelta/basic_2/dynamic/cnv_cpce.ma | 68 ++++++++++++ .../lambdadelta/basic_2/dynamic/cnv_fsb.ma | 7 ++ .../basic_2/rt_computation/fpbg.ma | 7 ++ .../lambdadelta/basic_2/rt_conversion/cpce.ma | 104 +++++++++++------- .../basic_2/rt_conversion/cpce_drops.ma | 46 ++++++++ .../static_2/relocation/drops_drops.ma | 20 +++- 8 files changed, 215 insertions(+), 47 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 9d87f9909..59cf50f6e 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -95,7 +95,7 @@ $(DEP_INPUT): LINE = $(MAS:%=%:include \"\".) $(DEP_INPUT): $(MAS) Makefile @echo " GREP include" - $(H)grep "include \"" $^ > $(DEP_INPUT) + $(H)grep "include \"" $(MAS) > $(DEP_INPUT) $(H)echo "$(LINE)" | sed -e 's/\"\. /\"\.\n/g' >> $(DEP_INPUT) # dep ######################################################################## diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index c3fa8e11b..4db46f940 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -159,6 +159,14 @@ lemma cnv_fwd_flat (a) (h) (I) (G) (L): ] -H /2 width=1 by conj/ qed-. +lemma cnv_fwd_pair_sn (a) (h) (I) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![a,h] → ⦃G,L⦄ ⊢ V ![a,h]. +#a #h * [ #p ] #I #G #L #V #T #H +[ elim (cnv_inv_bind … H) -H #HV #_ +| elim (cnv_fwd_flat … H) -H #HV #_ +] // +qed-. + (* Basic_2A1: removed theorems 3: shnv_cast shnv_inv_cast snv_shnv_cast *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma new file mode 100644 index 000000000..faca3d631 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -0,0 +1,68 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/cpue_csx.ma". +include "basic_2/rt_conversion/cpce_drops.ma". +include "basic_2/dynamic/cnv_cpue.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with context-sensitive parallel eta-conversion for terms ******) + +lemma cpce_total_cnv (a) (h) (G) (L): + ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. +#a #h #G #L #T1 #HT1 +lapply (cnv_fwd_csx … HT1) #H +generalize in match HT1; -HT1 +@(csx_ind_fpbg … H) -G -L -T1 +#G #L * * +[ #s #_ #_ /2 width=2 by cpce_sort, ex_intro/ +| #i #H1i #IH #H2i + elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ] + [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W + lapply (csx_inv_lref_pair … HLK H1i) -H1i #H1W + elim (cpue_total_csx … H1W) -H1W #X + elim (abst_dec X) [ * | -IH ] + [ #p #V1 #U #H destruct * #n #HWU #_ + elim (IH G K V1) -IH + [ #V2 #HV12 + elim (lifts_total V2 (𝐔❴↑i❵)) #W2 #HVW2 + /3 width=12 by cpce_eta_drops, ex_intro/ + | /3 width=6 by cnv_cpms_trans, cnv_fwd_pair_sn/ + | /4 width=6 by fqup_cpms_fwd_fpbg, fpbg_fqu_trans, fqup_lref/ + ] + | #HnX #HWX + @(ex_intro … (#i)) + @cpce_zero_drops #n0 #p #K0 #W0 #V0 #U0 #HLK0 #HWU0 + lapply (drops_mono … HLK0 … HLK) -i -L #H destruct + elim (cnv_cpue_cpms_conf … H2W … HWU0 … HWX) -n0 -W #X0 * #n0 #HUX0 #_ #HX0 + elim (cpms_inv_abst_sn … HUX0) -HUX0 #V1 #U1 #_ #_ #H destruct -n0 -K -V0 -U0 + elim (tueq_inv_bind2 … HX0) -HX0 #U0 #_ #H destruct -U1 + /2 width=4 by/ + ] + | /5 width=3 by cpce_zero_drops, ex1_2_intro, ex_intro/ + ] +| #l #_ #_ /2 width=2 by cpce_gref, ex_intro/ +| #p #I #V1 #T1 #_ #IH #H + elim (cnv_inv_bind … H) -H #HV1 #HT1 + elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 + elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12 + /3 width=2 by cpce_bind, ex_intro/ +| #I #V1 #T1 #_ #IH #H + elim (cnv_fwd_flat … H) -H #HV1 #HT1 + elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12 + elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_flat_dx/ ] #T2 #HT12 + /3 width=2 by cpce_flat, ex_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma index 46c1255d6..763faf1d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_fsb.ma @@ -24,6 +24,13 @@ lemma cnv_fwd_fsb (a) (h): ∀G,L,T. ⦃G, L⦄ ⊢ T ![a, h] → ≥[h] 𝐒⦃ #a #h #G #L #T #H elim (cnv_fwd_aaa … H) -H /2 width=2 by aaa_fsb/ qed-. +(* Forward lemmas with strongly rt-normalizing terms ************************) + +lemma cnv_fwd_csx (a) (h): ∀G,L,T. ⦃G,L⦄ ⊢ T ![a,h] → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄. +#a #h #G #L #T #H +/3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ +qed-. + (* Inversion lemmas with proper parallel rst-computation for closures *******) lemma cnv_fpbg_refl_false (a) (h) (G) (L) (T): diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma index 1ce29c009..ba56fd0c5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma @@ -38,6 +38,13 @@ lemma fpbg_fpbq_trans: ∀h,G1,G,G2,L1,L,L2,T1,T,T2. /3 width=9 by fpbs_strap1, ex2_3_intro/ qed-. +lemma fpbg_fqu_trans (h): ∀G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ >[h] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ >[h] ⦃G2, L2, T2⦄. +#h #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 +/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/ +qed-. + (* Note: this is used in the closure proof *) lemma fpbg_fpbs_trans: ∀h,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h] ⦃G2, L2, T2⦄ → ∀G1,L1,T1. ⦃G1, L1, T1⦄ >[h] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h] ⦃G2, L2, T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma index 259fc7b07..3da6a1598 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/xoa/ex_5_7.ma". include "basic_2/notation/relations/pconveta_5.ma". include "basic_2/rt_computation/cpms.ma". @@ -20,13 +21,14 @@ include "basic_2/rt_computation/cpms.ma". (* avtivate genv *) inductive cpce (h): relation4 genv lenv term term ≝ | cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s) -| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0) -| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s → - cpce h G (K.ⓛV) (#0) (#0) -| cpce_eta : ∀n,p,G,K,V,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T → - cpce h G K W1 W2 → cpce h G (K.ⓛV) (#0) (+ⓛW2.ⓐ#0.#1) +| cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i) +| cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → + cpce h G (K.ⓘ{I}) (#0) (#0) +| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U → + cpce h G K V1 V2 → ⬆*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1) | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T → ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U +| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l) | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2. cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 → cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) @@ -46,44 +48,48 @@ lemma cpce_inv_sort_sn (h) (G) (L) (X2): #h #G #Y #X2 #s0 @(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2 [ #G #L #s #_ // -| #G #K #V #_ // -| #n #G #K #V #s #_ #_ // -| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct +| #G #i #_ // +| #G #K #I #_ #_ // +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct +| #G #L #l #_ // | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct ] qed-. -lemma cpce_inv_ldef_sn (h) (G) (K) (X2): - ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. -#h #G #Y #X2 #X -@(insert_eq_0 … (Y.ⓓX)) #Y1 -@(insert_eq_0 … (#0)) #X1 -* -G -Y1 -X1 -X2 +lemma cpce_inv_atom_sn (h) (G) (X2): + ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2. +#h #G #X2 #j +@(insert_eq_0 … LAtom) #Y +@(insert_eq_0 … (#j)) #X1 +* -G -Y -X1 -X2 [ #G #L #s #_ #_ // -| #G #K #V #_ #_ // -| #n #G #K #V #s #_ #_ #_ // -| #n #p #G #K #V #W1 #W2 #T #_ #_ #_ #H destruct -| #I #G #K #T #U #i #_ #_ #H #_ destruct +| #G #i #_ #_ // +| #G #K #I #_ #_ #_ // +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #_ #H destruct +| #I #G #K #T #U #i #_ #_ #_ #H destruct +| #G #L #l #_ #_ // | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct ] qed-. -lemma cpce_inv_ldec_sn (h) (G) (K) (X2): - ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 → - ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2 - | ∃∃n,p,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T & ⦃G,K⦄ ⊢ W1 ⬌η[h] W2 & +ⓛW2.ⓐ#0.#1 = X2. -#h #G #Y #X2 #X -@(insert_eq_0 … (Y.ⓛX)) #Y1 +lemma cpce_inv_zero_sn (h) (G) (K) (X2): + ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 → + ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2 + | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 + & ⬆*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2. +#h #G #Y0 #X2 #Z +@(insert_eq_0 … (Y0.ⓘ{Z})) #Y @(insert_eq_0 … (#0)) #X1 -* -G -Y1 -X1 -X2 +* -G -Y -X1 -X2 [ #G #L #s #H #_ destruct -| #G #K #V #_ #H destruct -| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/ -| #n #p #G #K #V #W1 #W2 #T #HV #HW #_ #H destruct /3 width=8 by ex3_5_intro, or_intror/ +| #G #i #_ #H destruct +| #G #K #I #HI #_ #H destruct /4 width=7 by or_introl, conj/ +| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #_ #H destruct /3 width=12 by or_intror, ex5_7_intro/ | #I #G #K #T #U #i #_ #_ #H #_ destruct +| #G #L #l #H #_ destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct ] @@ -92,30 +98,47 @@ qed-. lemma cpce_inv_lref_sn (h) (G) (K) (X2): ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 → ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2. -#h #G #Y #X2 #Z #j -@(insert_eq_0 … (Y.ⓘ{Z})) #Y1 +#h #G #Y0 #X2 #Z #j +@(insert_eq_0 … (Y0.ⓘ{Z})) #Y @(insert_eq_0 … (#↑j)) #X1 -* -G -Y1 -X1 -X2 +* -G -Y -X1 -X2 [ #G #L #s #H #_ destruct -| #G #K #V #H #_ destruct -| #n #G #K #V #s #_ #H #_ destruct -| #n #p #G #K #V #W1 #W2 #T #_ #_ #H #_ destruct +| #G #i #_ #H destruct +| #G #K #I #_ #H #_ destruct +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H #_ destruct | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/ +| #G #L #l #H #_ destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct ] qed-. +lemma cpce_inv_gref_sn (h) (G) (L) (X2): + ∀l. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2. +#h #G #Y #X2 #k +@(insert_eq_0 … (§k)) #X1 * -G -Y -X1 -X2 +[ #G #L #s #_ // +| #G #i #_ // +| #G #K #I #_ #_ // +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct +| #I #G #K #T #U #i #_ #_ #H destruct +| #G #L #l #_ // +| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct +] +qed-. + lemma cpce_inv_bind_sn (h) (G) (K) (X2): ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 → ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2. #h #G #Y #X2 #q #Z #U #X @(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2 [ #G #L #s #H destruct -| #G #K #V #H destruct -| #n #G #K #V #s #_ #H destruct -| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct +| #G #i #H destruct +| #G #K #I #_ #H destruct +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct +| #G #L #l #H destruct | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct ] @@ -127,10 +150,11 @@ lemma cpce_inv_flat_sn (h) (G) (L) (X2): #h #G #Y #X2 #Z #U #X @(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2 [ #G #L #s #H destruct -| #G #K #V #H destruct -| #n #G #K #V #s #_ #H destruct -| #n #p #G #K #V #W1 #W2 #T #_ #_ #H destruct +| #G #i #H destruct +| #G #K #I #_ #H destruct +| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct +| #G #L #l #H destruct | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma new file mode 100644 index 000000000..49bf1e885 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/drops.ma". +include "basic_2/rt_conversion/cpce.ma". + +(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************) + +(* Properties with uniform slicing for local environments *******************) + +lemma cpce_eta_drops (h) (n) (G) (K): + ∀p,W,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U → + ∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 → + ∀i,L. ⬇*[i] L ≘ K.ⓛW → + ∀W2. ⬆*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i. +#h #n #G #K #p #W #V1 #U #HWU #V2 #HV12 #i elim i -i +[ #L #HLK #W2 #HVW2 + >(drops_fwd_isid … HLK) -L [| // ] /2 width=8 by cpce_eta/ +| #i #IH #L #HLK #W2 #HVW2 + elim (drops_inv_succ … HLK) -HLK #I #Y #HYK #H destruct + elim (lifts_split_trans … HVW2 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #X2 #HVX2 #HXW2 + /5 width=7 by cpce_lref, lifts_push_lref, lifts_bind, lifts_flat/ +] +qed. + +lemma cpce_zero_drops (h) (G): + ∀i,L. (∀n,p,K,W,V,U. ⬇*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → + ⦃G,L⦄ ⊢ #i ⬌η[h] #i. +#h #G #i elim i -i +[ * [ #_ // ] #L #I #Hi + /4 width=8 by cpce_zero, drops_refl/ +| #i #IH * [ -IH #_ // ] #L #I #Hi + /5 width=8 by cpce_lref, drops_drop/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma index 1c44ed555..4b52fd651 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_drops.ma @@ -91,6 +91,20 @@ lemma drops_mono: ∀b1,f,L,L1. ⬇*[b1, f] L ≘ L1 → /3 width=8 by drops_conf, drops_fwd_isid/ qed-. +lemma drops_inv_uni: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → ∀I,K. ⬇*[i] L ≘ K.ⓘ{I} → ⊥. +#L #i #H1 #I #K #H2 +lapply (drops_F … H2) -H2 #H2 +lapply (drops_mono … H2 … H1) -L -i #H destruct +qed-. + +lemma drops_ldec_dec: ∀L,i. Decidable (∃∃K,W. ⬇*[i] L ≘ K.ⓛW). +#L #i elim (drops_F_uni L i) [| * * [ #I #K1 | * #W1 #K1 ] ] +[4: /3 width=3 by ex1_2_intro, or_introl/ +|*: #H1L @or_intror * #K2 #W2 #H2L + lapply (drops_mono … H2L … H1L) -L #H destruct +] +qed-. + (* Basic_2A1: includes: drop_conf_lt *) lemma drops_conf_skip1: ∀b2,f,L,L2. ⬇*[b2, f] L ≘ L2 → ∀b1,f1,I1,K1. ⬇*[b1, f1] L ≘ K1.ⓘ{I1} → @@ -125,9 +139,3 @@ lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0 lapply (drops_mono … H0 … Hf2) -L #H destruct /2 width=1 by conj/ qed-. - -lemma drops_inv_uni: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≘ ⋆ → ∀I,K. ⬇*[i] L ≘ K.ⓘ{I} → ⊥. -#L #i #H1 #I #K #H2 -lapply (drops_F … H2) -H2 #H2 -lapply (drops_mono … H2 … H1) -L -i #H destruct -qed-. -- 2.39.2