(* 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
].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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_append_empty_sn //
+| #hd #tl #IH <list_append_lcons_sn <IH //
+]
+qed.
+
+lemma list_append_assoc (A):
+ associative … (list_append A).
+#A #l1 elim l1 -l1
+[ <list_append_empty_sn //
+| #a1 #l1 #IH *
+ [ #l3 <list_append_empty_dx <list_append_empty_sn //
+ | #a2 #l2 #l3 <list_append_lcons_sn <list_append_lcons_sn <IH //
+ ]
+]
+qed.
rec definition list_eq A (l1,l2:list A) on l1 ≝
match l1 with
-[ list_nil ⇒
+[ list_empty ⇒
match l2 with
- [ list_nil ⇒ ⊤
- | list_cons _ _ ⇒ ⊥
+ [ list_empty ⇒ ⊤
+ | list_lcons _ _ ⇒ ⊥
]
-| list_cons a1 l1 ⇒
+| list_lcons a1 l1 ⇒
match l2 with
- [ list_nil ⇒ ⊥
- | list_cons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
+ [ list_empty ⇒ ⊥
+ | list_lcons a2 l2 ⇒ a1 = a2 ∧ list_eq A l1 l2
]
].
(* LENGTH FOR LISTS *********************************************************)
rec definition list_length A (l:list A) on l ≝ match l with
-[ list_nil ⇒ 𝟎
-| list_cons _ l ⇒ ↑(list_length A l)
+[ list_empty ⇒ 𝟎
+| list_lcons _ l ⇒ ↑(list_length A l)
].
interpretation
(* Basic constructions ******************************************************)
-lemma list_length_nil (A:Type[0]): |list_nil A| = 𝟎.
+lemma list_length_empty (A:Type[0]): |list_empty A| = 𝟎.
// qed.
-lemma list_length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
+lemma list_length_lcons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|.
// qed.
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
|l| = 𝟎 → l = Ⓔ.
-#A * // #a #l >list_length_cons #H
+#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero … H)
qed-.
|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-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
(* GROUND NOTATION **********************************************************)
notation "hvbox( l1 @@ break l2 )"
- right associative with precedence 47
+ right associative with precedence 55
for @{ 'Append $l1 $l2 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
[ "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" * ]
projects / helm.git / commitdiff