Listb contains some boolean functions over lists.

[helm.git] / matita / matita / lib / basics / list.ma

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 4d99c59c8e3364f4ef0b71fd3c1227ad444f9bc1..eaf89510a153c2f90e67c23c45caccf93a09f9d0 100644 (file)
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -10,7 +10,7 @@
       V_______________________________________________________________ *)
 
 include "basics/types.ma".
-include "basics/bool.ma".
+include "arithmetics/nat.ma".
 
 inductive list (A:Type[0]) : Type[0] :=
   | nil: list A
@@ -72,7 +72,7 @@ ntheorem cons_append_commute:
 //; nqed. *)
 
 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
-/2/ qed.
+#A #a #l #l1 >associative_append // qed.
 
 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop. 
   l1@l2=[] → P (nil A) (nil A) → P l1 l2.
@@ -114,6 +114,25 @@ match l1 with
   | cons a tl ⇒ (map ??(dp ?? a) (g a)) @ dprodl A f tl g
   ].
 
+(**************************** length ******************************)
+
+let rec length (A:Type[0]) (l:list A) on l ≝ 
+  match l with 
+    [ nil ⇒ 0
+    | cons a tl ⇒ S (length A tl)].
+
+notation "|M|" non associative with precedence 60 for @{'norm $M}.
+interpretation "norm" 'norm l = (length ? l).
+
+let rec nth n (A:Type[0]) (l:list A) (d:A)  ≝  
+  match n with
+    [O ⇒ hd A l d
+    |S m ⇒ nth m A (tail A l) d].
+
+lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
+#A #a #i elim i normalize //
+qed.
+
 (**************************** fold *******************************)
 
 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝  
@@ -168,3 +187,32 @@ theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
   [>nill //|#a #tl #Hind <assoc //]
 qed.
 
+(********************** lhd and ltl ******************************)
+
+let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
+   [ O   ⇒ nil …
+   | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
+   ].
+
+let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
+   [ O   ⇒ l
+   | S n ⇒ ltl A (tail … l) n
+   ].
+
+lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
+#A #n elim n //
+qed.
+
+lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
+#A #n elim n normalize //
+qed.
+
+lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
+#A #n elim n -n //
+#n #IHn #l elim l normalize //
+qed.
+
+lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
+#A #n elim n -n /2/
+#n #IHn *; normalize /2/
+qed.