From dd41efaab7f147d5673cc30a27d36375f9b52c9d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 2 Dec 2021 22:45:57 +0100 Subject: [PATCH] update in ground + additions and corrections on lists --- .../contribs/lambdadelta/ground/lib/list.ma | 18 +++--- .../lambdadelta/ground/lib/list_append.ma | 58 +++++++++++++++++++ .../lambdadelta/ground/lib/list_eq.ma | 12 ++-- .../lambdadelta/ground/lib/list_length.ma | 14 ++--- .../lambdadelta/ground/lib/list_rcons.ma | 43 ++++++++++++++ .../ground/notation/functions/append_2.ma | 2 +- .../ground/notation/functions/oplus_3.ma | 27 +++++++++ .../ground/notation/functions/oplusleft_3.ma | 27 +++++++++ .../lambdadelta/ground/web/ground_src.tbl | 7 ++- 9 files changed, 184 insertions(+), 24 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/list_append.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma create mode 100644 matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma index 184438f61..21a0f7560 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma @@ -18,20 +18,20 @@ include "ground/lib/relations.ma". (* LISTS ********************************************************************) -inductive list (A:Type[0]) : Type[0] := -| list_nil : list A -| list_cons: A → list A → list A +inductive list (A:Type[0]): Type[0] := +| list_empty: list A +| list_lcons: A → list A → list A . interpretation - "nil (lists)" - 'CircledE A = (list_nil A). + "empty (lists)" + 'CircledE A = (list_empty A). interpretation - "cons (lists)" - 'OPlusRight A hd tl = (list_cons A hd tl). + "left cons (lists)" + 'OPlusRight A hd tl = (list_lcons A hd tl). rec definition list_all A (R:predicate A) (l:list A) on l ≝ match l with -[ list_nil ⇒ ⊤ -| list_cons hd tl ⇒ ∧∧ R hd & list_all A R tl +[ list_empty ⇒ ⊤ +| list_lcons hd tl ⇒ ∧∧ R hd & list_all A R tl ]. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma new file mode 100644 index 000000000..2dcf8e576 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/functions/oplus_3.ma". +include "ground/lib/list.ma". + +(* APPEND FOR LISTS *********************************************************) + +rec definition list_append A (l1:list A) (l2:list A) on l1 ≝ match l1 with +[ list_empty ⇒ l2 +| list_lcons hd tl ⇒ hd ⨮ (list_append A tl l2) +]. + +interpretation + "append (lists)" + 'OPlus A l1 l2 = (list_append A l1 l2). + +(* Basic constructions ******************************************************) + +lemma list_append_empty_sn (A): + ∀l2. l2 = Ⓔ ⨁{A} l2. +// qed. + +lemma list_append_lcons_sn (A): + ∀a,l1,l2. a ⨮ l1 ⨁ l2 = (a⨮l1) ⨁{A} l2. +// qed. + +(* Advanced constructions ***************************************************) + +lemma list_append_empty_dx (A): + ∀l1. l1 = l1 ⨁{A} Ⓔ. +#A #l1 elim l1 -l1 +[ list_length_cons #H +#A * // #a #l >list_length_lcons #H elim (eq_inv_nsucc_zero … H) qed-. @@ -50,9 +50,9 @@ lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x → ∃∃tl,a. x = |tl| & l = a ⨮ tl. #A * -[ #x >list_length_nil #H +[ #x >list_length_empty #H elim (eq_inv_zero_nsucc … H) -| #a #l #x >list_length_cons #H +| #a #l #x >list_length_lcons #H /3 width=4 by eq_inv_nsucc_bi, ex2_2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma new file mode 100644 index 000000000..429a766fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/notation/functions/oplusleft_3.ma". +include "ground/lib/list_append.ma". + +(* RIGHT CONS FOR LISTS *****************************************************) + +interpretation + "right cons (lists)" + 'OPlusLeft A hd tl = (list_append A hd (list_lcons A tl (list_empty A))). + +(* Basic constructions ******************************************************) + +lemma list_cons_comm (A): + ∀a. a ⨮ Ⓔ = Ⓔ ⨭{A} a. +// qed. + +lemma list_cons_shift (A): + ∀a1,l,a2. a1 ⨮{A} l ⨭ a2 = (a1 ⨮ l) ⨭ a2. +// qed. + +(* Advanced constructions ***************************************************) + +(* Note: this is list_append_lcons_dx *) +lemma list_append_rcons_sn (A): + ∀l1,l2,a. l1 ⨁ (a ⨮ l2) = (l1 ⨭ a) ⨁{A} l2. +// qed. + +lemma list_append_rcons_dx (A): + ∀l1,l2,a. l1 ⨁ l2 ⨭ a = l1 ⨁{A} (l2 ⨭ a). +// qed. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma index acf8e6df2..1d14afad7 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma @@ -15,5 +15,5 @@ (* GROUND NOTATION **********************************************************) notation "hvbox( l1 @@ break l2 )" - right associative with precedence 47 + right associative with precedence 55 for @{ 'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma new file mode 100644 index 000000000..d1860243f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( hd ⨁ break tl )" + right associative with precedence 55 + for @{ 'OPlus $S $hd $tl }. + +notation > "hvbox( hd ⨁ break tl )" + right associative with precedence 55 + for @{ 'OPlus ? $hd $tl }. + +notation > "hvbox( hd ⨁{ break term 46 S } break term 54 tl )" + non associative with precedence 55 + for @{ 'OPlus $S $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma new file mode 100644 index 000000000..2e4bbf673 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( hd ⨭ break tl )" + left associative with precedence 50 + for @{ 'OPlusLeft $S $hd $tl }. + +notation > "hvbox( hd ⨭ break tl )" + left associative with precedence 50 + for @{ 'OPlusLeft ? $hd $tl }. + +notation > "hvbox( hd ⨭{ break term 46 S } break term 50 tl )" + non associative with precedence 50 + for @{ 'OPlusLeft $S $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index a4c2883e4..be1cfadbb 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -130,8 +130,13 @@ table { [ "stream ( ? ⨮{?} ? )" * ] } ] + [ { "lists" * } { + [ "list_append ( ?⨁{?}? )" "list_rcons ( ?⨭{?}? )" * ] + [ "list_length ( |?| )" * ] + [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" * ] + } + ] [ { "" * } { - [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" "list_length ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ] [ "ltc" "ltc_ctc" * ] [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ] -- 2.39.2