From: Ferruccio Guidi Date: Mon, 24 Apr 2017 15:07:30 +0000 (+0000) Subject: some improvements before setting up the exclusion binder X-Git-Tag: make_still_working~454 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=73966e3e9fd17155ca67e6b4a32f52225cea9d3c some improvements before setting up the exclusion binder --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index fbf3612a6..c6ba0e03d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -47,6 +47,7 @@ a: application b: generic binder with one argument d: abbreviation f: generic flat with one argument +i: generic binder for local environments l: typed abstraction n: native type annotation u: generic binder with zero argument diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma index 5f6319bd2..57b921a88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabbr_2.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . break ⓓ T1 )" - left associative with precedence 49 + left associative with precedence 50 for @{ 'DxAbbr $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma index b3d909641..d9b504ce3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxabst_2.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . break ⓛ T1 )" - left associative with precedence 50 + left associative with precedence 51 for @{ 'DxAbst $L $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma index e4f48e77c..023e50eb4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind1_2.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . break ⓤ { term 46 I } )" - non associative with precedence 46 + non associative with precedence 47 for @{ 'DxBind1 $L $I }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma index fc371c285..2deb5e842 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxbind2_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L . break ⓑ { term 46 I } break term 48 T1 )" - non associative with precedence 47 +notation "hvbox( L . break ⓑ { term 46 I } break term 49 T1 )" + non associative with precedence 48 for @{ 'DxBind2 $L $I $T1 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma new file mode 100644 index 000000000..51e9522f6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxitem_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L . ⓘ { break term 46 I } )" + non associative with precedence 46 + for @{'DxItem $L $I }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma index 34ad27e9f..96f543c2b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/dxvoid_1.ma @@ -15,5 +15,5 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) notation "hvbox( L . ⓧ )" - non associative with precedence 48 + non associative with precedence 49 for @{ 'DxVoid $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma new file mode 100644 index 000000000..000993bf0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snitem_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⓘ { term 46 I } . break term 55 L )" + non associative with precedence 55 + for @{ 'SnItem $I $L }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma index f78ecb55c..61483a73d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma @@ -13,7 +13,9 @@ (**************************************************************************) include "ground_2/notation/functions/append_2.ma". +include "basic_2/notation/functions/snbind1_2.ma". include "basic_2/notation/functions/snbind2_3.ma". +include "basic_2/notation/functions/snvoid_1.ma". include "basic_2/notation/functions/snabbr_2.ma". include "basic_2/notation/functions/snabst_2.ma". include "basic_2/syntax/lenv.ma". @@ -26,10 +28,16 @@ rec definition append L K on K ≝ match K with ]. interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). - +(* +interpretation "local environment tail binding construction (unary)" + 'SnBind1 I L = (append (LUnit LAtom I) L). +*) interpretation "local environment tail binding construction (binary)" 'SnBind2 I T L = (append (LPair LAtom I T) L). - +(* +interpretation "tail exclusion (local environment)" + 'SnVoid L = (append (LUnit LAtom Void) L). +*) interpretation "tail abbreviation (local environment)" 'SnAbbr T L = (append (LPair LAtom Abbr T) L). @@ -67,3 +75,10 @@ lemma append_inj_sn: ∀K,L1,L2. L1@@K = L2@@K → L1 = L2. #K #I #V #IH #L1 #L2 >append_pair #H elim (destruct_lpair_lpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *) qed-. + +(* Basic_1: uses: chead_ctail *) +(* Basic_2A1: uses: lpair_ltail *) +lemma lenv_case_tail: ∀L. L = ⋆ ∨ ∃∃K,I,V. L = ⓑ{I}V.K. +#L elim L -L /2 width=1 by or_introl/ +#L #I #V * [2: * ] /3 width=4 by ex1_3_intro, or_intror/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma index cab2cb810..2743241ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma @@ -28,28 +28,22 @@ lemma ltail_length: ∀I,L,V. |ⓑ{I}V.L| = ⫯|L|. #I #L #V >append_length // qed. -(* Basic_1: was just: chead_ctail *) -lemma lpair_ltail: ∀L,I,V. ∃∃J,K,W. L.ⓑ{I}V = ⓑ{J}W.K & |L| = |K|. -#L elim L -L /2 width=5 by ex2_3_intro/ -#L #Z #X #IHL #I #V elim (IHL Z X) -IHL -#J #K #W #H #_ >H -H >ltail_length -@(ex2_3_intro … J (K.ⓑ{I}V) W) /2 width=1 by length_pair/ -qed-. - (* Advanced inversion lemmas on length for local environments ***************) (* Basic_2A1: was: length_inv_pos_dx_ltail *) lemma length_inv_succ_dx_ltail: ∀L,l. |L| = ⫯l → ∃∃I,K,V. |K| = l & L = ⓑ{I}V.K. #Y #l #H elim (length_inv_succ_dx … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +elim (lenv_case_tail … L) [2: * #K #J #W ] +#H destruct /2 width=5 by ex2_3_intro/ qed-. (* Basic_2A1: was: length_inv_pos_sn_ltail *) lemma length_inv_succ_sn_ltail: ∀L,l. ⫯l = |L| → ∃∃I,K,V. l = |K| & L = ⓑ{I}V.K. #Y #l #H elim (length_inv_succ_sn … H) -H #I #L #V #Hl #HLK destruct -elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ +elim (lenv_case_tail … L) [2: * #K #J #W ] +#H destruct /2 width=5 by ex2_3_intro/ qed-. (* Inversion lemmas with length for local environments **********************) @@ -108,9 +102,11 @@ qed-. (* Basic eliminators ********************************************************) (* Basic_1: was: c_tail_ind *) -lemma lenv_ind_alt: ∀R:predicate lenv. - R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → - ∀L. R L. -#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1 -#L #I #V #H destruct elim (lpair_ltail L I V) /4 width=1 by/ +(* Basic_2A1: was: lenv_ind_alt *) +lemma lenv_ind_tail: ∀R:predicate lenv. + R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) → ∀L. R L. +#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // +#L #I #V -IH1 #H destruct +elim (lenv_case_tail … L) [2: * #K #J #W ] +#H destruct /3 width=1 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma new file mode 100644 index 000000000..ca474406d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind.ma @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/term.ma". + +(* BINDERS FOR LOCAL ENVIRONMENTS ******************************************) + +inductive bind: Type[0] ≝ +| BUnit: bind1 → bind +| BPair: bind2 → term → bind +. + +(* Basic properties ********************************************************) + +lemma eq_bind_dec: ∀I1,I2:bind. Decidable (I1 = I2). +* #I1 [2: #V1 ] * #I2 [2,4: #V2 ] +[ elim (eq_bind2_dec I1 I2) #HI + [ elim (eq_term_dec V1 V2) #HV /2 width=1 by or_introl/ ] + @or_intror #H destruct /2 width=1 by/ +| @or_intror #H destruct +| @or_intror #H destruct +| elim (eq_bind1_dec I1 I2) #HI /2 width=1 by or_introl/ + @or_intror #H destruct /2 width=1 by/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma new file mode 100644 index 000000000..2dda071d3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/bind_weight.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/term.ma". + +(* BINDERS FOR LOCAL ENVIRONMENTS ******************************************) + +include "basic_2/syntax/term_weight.ma". +include "basic_2/syntax/bind.ma". + +(* WEIGHT OF A BINDER FOR LOCAL ENVIRONMENTS *******************************) + +rec definition bw I ≝ match I with +[ BUnit _ ⇒ 1 +| BPair _ V ⇒ ♯{V} +]. + +interpretation "weight (binder for local environments)" 'Weight I = (bw I). + +(* Basic properties *********************************************************) + +lemma bw_pos: ∀I. 1 ≤ ♯{I}. +* // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_restricted_weight.ma index 32fd77331..467d3f1b7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_restricted_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_restricted_weight.ma @@ -27,7 +27,11 @@ interpretation "weight (restricted closure)" 'Weight L T = (rfw L T). lemma rfw_shift: ∀p,I,K,V,T. ♯{K.ⓑ{I}V, T} < ♯{K, ⓑ{p,I}V.T}. normalize /2 width=1 by monotonic_le_plus_r/ qed. - +(* +lemma rfw_clear: ∀p,I1,I2,K,V,T. ♯{K.ⓤ{I1}, T} < ♯{K, ⓑ{p,I2}V.T}. +normalize /4 width=1 by monotonic_le_plus_r, le_S_S/ +qed. +*) lemma rfw_tpair_sn: ∀I,L,V,T. ♯{L, V} < ♯{L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?%%); // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_weight.ma index b93368814..f2e896ad4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/cl_weight.ma @@ -29,7 +29,11 @@ interpretation "weight (closure)" 'Weight G L T = (fw G L T). lemma fw_shift: ∀p,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{p,I}V.T}. normalize /2 width=1 by monotonic_le_plus_r/ qed. - +(* +lemma fw_clear: ∀p,I1,I2,G,K,V,T. ♯{G, K.ⓤ{I1}, T} < ♯{G, K, ⓑ{p,I2}V.T}. +normalize /4 width=1 by monotonic_le_plus_r, le_S_S/ +qed. +*) lemma fw_tpair_sn: ∀I,G,L,V,T. ♯{G, L, V} < ♯{G, L, ②{I}V.T}. normalize in ⊢ (?→?→?→?→?→?%%); // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma index ab861be57..bb9451320 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma @@ -24,6 +24,11 @@ inductive item0: Type[0] ≝ | GRef: nat → item0 (* reference by position: starting at 0 *) . +(* binary binding items *) +inductive bind1: Type[0] ≝ + | Void: bind1 (* exclusion *) +. + (* binary binding items *) inductive bind2: Type[0] ≝ | Abbr: bind2 (* abbreviation *) @@ -56,6 +61,10 @@ lemma eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2). #Hni12 @or_intror #H destruct /2 width=1 by/ qed-. +lemma eq_bind1_dec: ∀I1,I2:bind1. Decidable (I1 = I2). +* * /2 width=1 by or_introl/ +qed-. + (* Basic_1: was: bind_dec *) lemma eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2). * * /2 width=1 by or_introl/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma index 05b8fde62..7b6bc80eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma @@ -13,10 +13,13 @@ (**************************************************************************) include "basic_2/notation/constructors/star_0.ma". +include "basic_2/notation/constructors/dxitem_2.ma". +include "basic_2/notation/constructors/dxbind1_2.ma". include "basic_2/notation/constructors/dxbind2_3.ma". +include "basic_2/notation/constructors/dxvoid_1.ma". include "basic_2/notation/constructors/dxabbr_2.ma". include "basic_2/notation/constructors/dxabst_2.ma". -include "basic_2/syntax/term.ma". +include "basic_2/syntax/bind.ma". (* LOCAL ENVIRONMENTS *******************************************************) @@ -28,10 +31,16 @@ inductive lenv: Type[0] ≝ interpretation "sort (local environment)" 'Star = LAtom. - +(* +interpretation "local environment binding construction (unary)" + 'DxBind1 L I = (LUnit L I). +*) interpretation "local environment binding construction (binary)" 'DxBind2 L I T = (LPair L I T). - +(* +interpretation "void (local environment)" + 'DxVoid L = (LPair L Void). +*) interpretation "abbreviation (local environment)" 'DxAbbr L T = (LPair L Abbr T). diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_weight.ma index 1a61b7d4f..4bf0bcaa8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_weight.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/syntax/term_weight.ma". +include "basic_2/syntax/bind_weight.ma". include "basic_2/syntax/lenv.ma". (* WEIGHT OF A LOCAL ENVIRONMENT ********************************************) @@ -27,7 +27,7 @@ interpretation "weight (local environment)" 'Weight L = (lw L). (* Basic properties *********************************************************) lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}. -/3 width=1 by lt_plus_to_minus_r, monotonic_lt_plus_r/ qed. +normalize /2 width=1 by monotonic_le_plus_r/ qed. (* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *) (* Basic_1: removed local theorems 1: clt_wf__q_ind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_weight.ma index 9076a9b2f..63b498610 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_weight.ma @@ -19,7 +19,7 @@ include "basic_2/syntax/term.ma". rec definition tw T ≝ match T with [ TAtom _ ⇒ 1 -| TPair _ V T ⇒ tw V + tw T + 1 +| TPair _ V T ⇒ ⫯(tw V + tw T) ]. interpretation "weight (term)" 'Weight T = (tw T). 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 673982592..322483d4e 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 @@ -257,6 +257,10 @@ table { [ "lenv" * ] } ] + [ { "binders for local environments" * } { + [ "bind" "bind_weight" * ] + } + ] [ { "terms" * } { [ "term_vector ( Ⓐ?.? )" * ] [ "term_simple ( 𝐒⦃?⦄ )" * ]