From 48bd1f41417fb167a100eb1613a64a711484b69a Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Oct 2019 18:35:57 +0200 Subject: [PATCH] update in basic_2 + new definition of cpce --- .../lambdadelta/basic_2/dynamic/cnv_cpce.ma | 4 +- .../lambdadelta/basic_2/dynamic/cnv_lpce.ma | 70 ++++++-- .../lambdadelta/basic_2/rt_conversion/cpce.ma | 158 ++++++++++++------ .../basic_2/rt_conversion/cpce_drops.ma | 94 +++++++---- .../basic_2/rt_conversion/lpce_drops.ma | 26 +++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../ground_2/notation/xoa/ex_7_8.ma | 26 +++ .../lambdadelta/ground_2/xoa/ex_7_8.ma | 28 ++++ .../lambdadelta/ground_2/xoa2.conf.xml | 1 + 9 files changed, 313 insertions(+), 98 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_7_8.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/xoa/ex_7_8.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma index a4b4078d8..b9b6560fb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma @@ -20,8 +20,9 @@ include "basic_2/dynamic/cnv_cpmuwe.ma". (* Properties with context-sensitive parallel eta-conversion for terms ******) -lemma cpce_total_cnv (h) (a) (G) (L): +axiom cpce_total_cnv (h) (a) (G) (L): ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] → ∃T2. ⦃G,L⦄ ⊢ T1 ⬌η[h] T2. +(* #h #a #G #L #T1 #HT1 lapply (cnv_fwd_csx … HT1) #H generalize in match HT1; -HT1 @@ -67,3 +68,4 @@ generalize in match HT1; -HT1 /3 width=2 by cpce_flat, ex_intro/ ] qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma index 33ce0e024..401b10bdb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_lpce.ma @@ -12,39 +12,77 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/cnv_cpce.ma". +include "basic_2/rt_transition/lpr_drops.ma". +include "basic_2/rt_computation/cpms_lpr.ma". +include "basic_2/rt_computation/fpbg_fqup.ma". +include "basic_2/rt_conversion/cpce_drops.ma". +include "basic_2/rt_conversion/lpce_drops.ma". +include "basic_2/dynamic/cnv_drops.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) definition IH (h) (a): relation3 genv lenv term ≝ λG,L0,T0. ⦃G,L0⦄ ⊢ T0 ![h,a] → ∀n,T1. ⦃G,L0⦄ ⊢ T0 ➡[n,h] T1 → ∀T2. ⦃G,L0⦄ ⊢ T0 ⬌η[h] T2 → - ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → - ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L0⦄ ⊢ T2 ➡[n,h] T. + ∀L1. ⦃G,L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L0⦄ ⊢ ⬌η[h] L2 → + ∃∃T. ⦃G,L1⦄ ⊢ T1 ⬌η[h] T & ⦃G,L2⦄ ⊢ T2 ➡[n,h] T. + +(* Properties with eta-conversion for full local environments ***************) lemma pippo_aux (h) (a) (G0) (L0) (T0): (∀G,L,T. ⦃G0,L0,T0⦄ >[h] ⦃G,L,T⦄ → IH h a G L T) → IH h a G0 L0 T0. #h #a #G0 #L0 * * -[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 +[ #s #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 elim (cpm_inv_sort1 … HX1) -HX1 #H #Hn destruct lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct /3 width=3 by cpce_sort, cpm_sort, ex2_intro/ -| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01 +| #i #IH #Hi #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 elim (cnv_inv_lref_drops … Hi) -Hi #I #K0 #W0 #HLK0 #HW0 elim (lpr_drops_conf … HLK0 … HL01) [| // ] #Y1 #H1 #HLK1 - elim (lex_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct - elim (cpce_inv_lref_sn_drops_bind … HX2 … HLK0) -HX2 * - [ #HI #H destruct - elim (cpm_inv_lref1_drops … HX1) -HX1 * - [ #H1 #H2 destruct -HW0 -HLK0 -IH + elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK01 #HW01 #H destruct + elim (lpce_drops_conf … HLK0 … HL02) [| // ] #Y2 #H2 #HLK2 + elim (lpce_inv_pair_sn … H2) -H2 #K2 #W2 #HK02 #HW02 #H destruct + elim (cpm_inv_lref1_drops … HX1) -HX1 * + [ #H1 #H2 destruct + elim (cpce_inv_lref_sn_drops_pair … HX2 … HLK0) -HX2 * + [ #H1 #H2 destruct -L0 -K0 -W0 + /3 width=3 by cpce_ldef_drops, ex2_intro/ + | #H1 #HW #H2 destruct -L0 -W2 -HW0 -HK02 @(ex2_intro … (#i)) [| // ] - @cpce_zero_drops #n #p #Y1 #X1 #V1 #U1 #HLY1 #HWU1 - lapply (drops_mono … HLY1 … HLK1) -L1 #H2 destruct - /4 width=12 by lpr_cpms_trans, cpms_step_sn/ - | #Y0 #W0 #W1 #HLY0 #HW01 #HWX1 -HI -HW0 -IH - lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct - @(ex2_intro … X1) [| /2 width=6 by cpm_delta_drops/ ] + @(cpce_ldec_drops … HLK1) -HLK1 #n #p #V0 #U0 #HWU0 + /4 width=10 by lpr_cpms_trans, cpms_step_sn/ + | #n #p #W01 #W02 #V0 #V01 #V02 #U0 #H1 #HWU0 #HW001 #HW012 #HV001 #HV012 #H2 destruct + ] + | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1 + #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 -HL01 -HL02 + lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct + lapply (cpce_inv_lref_sn_drops_ldef … HX2 … HLK0) -HX2 #H destruct + elim (IH … HW0 … HW01 … HW02 … HK01 … HK02) + [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 + elim (lifts_total W (𝐔❴↑i❵)) #V #HWV + /3 width=9 by cpce_lifts_bi, cpm_delta_drops, ex2_intro/ + | lapply (drops_isuni_fwd_drop2 … HLK1) [ // ] -W1 #HLK1 + #m #Y0 #X0 #W1 #HLY0 #HW01 #HWX1 #H destruct -HL01 -HL02 + lapply (drops_mono … HLY0 … HLK0) -HLY0 #H destruct + elim (cpce_inv_lref_sn_drops_ldec … HX2 … HLK0) -HX2 * + [ #_ #H destruct + elim (IH … HW0 … HW01 … HW02 … HK01 … HK02) + [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 + elim (lifts_total W (𝐔❴↑i❵)) #V #HWV + /3 width=9 by cpce_lifts_bi, cpm_ell_drops, ex2_intro/ + | lapply (drops_isuni_fwd_drop2 … HLK2) [ // ] -W2 #HLK2 + #n #p #W01 #W02 #V0 #V01 #V02 #U0 #_ #HW001 #HW012 #_ #_ #H destruct -V0 -V01 -U0 + elim (IH … HW0 … HW01 … HW001 … HK01 … HK02) + [| /3 width=2 by fqup_fpbg, fqup_lref/ ] -L0 -K0 #W #HW1 #HW2 + elim (lifts_total W (𝐔❴↑i❵)) #V #HWV + /4 width=11 by cpce_lifts_bi, cpm_lifts_bi, cpm_ee, ex2_intro/ + ] + ] +| #l #_ #_ #n #X1 #HX1 #X2 #HX2 #L1 #HL01 #L2 #HL02 + elim (cpm_inv_gref1 … HX1) -HX1 #H1 #H2 destruct + lapply (cpce_inv_gref_sn … HX2) -HX2 #H destruct + /3 width=3 by cpce_gref, cpr_refl, ex2_intro/ (* lemma cpce_inv_eta_drops (h) (n) (G) (L) (i): 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 7deb96dab..5ba7d4f3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/xoa/ex_5_7.ma". include "basic_2/notation/relations/pconveta_5.ma". include "basic_2/rt_computation/cpms.ma". @@ -22,10 +21,14 @@ include "basic_2/rt_computation/cpms.ma". inductive cpce (h): relation4 genv lenv term term ≝ | cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s) | 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_unit: ∀I,G,K. cpce h G (K.ⓤ{I}) (#0) (#0) +| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0) +| cpce_ldec: ∀G,K,W. (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → + cpce h G (K.ⓛW) (#0) (#0) +| cpce_eta : ∀n,p,G,K,W,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → + cpce h G K W W1 → ⇧*[1] W1 ≘ W2 → + cpce h G K V V1 → ⇧*[1] V1 ≘ V2 → + cpce h G (K.ⓛW) (#0) (ⓝW2.+ⓛV2.ⓐ#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) @@ -43,14 +46,16 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma cpce_inv_sort_sn (h) (G) (L) (X2): - ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2. -#h #G #Y #X2 #s0 +lemma cpce_inv_sort_sn (h) (G) (L) (s): + ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2. +#h #G #Y #s0 #X2 @(insert_eq_0 … (⋆s0)) #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 #_ // +| #G #K #V #_ // +| #G #K #W #_ #_ // +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct | #G #L #l #_ // | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct @@ -58,16 +63,18 @@ lemma cpce_inv_sort_sn (h) (G) (L) (X2): ] qed-. -lemma cpce_inv_atom_sn (h) (G) (X2): - ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2. -#h #G #X2 #j +lemma cpce_inv_atom_sn (h) (G) (i): + ∀X2. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2. +#h #G #i0 #X2 @(insert_eq_0 … LAtom) #Y -@(insert_eq_0 … (#j)) #X1 +@(insert_eq_0 … (#i0)) #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 #_ #_ // +| #G #K #V #_ #_ // +| #G #K #W #_ #_ #_ // +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #_ #H destruct | #G #L #l #_ #_ // | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct @@ -75,19 +82,62 @@ lemma cpce_inv_atom_sn (h) (G) (X2): ] qed-. -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 +lemma cpce_inv_unit_sn (h) (I) (G) (K): + ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. +#h #I0 #G #K0 #X2 +@(insert_eq_0 … (K0.ⓤ{I0})) #Y +@(insert_eq_0 … (#0)) #X1 +* -G -Y -X1 -X2 +[ #G #L #s #_ #_ // +| #G #i #_ #_ // +| #I #G #K #_ #_ // +| #G #K #V #_ #_ // +| #G #K #W #_ #_ #_ // +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #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) (V): + ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2. +#h #G #K0 #V0 #X2 +@(insert_eq_0 … (K0.ⓓV0)) #Y +@(insert_eq_0 … (#0)) #X1 +* -G -Y -X1 -X2 +[ #G #L #s #_ #_ // +| #G #i #_ #_ // +| #I #G #K #_ #_ // +| #G #K #V #_ #_ // +| #G #K #W #_ #_ #_ // +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #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) (W): + ∀X2. ⦃G,K.ⓛW⦄ ⊢ #0 ⬌η[h] X2 → + ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2 + | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U + & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[1] W1 ≘ W2 + & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[1] V1 ≘ V2 + & ⓝW2.+ⓛV2.ⓐ#0.#1 = X2. +#h #G #K0 #W0 #X2 +@(insert_eq_0 … (K0.ⓛW0)) #Y @(insert_eq_0 … (#0)) #X1 * -G -Y -X1 -X2 [ #G #L #s #H #_ destruct | #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 #_ #H destruct +| #G #K #V #_ #H destruct +| #G #K #W #HW #_ #H destruct /4 width=5 by or_introl, conj/ +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #HWU #HW1 #HW12 #HV1 #HV12 #_ #H destruct + /3 width=14 by or_intror, ex6_8_intro/ | #I #G #K #T #U #i #_ #_ #H #_ destruct | #G #L #l #H #_ destruct | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct @@ -95,17 +145,19 @@ lemma cpce_inv_zero_sn (h) (G) (K) (X2): ] qed-. -lemma cpce_inv_lref_sn (h) (G) (K) (X2): - ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 → +lemma cpce_inv_lref_sn (h) (I) (G) (K) (i): + ∀X2. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 → ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⇧*[1] T2 ≘ X2. -#h #G #Y0 #X2 #Z #j -@(insert_eq_0 … (Y0.ⓘ{Z})) #Y -@(insert_eq_0 … (#↑j)) #X1 +#h #I0 #G #K0 #i0 #X2 +@(insert_eq_0 … (K0.ⓘ{I0})) #Y +@(insert_eq_0 … (#↑i0)) #X1 * -G -Y -X1 -X2 [ #G #L #s #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 #H #_ destruct +| #G #K #V #H #_ destruct +| #G #K #W #_ #H #_ destruct +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #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 @@ -113,14 +165,16 @@ lemma cpce_inv_lref_sn (h) (G) (K) (X2): ] 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 +lemma cpce_inv_gref_sn (h) (G) (L) (l): + ∀X2. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2. +#h #G #Y #l0 #X2 +@(insert_eq_0 … (§l0)) #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 #_ // +| #G #K #V #_ // +| #G #K #W #_ #_ // +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #U #_ #_ #_ #_ #_ #H destruct | #I #G #K #T #U #i #_ #_ #H destruct | #G #L #l #_ // | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct @@ -128,15 +182,17 @@ lemma cpce_inv_gref_sn (h) (G) (L) (X2): ] qed-. -lemma cpce_inv_bind_sn (h) (G) (K) (X2): - ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 → +lemma cpce_inv_bind_sn (h) (p) (I) (G) (K) (V1) (T1): + ∀X2. ⦃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 +#h #p0 #I0 #G #Y #V0 #T0 #X2 +@(insert_eq_0 … (ⓑ{p0,I0}V0.T0)) #X1 * -G -Y -X1 -X2 [ #G #L #s #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 #H destruct +| #G #K #V #H destruct +| #G #K #W #_ #H destruct +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #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/ @@ -144,15 +200,17 @@ lemma cpce_inv_bind_sn (h) (G) (K) (X2): ] qed-. -lemma cpce_inv_flat_sn (h) (G) (L) (X2): - ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 → +lemma cpce_inv_flat_sn (h) (I) (G) (L) (V1) (T1): + ∀X2. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 → ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2. -#h #G #Y #X2 #Z #U #X -@(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2 +#h #I0 #G #Y #V0 #T0 #X2 +@(insert_eq_0 … (ⓕ{I0}V0.T0)) #X1 * -G -Y -X1 -X2 [ #G #L #s #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 #H destruct +| #G #K #V #H destruct +| #G #K #W #_ #H destruct +| #n #p #G #K #W #W1 #W2 #V #V1 #V2 #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 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 index 25be293aa..fbf7b3002 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/xoa/ex_7_8.ma". include "basic_2/rt_computation/cpms_drops.ma". include "basic_2/rt_conversion/cpce.ma". @@ -19,29 +20,45 @@ include "basic_2/rt_conversion/cpce.ma". (* Advanced properties ******************************************************) -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/ +lemma cpce_ldef_drops (h) (G) (K) (V): + ∀i,L. ⇩*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i ⬌η[h] #i. +#h #G #K #V #i elim i -i +[ #L #HLK + lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct + /2 width=1 by cpce_ldef/ +| #i #IH #L #HLK + elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct + /3 width=3 by cpce_lref/ ] qed. -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 +lemma cpce_ldec_drops (h) (G) (K) (W): + (∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) → + ∀i,L. ⇩*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i ⬌η[h] #i. +#h #G #K #W #HW #i elim i -i +[ #L #HLK + lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct + /3 width=5 by cpce_ldec/ +| #i #IH #L #HLK + elim (drops_inv_succ … HLK) -HLK #Z #Y #HYK #H destruct + /3 width=3 by cpce_lref/ +] +qed. + +lemma cpce_eta_drops (h) (G) (K) (W): + ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → + ∀W1. ⦃G,K⦄ ⊢ W ⬌η[h] W1 → ∀V1. ⦃G,K⦄ ⊢ V ⬌η[h] V1 → + ∀i,L. ⇩*[i] L ≘ K.ⓛW → ∀W2. ⇧*[↑i] W1 ≘ W2 → + ∀V2. ⇧*[↑i] V1 ≘ V2 → ⦃G,L⦄ ⊢ #i ⬌η[h] ⓝW2.+ⓛV2.ⓐ#0.#↑i. +#h #G #K #W #n #p #V #U #HWU #W1 #HW1 #V1 #HV1 #i elim i -i +[ #L #HLK #W2 #HW12 #V2 #HV12 + lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct + /2 width=8 by cpce_eta/ +| #i #IH #L #HLK #W2 #HW12 #V2 #HV12 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/ + elim (lifts_split_trans … HW12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XW #HXW1 #HXW2 + elim (lifts_split_trans … HV12 (𝐔❴↑i❵) (𝐔❴1❵)) [| // ] #XV #HXV1 #HXV2 + /6 width=9 by cpce_lref, lifts_push_lref, lifts_bind, lifts_flat/ ] qed. @@ -61,12 +78,29 @@ qed-. (* Advanced inversion lemmas ************************************************) -lemma cpce_inv_lref_sn_drops_bind (h) (G) (i) (L): +axiom cpce_inv_lref_sn_drops_pair (h) (G) (i) (L): ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → - ∀I,K. ⇩*[i] L ≘ K.ⓘ{I} → - ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2 - | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 - & ⇧*[↑i] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#(↑i) = X2. + ∀I,K,W. ⇩*[i] L ≘ K.ⓑ{I}W → + ∨∨ ∧∧ Abbr = I & #i = X2 + | ∧∧ Abst = I & ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2 + | ∃∃n,p,W1,W2,V,V1,V2,U. Abst = I & ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U + & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2 + & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2 + & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2. + +axiom cpce_inv_lref_sn_drops_ldef (h) (G) (i) (L): + ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → + ∀K,V. ⇩*[i] L ≘ K.ⓓV → #i = X2. + +axiom cpce_inv_lref_sn_drops_ldec (h) (G) (i) (L): + ∀X2. ⦃G,L⦄ ⊢ #i ⬌η[h] X2 → + ∀K,W. ⇩*[i] L ≘ K.ⓛW → + ∨∨ ∧∧ ∀n,p,V,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #i = X2 + | ∃∃n,p,W1,W2,V,V1,V2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U + & ⦃G,K⦄ ⊢ W ⬌η[h] W1 & ⇧*[↑i] W1 ≘ W2 + & ⦃G,K⦄ ⊢ V ⬌η[h] V1 & ⇧*[↑i] V1 ≘ V2 + & ⓝW2.+ⓛV2.ⓐ#0.#(↑i) = X2. +(* #h #G #i elim i -i [ #L #X2 #HX2 #I #K #HLK lapply (drops_fwd_isid … HLK ?) -HLK [ // ] #H destruct @@ -101,11 +135,12 @@ elim (cpce_inv_lref_sn_drops_bind … HX2 … HLK) -L * elim (HI … HWU) -n -p -K -X2 -V1 -V2 -W2 -U -i // ] qed-. - +*) (* Properties with uniform slicing for local environments *******************) -lemma cpce_lifts_sn (h) (G): +axiom cpce_lifts_sn (h) (G): d_liftable2_sn … lifts (cpce h G). +(* #h #G #K #T1 #T2 #H elim H -G -K -T1 -T2 [ #G #K #s #b #f #L #HLK #X #HX lapply (lifts_inv_sort1 … HX) -HX #H destruct @@ -172,15 +207,16 @@ lemma cpce_lifts_sn (h) (G): /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ ] qed-. - +*) lemma cpce_lifts_bi (h) (G): d_liftable2_bi … lifts (cpce h G). /3 width=12 by cpce_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. (* Inversion lemmas with uniform slicing for local environments *************) -lemma cpce_inv_lifts_sn (h) (G): +axiom cpce_inv_lifts_sn (h) (G): d_deliftable2_sn … lifts (cpce h G). +(* #h #G #K #T1 #T2 #H elim H -G -K -T1 -T2 [ #G #K #s #b #f #L #HLK #X #HX lapply (lifts_inv_sort2 … HX) -HX #H destruct @@ -249,7 +285,7 @@ lemma cpce_inv_lifts_sn (h) (G): /3 width=5 by cpce_flat, lifts_flat, ex2_intro/ ] qed-. - +*) lemma cpce_inv_lifts_bi (h) (G): d_deliftable2_bi … lifts (cpce h G). /3 width=12 by cpce_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_drops.ma new file mode 100644 index 000000000..2d683d06f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/lpce_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/relocation/drops_lex.ma". +include "basic_2/rt_conversion/lpce.ma". + +(* PARALLEL ETA-CONVERSION FOR FULL LOCAL ENVIRONMENTS **********************) + +(* Inversion lemmas with generic slicing for local environments *************) + +lemma lpce_drops_conf (h) (G): dropable_sn (cpce h G). +/2 width=3 by lex_dropable_sn/ qed-. + +lemma lpce_drops_trans (h) (G): dropable_dx (cpce h G). +/2 width=3 by lex_dropable_dx/ qed-. 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 784332f15..3422c89b3 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 @@ -25,7 +25,7 @@ table { ] [ { "context-sensitive native validity" * } { [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ] - [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_lpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } @@ -45,7 +45,7 @@ table { class "blue" [ { "rt-conversion" * } { [ { "context-sensitive parallel eta-conversion" * } { - [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" * ] + [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" "lpce_drops" * ] [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ] [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" "cpce_drops" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_7_8.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_7_8.ma new file mode 100644 index 000000000..9cb6e9c21 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_7_8.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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (7, 8) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex8 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex8 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P6) }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_7_8.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_7_8.ma new file mode 100644 index 000000000..6013be252 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_7_8.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_7_8.ma". + +(* multiple existental quantifier (7, 8) *) + +inductive ex7_8 (A0,A1,A2,A3,A4,A5,A6,A7:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→A7→Prop) : Prop ≝ + | ex7_8_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7. P0 x0 x1 x2 x3 x4 x5 x6 x7 → P1 x0 x1 x2 x3 x4 x5 x6 x7 → P2 x0 x1 x2 x3 x4 x5 x6 x7 → P3 x0 x1 x2 x3 x4 x5 x6 x7 → P4 x0 x1 x2 x3 x4 x5 x6 x7 → P5 x0 x1 x2 x3 x4 x5 x6 x7 → P6 x0 x1 x2 x3 x4 x5 x6 x7 → ex7_8 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 8)" 'Ex8 P0 P1 P2 P3 P4 P5 P6 = (ex7_8 ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index 8f974dbe0..2643ba620 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -8,6 +8,7 @@ 1 4 5 1 5 7 + 7 8 9 3 -- 2.39.2