From 87f57ddc367303c33e19c83cd8989cd561f3185b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 2 Jun 2019 15:52:42 +0200 Subject: [PATCH] milestone in basic_2 MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + Parametrized applicability condition allows λδ-2B to generalize both λδ-1A and λδ-1B. + ground_2: minor additions --- .../lambdadelta/apps_2/examples/ex_cnv_eta.ma | 10 ++--- .../lambdadelta/basic_2/dynamic/cnv.ma | 13 +++--- .../lambdadelta/basic_2/dynamic/cnv_aaa.ma | 43 +++++++------------ .../lambdadelta/basic_2/dynamic/cnv_cpes.ma | 29 ++++--------- .../basic_2/dynamic/cnv_cpm_tdeq.ma | 5 +-- .../basic_2/dynamic/cnv_cpm_trans.ma | 4 +- .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 17 +++++--- .../lambdadelta/basic_2/dynamic/nta.ma | 4 +- .../lambdadelta/basic_2/dynamic/nta_cpms.ma | 10 ++--- .../lambdadelta/basic_2/dynamic/nta_ind.ma | 2 +- .../basic_2/dynamic/nta_preserve.ma | 7 ++- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 8 +++- .../lambdadelta/ground_2/lib/arith_2b.ma | 4 ++ .../lambdadelta/ground_2/ynat/ynat_lt.ma | 8 ++++ 14 files changed, 80 insertions(+), 84 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma index 704301fe0..2b3dfcd4c 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_cnv_eta.ma @@ -20,10 +20,10 @@ include "basic_2/dynamic/cnv.ma". (* Extended validy (basic_2B) vs. restricted validity (basic_1A) ************) (* Note: extended validity of a closure, height of cnv_appl > 1 *) -lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 ![Ⓕ,h]. +lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0⦄ ⊢ ⓐ#2.#0 !*[h]. #h #p #G #L #s @(cnv_appl … 2 p … (⋆s) … (⋆s)) -[ #H destruct +[ // | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/ | /4 width=1 by cnv_bind, cnv_zero/ | /5 width=3 by cpm_cpms, cpm_lref, cpm_ell, lifts_sort/ @@ -32,15 +32,15 @@ lemma cnv_extended (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛ#0 qed. (* Note: restricted validity of the η-expanded closure, height of cnv_appl = 1 **) -lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![Ⓣ,h]. +lemma vnv_restricted (h) (p): ∀G,L,s. ⦃G, L.ⓛ⋆s.ⓛⓛ{p}⋆s.⋆s.ⓛⓛ{p}⋆s.ⓐ#0.#1⦄ ⊢ ⓐ#2.#0 ![h]. #h #p #G #L #s @(cnv_appl … 1 p … (⋆s) … (ⓐ#0.#2)) -[ /2 width=1 by/ +[ /2 width=1 by ylt_inj/ | /4 width=1 by cnv_sort, cnv_zero, cnv_lref/ | @cnv_zero @cnv_bind // @(cnv_appl … 1 p … (⋆s) … (⋆s)) - [ /2 width=1 by/ + [ /2 width=1 by ylt_inj/ | /2 width=1 by cnv_sort, cnv_zero/ | /4 width=1 by cnv_sort, cnv_zero, cnv_lref, cnv_bind/ | /2 width=3 by cpms_ell, lifts_sort/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma index 4db46f940..fe0b19cf3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_lt.ma". include "basic_2/notation/relations/exclaim_5.ma". include "basic_2/notation/relations/exclaim_4.ma". include "basic_2/notation/relations/exclaimstar_4.ma". @@ -21,12 +22,12 @@ include "basic_2/rt_computation/cpms.ma". (* activate genv *) (* Basic_2A1: uses: snv *) -inductive cnv (a) (h): relation3 genv lenv term ≝ +inductive cnv (a:ynat) (h): relation3 genv lenv term ≝ | cnv_sort: ∀G,L,s. cnv a h G L (⋆s) | cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0) | cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i) | cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T) -| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n ≤ 1) → cnv a h G L V → cnv a h G L T → +| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T → ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T) | cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T → ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → cnv a h G L (ⓝU.T) @@ -36,10 +37,10 @@ interpretation "context-sensitive native validity (term)" 'Exclaim a h G L T = (cnv a h G L T). interpretation "context-sensitive restricted native validity (term)" - 'Exclaim h G L T = (cnv true h G L T). + 'Exclaim h G L T = (cnv (yinj (S (S O))) h G L T). interpretation "context-sensitive extended native validity (term)" - 'ExclaimStar h G L T = (cnv false h G L T). + 'ExclaimStar h G L T = (cnv Y h G L T). (* Basic inversion lemmas ***************************************************) @@ -111,7 +112,7 @@ lemma cnv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] /2 width=4 by cnv_inv_bind_aux/ qed-. fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T → - ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. #a #h #G #L #X * -L -X [ #G #L #s #X1 #X2 #H destruct @@ -125,7 +126,7 @@ qed-. (* Basic_2A1: uses: snv_inv_appl *) lemma cnv_inv_appl (a) (h): ∀G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → - ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. /2 width=3 by cnv_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index cb2f97f55..c63a1aa12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -12,7 +12,9 @@ (* *) (**************************************************************************) +include "ground_2/lib/arith_2b.ma". include "basic_2/rt_computation/cpms_aaa.ma". +include "basic_2/rt_computation/lprs_cpms.ma". include "basic_2/dynamic/cnv.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) @@ -61,32 +63,19 @@ qed-. (* Advanced inversion lemmas ************************************************) -lemma cnv_inv_appl_SO (a) (h) (G) (L): - ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → - ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & - ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. -* #h #G #L #V #T #H -elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU -[ elim (cnv_fwd_aaa … HT) #A #HA - elim (aaa_cpm_SO h … (ⓛ{p}W.U)) - [|*: /2 width=8 by cpms_aaa_conf/ ] #X #HU0 - elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct - lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0 - lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0 - /2 width=7 by ex5_4_intro/ -| lapply (Ha ?) -Ha [ // ] #Ha - lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct - /2 width=7 by ex5_4_intro/ -| @(ex5_4_intro … HV HT HVW HTU) #H destruct -] -qed-. - -lemma cnv_inv_appl_true (h) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] → - ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] & - ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W0.U0. -#h #G #L #V #T #H -elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn ->Hn -n [| // ] #HV #HT #HVW #HTU +lemma cnv_inv_appl_pred (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![yinj a, h] → + ∃∃p,W0,U0. ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W0.U0. +#a #h #G #L #V #T #H +elim (cnv_inv_appl … H) -H #n #p #W #U #Ha #HV #HT #HVW #HTU +lapply (ylt_inv_inj … Ha) -Ha #Ha +elim (cnv_fwd_aaa … HT) #A #HA +elim (cpms_total_aaa h … (a-↑n) … (ⓛ{p}W.U)) +[|*: /2 width=8 by cpms_aaa_conf/ ] -HA #X #HU0 +elim (cpms_inv_abst_sn … HU0) #W0 #U0 #HW0 #_ #H destruct +lapply (cpms_trans … HVW … HW0) -HVW -HW0 #HVW0 +lapply (cpms_trans … HTU … HU0) -HTU -HU0 +>(arith_m2 … Ha) -Ha #HTU0 /2 width=5 by ex4_3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma index 3437d2629..e2eca5cdf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/cpms_cpms.ma". include "basic_2/rt_equivalence/cpes.ma". include "basic_2/dynamic/cnv_aaa.ma". @@ -21,7 +20,7 @@ include "basic_2/dynamic/cnv_aaa.ma". (* Properties with t-bound rt-equivalence for terms *************************) lemma cnv_appl_cpes (a) (h) (G) (L): - ∀n. (a = Ⓣ → n ≤ 1) → + ∀n. yinj n < a → ∀V. ⦃G, L⦄ ⊢ V ![a, h] → ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∀W. ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W → ∀p,U. ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U → ⦃G, L⦄ ⊢ ⓐV.T ![a, h]. @@ -39,30 +38,20 @@ qed. lemma cnv_inv_appl_cpes (a) (h) (G) (L): ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → - ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ∃∃n,p,W,U. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U. #a #h #G #L #V #T #H elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU /3 width=7 by cpms_div, ex5_4_intro/ qed-. -lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L): - ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → - ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & - ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U. +lemma cnv_inv_appl_pred_cpes (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![yinj a, h] → + ∃∃p,W,U. ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[↓a, h] ⓛ{p}W.U. #a #h #G #L #V #T #H -elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU -/3 width=7 by cpms_div, ex5_4_intro/ -qed-. - -lemma cnv_inv_appl_true_cpes (h) (G) (L): - ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] → - ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] & - ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U. -#h #G #L #V #T #H -elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn ->Hn -n [| // ] #HV #HT #HVW #HTU -/2 width=5 by ex4_3_intro/ +elim (cnv_inv_appl_pred … H) -H #p #W #U #HV #HT #HVW #HTU +/3 width=7 by cpms_div, ex4_3_intro/ qed-. lemma cnv_inv_cast_cpes (a) (h) (G) (L): @@ -82,7 +71,7 @@ lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term): (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] → Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T) ) → - (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] → + (∀n,p,G,L,V,W,T,U. yinj n < a → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] → ⦃G,L⦄ ⊢ V ⬌*[h,1,0]W → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W.U → Q G L V → Q G L T → Q G L (ⓐV.T) ) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma index c02e30077..d1f41252b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq.ma @@ -15,7 +15,6 @@ include "ground_2/xoa/ex_5_1.ma". include "ground_2/xoa/ex_9_3.ma". include "basic_2/rt_transition/cpm_tdeq.ma". -include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_computation/fpbg_fqup.ma". include "basic_2/dynamic/cnv_fsb.ma". @@ -76,7 +75,7 @@ qed-. lemma cpm_tdeq_inv_appl_sn (a) (h) (n) (G) (L): ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] → ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛ X → - ∃∃m,q,W,U1,T2. a = Ⓣ → m ≤ 1 & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 + ∃∃m,q,W,U1,T2. yinj m < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1 & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛ T2 & X = ⓐV.T2. #a #h #n #G #L #V #T1 #H0 #X #H1 #H2 elim (cpm_inv_appl1 … H1) -H1 * @@ -134,7 +133,7 @@ lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …): ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2) ) → - (∀m. (a = Ⓣ → m ≤ 1) → + (∀m. yinj m < a → ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G, L⦄ ⊢ V ➡*[1,h] W → ∀p,T1,U1. ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma index 8e2781a6b..8c720f4ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -69,7 +69,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h): lapply (cpms_trans … HXV2 … HXW1) -XW1 Stage "B" + + Parametrized applicability condition + allows λδ-2B to generalize both λδ-1A and λδ-1B. + - Extended (λδ-2) and restricted (λδ-1) validity is decidable + Extended (λδ-2A) and restricted (λδ-1A) validity is decidable (anniversary milestone). @@ -37,7 +41,7 @@ (i.e. no induction on the degree). - Extended (λδ-2) and restricted (λδ-1) type rules justified. + Extended (λδ-2A) and restricted (λδ-1A) type rules justified. λδ-2A completed with diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma index c6203acd4..5729f64cf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith_2b.ma @@ -42,3 +42,7 @@ qed. lemma arith_l1: ∀x. 1 = 1-x+(x-(x-1)). #x minus_minus [|*: // ]