From 647b419e96770d90a82d7a9e5e8843566a9f93ee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 15 Jun 2019 15:19:59 +0200 Subject: [PATCH] updating the structures for sorts + strict monotonicity is now an optional property + new optional properties: acyclicity and decidability + "next" now has a specific notation + refactored sort degree is now based on acyclicity and decidability --- .../basic_2/dynamic/cnv_cpm_conf.ma | 2 +- .../basic_2/dynamic/cnv_cpm_tdeq.ma | 2 +- .../basic_2/dynamic/cnv_cpm_tdeq_conf.ma | 2 +- .../lambdadelta/basic_2/dynamic/nta.ma | 2 +- .../lambdadelta/basic_2/dynamic/nta_cpcs.ma | 2 +- .../lambdadelta/basic_2/dynamic/nta_ind.ma | 6 +- .../lambdadelta/basic_2/rt_transition/cpg.ma | 10 +- .../basic_2/rt_transition/cpg_drops.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpm.ma | 6 +- .../basic_2/rt_transition/cpm_drops.ma | 2 +- .../basic_2/rt_transition/cpm_tdeq.ma | 2 +- .../lambdadelta/basic_2/rt_transition/cpx.ma | 8 +- .../basic_2/rt_transition/cpx_drops.ma | 2 +- .../lambdadelta/static_2/etc/sh_lt.etc | 4 - .../lambdadelta/static_2/syntax/sd.ma | 118 +++++------------- .../lambdadelta/static_2/syntax/sd_d.ma | 99 +++++++++++++++ .../lambdadelta/static_2/syntax/sd_lt.ma | 32 +++++ .../lambdadelta/static_2/syntax/sh_lt.ma | 15 ++- .../lambdadelta/static_2/syntax/sh_props.ma | 29 +++++ .../lambdadelta/static_2/web/static_2_src.tbl | 6 +- 20 files changed, 230 insertions(+), 121 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma create mode 100644 matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma index 141a733c2..c10e470dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma @@ -28,7 +28,7 @@ fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I): /2 width=3 by ex2_intro/ qed-. fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s): - ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡*[h] T. + ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(⫯[h]s) ➡*[h] T. /3 width=3 by cpm_cpms, ex2_intro/ qed-. fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i): 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 c10cdba20..e3057788c 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 @@ -128,7 +128,7 @@ qed-. lemma cpm_tdeq_ind (a) (h) (n) (G) (Q:relation3 …): (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) → - (∀L,s. n = 1 → Q L (⋆s) (⋆(next h s))) → + (∀L,s. n = 1 → Q L (⋆s) (⋆(⫯[h]s))) → (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T1![a,h] → ∀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) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma index 3dbea60d6..752d02d11 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_tdeq_conf.ma @@ -33,7 +33,7 @@ fact cnv_cpm_tdeq_conf_lpr_atom_atom_aux (h) (G0) (L1) (L2) (I): qed-. fact cnv_cpm_tdeq_conf_lpr_atom_ess_aux (h) (G0) (L1) (L2) (s): - ∃∃T. ⦃G0,L1⦄ ⊢ ⋆s ➡[1,h] T & ⋆s ≛ T & ⦃G0,L2⦄ ⊢ ⋆(next h s) ➡[h] T & ⋆(next h s) ≛ T. + ∃∃T. ⦃G0,L1⦄ ⊢ ⋆s ➡[1,h] T & ⋆s ≛ T & ⦃G0,L2⦄ ⊢ ⋆(⫯[h]s) ➡[h] T & ⋆(⫯[h]s) ≛ T. #h #G0 #L1 #L2 #s /3 width=5 by tdeq_sort, ex4_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma index 66ddc0d99..84bbfeda9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma @@ -35,7 +35,7 @@ interpretation "extended native type assignment (term)" (* Basic_1: was by definition: ty3_sort *) (* Basic_2A1: was by definition: nta_sort ntaa_sort *) -lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(next h s). +lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(⫯[h]s). #a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/ qed. 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 100d6317b..d4aec09f3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma @@ -45,7 +45,7 @@ qed-. (* 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 & ⦃G,L⦄ ⊢ X2 ![a,h]. + ∧∧ ⦃G,L⦄ ⊢ ⋆(⫯[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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma index d459d184a..89565cde7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma @@ -22,7 +22,7 @@ include "basic_2/dynamic/nta_preserve.ma". (* Advanced eliminators *****************************************************) lemma nta_ind_rest_cnv (h) (Q:relation4 …): - (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀G,L,s. Q G L (⋆s) (⋆(⫯[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 @@ -79,7 +79,7 @@ lemma nta_ind_rest_cnv (h) (Q:relation4 …): qed-. lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …): - (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀G,L,s. Q G L (⋆s) (⋆(⫯[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 @@ -144,7 +144,7 @@ lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …): qed-. lemma nta_ind_ext_cnv (h) (Q:relation4 …): - (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀G,L,s. Q G L (⋆s) (⋆(⫯[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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index 6d36b466c..72656dd1a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -15,7 +15,7 @@ include "ground_2/steps/rtc_max.ma". include "ground_2/steps/rtc_plus.ma". include "basic_2/notation/relations/predty_7.ma". -include "static_2/syntax/sort.ma". +include "static_2/syntax/sh.ma". include "static_2/syntax/lenv.ma". include "static_2/syntax/genv.ma". include "static_2/relocation/lifts.ma". @@ -25,7 +25,7 @@ include "static_2/relocation/lifts.ma". (* avtivate genv *) inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝ | cpg_atom : ∀I,G,L. cpg Rt h (𝟘𝟘) G L (⓪{I}) (⓪{I}) -| cpg_ess : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(next h s)) +| cpg_ess : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(⫯[h]s)) | cpg_delta: ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 → ⬆*[1] V2 ≘ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2 | cpg_ell : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 → @@ -70,7 +70,7 @@ qed. fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈[Rt,c,h] T2 → ∀J. T1 = ⓪{J} → ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 - | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙 + | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙 | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 & @@ -96,7 +96,7 @@ qed-. lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 → ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 - | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙 + | ∃∃s. J = Sort s & T2 = ⋆(⫯[h]s) & c = 𝟘𝟙 | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV | ∃∃cV,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⬆*[1] V2 ≘ T2 & @@ -106,7 +106,7 @@ lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[Rt,c,h] T2 → /2 width=3 by cpg_inv_atom1_aux/ qed-. lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G,L⦄ ⊢ ⋆s ⬈[Rt,c,h] T2 → - ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(next h s) ∧ c = 𝟘𝟙. + ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(⫯[h]s) ∧ c = 𝟘𝟙. #Rt #c #h #G #L #T2 #s #H elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/ [ #s0 #H destruct /3 width=1 by or_intror, conj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 71d38a1ba..977ec175d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -63,7 +63,7 @@ qed-. lemma cpg_inv_atom1_drops: ∀Rt,c,h,I,G,L,T2. ⦃G,L⦄ ⊢ ⓪{I} ⬈[Rt,c,h] T2 → ∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘 - | ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙 + | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s & c = 𝟘𝟙 | ∃∃cV,i,K,V,V2. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ⬈[Rt,cV,h] V2 & ⬆*[↑i] V2 ≘ T2 & I = LRef i & c = cV | ∃∃cV,i,K,V,V2. ⬇*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ⬈[Rt,cV,h] V2 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index c8f746351..db5bdfe78 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -32,7 +32,7 @@ interpretation (* Basic properties *********************************************************) -lemma cpm_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ➡[1,h] ⋆(next h s). +lemma cpm_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ➡[1,h] ⋆(⫯[h]s). /2 width=3 by cpg_ess, ex2_intro/ qed. lemma cpm_delta: ∀n,h,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 → @@ -131,7 +131,7 @@ qed. lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ➡[n,h] T2 → ∨∨ T2 = ⓪{J} ∧ n = 0 - | ∃∃s. T2 = ⋆(next h s) & J = Sort s & n = 1 + | ∃∃s. T2 = ⋆(⫯[h]s) & J = Sort s & n = 1 | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓓV1 & J = LRef 0 | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ➡[m,h] V2 & ⬆*[1] V2 ≘ T2 & @@ -304,7 +304,7 @@ qed-. lemma cpm_ind (h): ∀Q:relation5 nat genv lenv term term. (∀I,G,L. Q 0 G L (⓪{I}) (⓪{I})) → - (∀G,L,s. Q 1 G L (⋆s) (⋆(next h s))) → + (∀G,L,s. Q 1 G L (⋆s) (⋆(⫯[h]s))) → (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 → Q n G K V1 V2 → ⬆*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2 ) → (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 → Q n G K V1 V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma index b6298c766..bc9463c95 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -67,7 +67,7 @@ qed. lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G,L⦄ ⊢ ⓪{I} ➡[n,h] T2 → ∨∨ T2 = ⓪{I} ∧ n = 0 - | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1 + | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s & n = 1 | ∃∃K,V,V2,i. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V ➡[n,h] V2 & ⬆*[↑i] V2 ≘ T2 & I = LRef i | ∃∃m,K,V,V2,i. ⬇*[i] L ≘ K.ⓛV & ⦃G,K⦄ ⊢ V ➡[m,h] V2 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma index b99c4309c..7f05e3b1c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_tdeq.ma @@ -32,7 +32,7 @@ qed-. lemma cpm_tdeq_inv_atom_sn (n) (h) (I) (G) (L): ∀X. ⦃G,L⦄ ⊢ ⓪{I} ➡[n,h] X → ⓪{I} ≛ X → ∨∨ ∧∧ X = ⓪{I} & n = 0 - | ∃∃s. X = ⋆(next h s) & I = Sort s & n = 1. + | ∃∃s. X = ⋆(⫯[h]s) & I = Sort s & n = 1. #n #h * #s #G #L #X #H1 #H2 [ elim (cpm_inv_sort1 … H1) -H1 cases n -n [| #n ] #H #Hn destruct -H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index e92d469a4..005c43355 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -27,7 +27,7 @@ interpretation (* Basic properties *********************************************************) (* Basic_2A1: was: cpx_st *) -lemma cpx_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ⬈[h] ⋆(next h s). +lemma cpx_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ⬈[h] ⋆(⫯[h]s). /2 width=2 by cpg_ess, ex_intro/ qed. lemma cpx_delta: ∀h,I,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ⬈[h] V2 → @@ -110,7 +110,7 @@ qed. lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[h] T2 → ∨∨ T2 = ⓪{J} - | ∃∃s. T2 = ⋆(next h s) & J = Sort s + | ∃∃s. T2 = ⋆(⫯[h]s) & J = Sort s | ∃∃I,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≘ T2 & L = K.ⓑ{I}V1 & J = LRef 0 | ∃∃I,K,T,i. ⦃G,K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≘ T2 & @@ -120,7 +120,7 @@ lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ⬈[h] T2 → qed-. lemma cpx_inv_sort1: ∀h,G,L,T2,s. ⦃G,L⦄ ⊢ ⋆s ⬈[h] T2 → - ∨∨ T2 = ⋆s | T2 = ⋆(next h s). + ∨∨ T2 = ⋆s | T2 = ⋆(⫯[h]s). #h #G #L #T2 #s * #c #H elim (cpg_inv_sort1 … H) -H * /2 width=1 by or_introl, or_intror/ qed-. @@ -240,7 +240,7 @@ qed-. lemma cpx_ind: ∀h. ∀Q:relation4 genv lenv term term. (∀I,G,L. Q G L (⓪{I}) (⓪{I})) → - (∀G,L,s. Q G L (⋆s) (⋆(next h s))) → + (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) → (∀I,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 → ⬆*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2 ) → (∀I,G,K,T,U,i. ⦃G,K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma index 9f1350864..500929b1d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma @@ -32,7 +32,7 @@ qed. (* Basic_2A1: was: cpx_inv_atom1 *) lemma cpx_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G,L⦄ ⊢ ⓪{I} ⬈[h] T2 → ∨∨ T2 = ⓪{I} - | ∃∃s. T2 = ⋆(next h s) & I = Sort s + | ∃∃s. T2 = ⋆(⫯[h]s) & I = Sort s | ∃∃J,K,V,V2,i. ⬇*[i] L ≘ K.ⓑ{J}V & ⦃G,K⦄ ⊢ V ⬈[h] V2 & ⬆*[↑i] V2 ≘ T2 & I = LRef i. #h #I #G #L #T2 * #c #H elim (cpg_inv_atom1_drops … H) -H * diff --git a/matita/matita/contribs/lambdadelta/static_2/etc/sh_lt.etc b/matita/matita/contribs/lambdadelta/static_2/etc/sh_lt.etc index 89eb9dde5..c623e79a6 100644 --- a/matita/matita/contribs/lambdadelta/static_2/etc/sh_lt.etc +++ b/matita/matita/contribs/lambdadelta/static_2/etc/sh_lt.etc @@ -1,6 +1,2 @@ definition sh_N: sh ≝ mk_sh S …. // defined. - -axiom nexts_dec: ∀h,s1,s2. Decidable (∃n. (next h)^n s1 = s2). - -axiom nexts_inj: ∀h,s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma index 8a9ae7183..533a79e05 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd.ma @@ -12,113 +12,57 @@ (* *) (**************************************************************************) -include "static_2/syntax/item_sh.ma". +include "static_2/syntax/sh.ma". (* SORT DEGREE **************************************************************) (* sort degree specification *) -record sd (h:sh): Type[0] ≝ { - deg : relation nat; (* degree of the sort *) - deg_total: ∀s. ∃d. deg s d; (* functional relation axioms *) - deg_mono : ∀s,d1,d2. deg s d1 → deg s d2 → d1 = d2; - deg_next : ∀s,d. deg s d → deg (next h s) (↓d) (* compatibility condition *) +record sd: Type[0] ≝ { +(* degree of the sort *) + deg: relation nat +}. + +(* sort degree postulates *) +record sd_props (h) (o): Prop ≝ { +(* functional relation axioms *) + deg_total: ∀s. ∃d. deg o s d; + deg_mono : ∀s,d1,d2. deg o s d1 → deg o s d2 → d1 = d2; +(* compatibility condition *) + deg_next : ∀s,d. deg o s d → deg o (⫯[h]s) (↓d) }. (* Notable specifications ***************************************************) definition deg_O: relation nat ≝ λs,d. d = 0. -definition sd_O: ∀h. sd h ≝ λh. mk_sd h deg_O …. -/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ defined. - -(* Basic_2A1: includes: deg_SO_pos *) -inductive deg_SO (h:sh) (s:nat) (s0:nat): predicate nat ≝ -| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n) -| deg_SO_zero: ((∃n. (next h)^n s0 = s) → ⊥) → deg_SO h s s0 0 -. - -fact deg_SO_inv_succ_aux: ∀h,s,s0,n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → - (next h)^n s0 = s. -#h #s #s0 #n0 * -n0 -[ #n #Hn #x #H destruct // -| #_ #x #H destruct -] -qed-. - -(* Basic_2A1: was: deg_SO_inv_pos *) -lemma deg_SO_inv_succ: ∀h,s,s0,n. deg_SO h s s0 (↑n) → (next h)^n s0 = s. -/2 width=3 by deg_SO_inv_succ_aux/ qed-. - -lemma deg_SO_refl: ∀h,s. deg_SO h s s 1. -#h #s @(deg_SO_succ … 0 ?) // -qed. - -lemma deg_SO_gt: ∀h,s1,s2. s1 < s2 → deg_SO h s1 s2 0. -#h #s1 #s2 #HK12 @deg_SO_zero * #n elim n -n normalize -[ #H destruct - elim (lt_refl_false … HK12) -| #n #_ #H - lapply (next_lt h ((next h)^n s2)) >H -H #H - lapply (transitive_lt … H HK12) -s1 #H1 - lapply (nexts_le h s2 n) #H2 - lapply (le_to_lt_to_lt … H2 H1) -h -n #H - elim (lt_refl_false … H) -] -qed. - -definition sd_SO: ∀h. nat → sd h ≝ λh,s. mk_sd h (deg_SO h s) …. -[ #s0 - lapply (nexts_dec h s0 s) * - [ * /3 width=2 by deg_SO_succ, ex_intro/ | /4 width=2 by deg_SO_zero, ex_intro/ ] -| #K0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2 // - [ < H2 in H1; -H2 #H - lapply (nexts_inj … H) -H #H destruct // - | elim H1 /2 width=2 by ex_intro/ - | elim H2 /2 width=2 by ex_intro/ - ] -| #s0 #n * - [ #d #H destruct elim d -d normalize - /2 width=1 by deg_SO_gt, deg_SO_succ, next_lt/ - | #H1 @deg_SO_zero * #d #H2 destruct - @H1 -H1 @(ex_intro … (↑d)) /2 width=1 by sym_eq/ (**) (* explicit constructor *) - ] -] -defined. +definition sd_O: sd ≝ mk_sd deg_O. -rec definition sd_d (h:sh) (s:nat) (d:nat) on d : sd h ≝ - match d with - [ O ⇒ sd_O h - | S d ⇒ match d with - [ O ⇒ sd_SO h s - | _ ⇒ sd_d h (next h s) d - ] - ]. +lemma sd_O_props (h): sd_props h sd_O ≝ mk_sd_props …. +/2 width=2 by le_n_O_to_eq, le_n, ex_intro/ qed. (* Basic inversion lemmas ***************************************************) -lemma deg_inv_pred: ∀h,o,s,d. deg h o (next h s) (↑d) → deg h o s (↑↑d). -#h #o #s #d #H1 -elim (deg_total h o s) #n #H0 -lapply (deg_next … H0) #H2 -lapply (deg_mono … H1 H2) -H1 -H2 #H >H >S_pred /2 width=2 by ltn_to_ltO/ +lemma deg_inv_pred (h) (o): sd_props h o → + ∀s,d. deg o (⫯[h]s) (↑d) → deg o s (↑↑d). +#h #o #Ho #s #d #H1 +elim (deg_total … Ho s) #d0 #H0 +lapply (deg_next … Ho … H0) #H2 +lapply (deg_mono … Ho … H1 H2) -H1 -H2 #H >H >S_pred +/2 width=2 by ltn_to_ltO/ qed-. -lemma deg_inv_prec: ∀h,o,s,n,d. deg h o ((next h)^n s) (↑d) → deg h o s (↑(d+n)). -#h #o #s #n elim n -n normalize /3 width=1 by deg_inv_pred/ +lemma deg_inv_prec (h) (o): sd_props h o → + ∀s,n,d. deg o ((next h)^n s) (↑d) → deg o s (↑(d+n)). +#h #o #H0 #s #n elim n -n normalize /3 width=3 by deg_inv_pred/ qed-. (* Basic properties *********************************************************) -lemma deg_iter: ∀h,o,s,d,n. deg h o s d → deg h o ((next h)^n s) (d-n). -#h #o #s #d #n elim n -n normalize /3 width=1 by deg_next/ +lemma deg_iter (h) (o): sd_props h o → + ∀s,d,n. deg o s d → deg o ((next h)^n s) (d-n). +#h #o #Ho #s #d #n elim n -n normalize /3 width=1 by deg_next/ qed. -lemma deg_next_SO: ∀h,o,s,d. deg h o s (↑d) → deg h o (next h s) d. +lemma deg_next_SO (h) (o): sd_props h o → + ∀s,d. deg o s (↑d) → deg o (next h s) d. /2 width=1 by deg_next/ qed-. - -lemma sd_d_SS: ∀h,s,d. sd_d h s (↑↑d) = sd_d h (next h s) (↑d). -// qed. - -lemma sd_d_correct: ∀h,d,s. deg h (sd_d h s d) s d. -#h #d elim d -d // #d elim d -d /3 width=1 by deg_inv_pred/ -qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma new file mode 100644 index 000000000..56c80d69e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_d.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/pull/pull_2.ma". +include "static_2/syntax/sh_props.ma". +include "static_2/syntax/sd.ma". + +(* SORT DEGREE **************************************************************) + +(* Basic_2A1: includes: deg_SO_pos *) +inductive deg_SO (h) (s) (s0): predicate nat ≝ +| deg_SO_succ : ∀n. (next h)^n s0 = s → deg_SO h s s0 (↑n) +| deg_SO_zero: (∀n. (next h)^n s0 = s → ⊥) → deg_SO h s s0 0 +. + +fact deg_SO_inv_succ_aux (h) (s) (s0): + ∀n0. deg_SO h s s0 n0 → ∀n. n0 = ↑n → (next h)^n s0 = s. +#h #s #s0 #n0 * -n0 +[ #n #Hn #x #H destruct // +| #_ #x #H destruct +] +qed-. + +(* Basic_2A1: was: deg_SO_inv_pos *) +lemma deg_SO_inv_succ (h) (s) (s0): + ∀n. deg_SO h s s0 (↑n) → (next h)^n s0 = s. +/2 width=3 by deg_SO_inv_succ_aux/ qed-. + +lemma deg_SO_refl (h) (s): deg_SO h s s 1. +#h #s @(deg_SO_succ … 0 ?) // +qed. + +definition sd_SO (h) (s): sd ≝ mk_sd (deg_SO h s). + +lemma sd_SO_props (h) (s): sh_decidable h → sh_acyclic h → + sd_props h (sd_SO h s). +#h #s #Hhd #Hha +@mk_sd_props +[ #s0 + elim (nexts_dec … Hhd s0 s) -Hhd + [ * /3 width=2 by deg_SO_succ, ex_intro/ + | /5 width=2 by deg_SO_zero, ex_intro/ + ] +| #s0 #d1 #d2 * [ #n1 ] #H1 * [1,3: #n2 ] #H2 + [ < H2 in H1; -H2 #H + lapply (nexts_inj … Hha … H) -H #H destruct // + | elim H1 /2 width=2 by ex_intro/ + | elim H2 /2 width=2 by ex_intro/ + | // + ] +| #s0 #d * + [ #n #H destruct cases n -n normalize + [ @deg_SO_zero #n >iter_n_Sm #H + lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct + | #n @deg_SO_succ >iter_n_Sm // + ] + | #H0 @deg_SO_zero #n >iter_n_Sm #H destruct + /2 width=2 by/ + ] +] +qed. + +rec definition sd_d (h:?) (s:?) (d:?) on d: sd ≝ + match d with + [ O ⇒ sd_O + | S d ⇒ match d with + [ O ⇒ sd_SO h s + | _ ⇒ sd_d h (next h s) d + ] + ]. + +lemma sd_d_props (h) (s) (d): sh_decidable h → sh_acyclic h → + sd_props h (sd_d h s d). +#h @pull_2 * [ // ] +#d elim d -d /2 width=1 by sd_SO_props/ +qed. + +(* Properties with sd_d *****************************************************) + +lemma sd_d_SS (h): + ∀s,d. sd_d h s (↑↑d) = sd_d h (⫯[h]s) (↑d). +// qed. + +lemma sd_d_correct (h): sh_decidable h → sh_acyclic h → + ∀s,d. deg (sd_d h s d) s d. +#h #Hhd #Hha @pull_2 #d elim d -d [ // ] +#d elim d -d /3 width=3 by deg_inv_pred, sd_d_props/ +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma new file mode 100644 index 000000000..238d1a28b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sd_lt.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/sh_lt.ma". +include "static_2/syntax/sd_d.ma". + +(* SORT DEGREE **************************************************************) + +(* Properties with sh_lt ****************************************************) + +lemma deg_SO_gt (h): sh_lt h → + ∀s1,s2. s1 < s2 → deg_SO h s1 s2 0. +#h #Hh #s1 #s2 #Hs12 @deg_SO_zero * normalize +[ #H destruct + elim (lt_refl_false … Hs12) +| #n #H + lapply (next_lt … Hh ((next h)^n s2)) >H -H #H + lapply (transitive_lt … H Hs12) -s1 #H1 + /3 width=5 by lt_le_false, nexts_le/ (* full auto too slow *) +] +qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma index 459d4d16b..494436476 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_lt.ma @@ -12,25 +12,30 @@ (* *) (**************************************************************************) -include "static_2/syntax/sort.ma". +include "static_2/syntax/sh_props.ma". (* SORT HIERARCHY ***********************************************************) -record is_lt (h): Prop ≝ +(* strict monotonicity condition *) +record sh_lt (h): Prop ≝ { - next_lt: ∀s. s < ⫯[h]s (* strict monotonicity condition *) + next_lt: ∀s. s < ⫯[h]s }. (* Basic properties *********************************************************) -lemma nexts_le (h): is_lt h → ∀s,n. s ≤ (next h)^n s. +lemma nexts_le (h): sh_lt h → ∀s,n. s ≤ (next h)^n s. #h #Hh #s #n elim n -n [ // ] normalize #n #IH lapply (next_lt … Hh ((next h)^n s)) #H lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/ qed. -lemma nexts_lt (h): is_lt h → ∀s,n. s < (next h)^(↑n) s. +lemma nexts_lt (h): sh_lt h → ∀s,n. s < (next h)^(↑n) s. #h #Hh #s #n normalize lapply (nexts_le … Hh s n) #H @(le_to_lt_to_lt … H) /2 width=1 by next_lt/ qed. + +axiom sh_lt_dec (h): sh_lt h → sh_decidable h. + +axiom sh_lt_acyclic (h): sh_lt h → sh_acyclic h. diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma new file mode 100644 index 000000000..4302026d4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/sh_props.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/sh.ma". + +(* SORT HIERARCHY ***********************************************************) + +(* acyclicity condition *) +record sh_acyclic (h): Prop ≝ +{ + nexts_inj: ∀s,n1,n2. (next h)^n1 s = (next h)^n2 s → n1 = n2 +}. + +(* decidability condition *) +record sh_decidable (h): Prop ≝ +{ + nexts_dec: ∀s1,s2. Decidable (∃n. (next h)^n s1 = s2) +}. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index fed1803e1..723104f7b 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -156,10 +156,14 @@ table { } ] [ { "items" * } { - [ [ "" ] "item_sh" * ] [ [ "" ] "item" * ] } ] + [ { "sorts" * } { + [ [ "degree" ] "sd" "sd_d" + "sd_lt" * ] + [ [ "hierarchy" ] "sh" + "( ⫯[?]? )" "sh_props" + "sh_lt" * ] + } + ] [ { "atomic arities" * } { [ [ "" ] "aarity" * ] } -- 2.39.2