lists

diff --git a/helm/software/matita/nlibrary/basics/list.ma b/helm/software/matita/nlibrary/basics/list.ma
new file mode 100644 (file)
index 0000000..6221060
--- /dev/null
+++ b/helm/software/matita/nlibrary/basics/list.ma
@@ -0,0 +1,91 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "basics/eq.ma".
+include "basics/bool.ma".
+
+ninductive list (A:Type) : Type :=
+  | nil: list A
+  | cons: A -> list A -> list A.
+
+notation "hvbox(hd break :: tl)"
+  right associative with precedence 47
+  for @{'cons $hd $tl}.
+
+notation "[ list0 x sep ; ]"
+  non associative with precedence 90
+  for ${fold right @'nil rec acc @{'cons $x $acc}}.
+
+notation "hvbox(l1 break @ l2)"
+  right associative with precedence 47
+  for @{'append $l1 $l2 }.
+
+interpretation "nil" 'nil = (nil ?).
+interpretation "cons" 'cons hd tl = (cons ? hd tl).
+
+ndefinition not_nil: ∀A:Type.list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+
+ntheorem nil_cons:
+  ∀A:Type.∀l:list A.∀a:A. a::l ≠ [].
+  #A; #l; #a; #Heq; nchange with (not_nil ? (a::l));
+  nrewrite > Heq; //;
+nqed.
+
+(*
+let rec id_list A (l: list A) on l :=
+  match l with
+  [ nil => []
+  | (cons hd tl) => hd :: id_list A tl ]. *)
+
+nlet rec append A (l1: list A) l2 on l1 :=
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :: append A tl l2 ].
+
+ndefinition tail := λA:Type.λl: list A.
+  match l with
+  [ nil ⇒  []
+  | cons hd tl ⇒  tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l.
+#A; #l; nelim l; nnormalize;//; nqed.
+
+ntheorem associative_append: 
+ ∀A:Type.associative (list A) (append A).
+#A; #l1; #l2; #l3; nelim l1; nnormalize; //; nqed.
+
+ntheorem cons_append_commute:
+  ∀A:Type.∀l1,l2:list A.∀a:A.
+    a :: (l1 @ l2) = (a :: l1) @ l2.
+//; nqed.
+
+ntheorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+/2/; nqed.
+
+nlet rec map (A,B:Type) (f: A → B) (l:list A) on l: list B ≝
+ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+  
+nlet rec foldr (A,B:Type) (f:A → B → B) (b:B) (l:list A) on l :B ≝  
+ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
+   
+ndefinition filter ≝ 
+  λT:Type.λl:list T.λp:T → bool.
+  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0).
+  
+ntheorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+#A; #B; #f; #g; #l; #eqfg; nelim l; nnormalize; //; nqed.
+