From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 6 Dec 2011 15:03:22 +0000 (+0000)
Subject: Listb contains some boolean functions over lists.
X-Git-Tag: make_still_working~2051
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=471aadb252fa56a9d8fe484da01fdcff0d12814c;p=helm.git

Listb contains some boolean functions over lists.
---

diff --git a/matita/matita/lib/basics/lists/list.ma b/matita/matita/lib/basics/lists/list.ma
new file mode 100644
index 000000000..a1ffa3995
--- /dev/null
+++ b/matita/matita/lib/basics/lists/list.ma
@@ -0,0 +1,230 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+include "basics/types.ma".
+include "arithmetics/nat.ma".
+
+inductive list (A:Type[0]) : Type[0] :=
+  | 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).
+
+definition not_nil: ∀A:Type[0].list A → Prop ≝
+ λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
+
+theorem nil_cons:
+  ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
+  #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
+qed.
+
+(*
+let rec id_list A (l: list A) on l :=
+  match l with
+  [ nil => []
+  | (cons hd tl) => hd :: id_list A tl ]. *)
+
+let rec append A (l1: list A) l2 on l1 ≝ 
+  match l1 with
+  [ nil ⇒  l2
+  | cons hd tl ⇒  hd :: append A tl l2 ].
+
+definition hd ≝ λA.λl: list A.λd:A.
+  match l with [ nil ⇒ d | cons a _ ⇒ a].
+
+definition tail ≝  λA.λl: list A.
+  match l with [ nil ⇒  [] | cons hd tl ⇒  tl].
+
+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+theorem append_nil: ∀A.∀l:list A.l @ [] = l.
+#A #l (elim l) normalize // qed.
+
+theorem associative_append: 
+ ∀A.associative (list A) (append A).
+#A #l1 #l2 #l3 (elim l1) normalize // qed.
+
+(* deleterio per auto 
+ntheorem cons_append_commute:
+  ∀A:Type.∀l1,l2:list A.∀a:A.
+    a :: (l1 @ l2) = (a :: l1) @ l2.
+//; nqed. *)
+
+theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
+#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.
+#A #l1 #l2 #P (cases l1) normalize //
+#a #l3 #heq destruct
+qed.
+
+theorem nil_to_nil:  ∀A.∀l1,l2:list A.
+  l1@l2 = [] → l1 = [] ∧ l2 = [].
+#A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
+qed.
+
+(* iterators *)
+
+let rec map (A,B:Type[0]) (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)].
+  
+let rec foldr (A,B:Type[0]) (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)].
+ 
+definition filter ≝ 
+  λT.λp:T → bool.
+  foldr T (list T) (λx,l0.if_then_else ? (p x) (x::l0) l0) (nil T).
+
+(* compose f [a1;...;an] [b1;...;bm] = 
+  [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
+ 
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+    foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+lemma filter_true : ∀A,l,a,p. p a = true → 
+  filter A p (a::l) = a :: filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+lemma filter_false : ∀A,l,a,p. p a = false → 
+  filter A p (a::l) = filter A p l.
+#A #l #a #p #pa (elim l) normalize >pa normalize // qed.
+
+theorem 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 (elim l) normalize // qed.
+
+let rec dprodl (A:Type[0]) (f:A→Type[0]) (l1:list A) (g:(∀a:A.list (f a))) on l1 ≝
+match l1 with
+  [ nil ⇒ nil ?
+  | 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).
+
+lemma length_append: ∀A.∀l1,l2:list A. 
+  |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // normalize /2/
+qed.
+
+(****************************** nth ********************************)
+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 ≝  
+ match l with 
+  [ nil ⇒ b 
+  | cons a l ⇒ if_then_else ? (p a) (op (f a) (fold A B op b p f l))
+      (fold A B op b p f l)].
+      
+notation "\fold  [ op , nil ]_{ ident i ∈ l | p} f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
+
+notation "\fold [ op , nil ]_{ident i ∈ l } f"
+  with precedence 80
+for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
+
+interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
+
+theorem fold_true: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true → 
+  \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+    op (f a) \fold[op,nil]_{i ∈ l| p i} (f i). 
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_false: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
+p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) = 
+  \fold[op,nil]_{i ∈ l| p i} (f i).
+#A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
+
+theorem fold_filter: 
+∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
+  \fold[op,nil]_{i ∈ l| p i} (f i) = 
+    \fold[op,nil]_{i ∈ (filter A p l)} (f i).
+#A #B #a #l #p #op #nil #f elim l //  
+#a #tl #Hind cases(true_or_false (p a)) #pa 
+  [ >filter_true // > fold_true // >fold_true //
+  | >filter_false // >fold_false // ]
+qed.
+
+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+  {op :2> A → A → A; 
+   nill:∀a. op nil a = a; 
+   nilr:∀a. op a nil = a;
+   assoc: ∀a,b,c.op a (op b c) = op (op a b) c
+  }.
+
+theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
+  op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
+    \fold[op,nil]_{i∈(I@J)} (f i).
+#A #B #I #J #nil #op #f (elim I) normalize 
+  [>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.
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
new file mode 100644
index 000000000..9af4b04a6
--- /dev/null
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -0,0 +1,196 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_______________________________________________________________ *)
+
+
+(* boolean functions over lists *)
+
+include "basics/lists/list.ma".
+include "basics/sets.ma".
+
+(********* search *********)
+
+let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
+  match l with
+  [ nil ⇒ false
+  | cons a tl ⇒ (a == x) ∨ memb S x tl
+  ].
+  
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
+qed.
+
+lemma memb_cons: ∀S,a,b,l. 
+  memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (b==a) normalize // 
+qed.
+
+lemma memb_append: ∀S,a,l1,l2. 
+memb S a (l1@l2) = true →
+  memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //] 
+#b #tl #Hind #l2 cases (b==a) normalize /2/ 
+qed. 
+
+lemma memb_append_l1: ∀S,a,l1,l2. 
+ memb S a l1= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize
+  [normalize #le #abs @False_ind /2/
+  |#b #tl #Hind #l2 cases (b==a) normalize /2/ 
+  ]
+qed. 
+
+lemma memb_append_l2: ∀S,a,l1,l2. 
+ memb S a l2= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize //
+#b #tl #Hind #l2 cases (b==a) normalize /2/ 
+qed. 
+
+lemma memb_exists: ∀S,a,l.memb S a l = true → 
+  ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /2/]
+#b #tl #Hind #H cases (orb_true_l … H)
+  [#eqba @(ex_intro … (nil S)) @(ex_intro … tl)
+   >(proj1 … (eqb_true …) eqba) //
+  |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+   @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+  ]
+qed.
+
+lemma not_memb_to_not_eq: ∀S,a,b,l. 
+ memb S a l = false → memb S b l = true → a==b = false.
+#S #a #b #l cases (true_or_false (a==b)) // 
+#eqab >(proj1 … (eqb_true …) eqab) #H >H #abs @False_ind /2/
+qed. 
+ 
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true → 
+  memb S2 (f a) (map … f l) = true.
+#S1 #S2 #f #a #l elim l normalize [//]
+#x #tl #memba cases (true_or_false (x==a))
+  [#eqx >eqx >(proj1 … (eqb_true …) eqx) 
+   >(proj2 … (eqb_true …) (refl … (f a))) normalize //
+  |#eqx >eqx cases (f x==f a) normalize /2/
+  ]
+qed.
+
+lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.   
+  memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+  memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
+#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
+  [#eqa1 >(proj1 … (eqb_true …) eqa1) @memb_append_l1 @memb_map // 
+  |#membtl @memb_append_l2 @Hind //
+  ]
+qed.
+
+(**************** unicity test *****************)
+
+let rec uniqueb (S:DeqSet) l on l : bool ≝
+  match l with 
+  [ nil ⇒ true
+  | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+  ].
+
+(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
+
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
+  match l1 with
+  [ nil ⇒ l2
+  | cons a tl ⇒ 
+     let r ≝ unique_append S tl l2 in
+     if (memb S a r) then r else a::r
+  ].
+
+axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2. 
+(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
+∀x. memb S x (unique_append S l1 l2) = true → P x. 
+
+lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+  uniqueb S (unique_append S l1 l2) = true.
+#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
+cases (true_or_false … (memb S a (unique_append S tl l2))) 
+#H >H normalize [@Hind //] >H normalize @Hind //
+qed.
+
+(******************* sublist *******************)
+definition sublist ≝ 
+  λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+lemma sublist_length: ∀S,l1,l2. 
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
+#S #l1 elim l1 // 
+#a #tl #Hind #l2 #unique #sub
+cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize 
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
+>eql2 in sub; #sub #x #membx 
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+  [#membxl3 @memb_append_l1 //
+  |#membxal4 cases (orb_true_l … membxal4)
+    [#eqax @False_ind lapply (andb_true_l … unique)
+     >(proj1 … (eqb_true …) eqax) >membx normalize /2/
+    |#membxl4 @memb_append_l2 //
+    ]
+  ]
+qed.
+
+lemma sublist_unique_append_l1: 
+  ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
+#x #tl #Hind #l2 #a 
+normalize cases (true_or_false … (x==a)) #eqxa >eqxa 
+[>(proj1 … (eqb_true …) eqxa) cases (true_or_false (memb S a (unique_append S tl l2)))
+  [#H >H normalize // | #H >H normalize >(proj2 … (eqb_true …) (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize 
+  [/2/ |>eqxa normalize /2/]
+]
+qed.
+
+lemma sublist_unique_append_l2: 
+  ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+#S #l1 elim l1 [normalize //] #x #tl #Hind normalize 
+#l2 #a cases (memb S x (unique_append S tl l2)) normalize
+[@Hind | cases (x==a) normalize // @Hind]
+qed.
+
+(********************* filtering *****************)
+
+lemma filter_true: ∀S,f,a,l. 
+  memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /2/]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+cases (true_or_false (b==a)) #eqab
+  [#_ <(proj1 … (eqb_true …) eqab) // | >eqab normalize @Hind]
+qed. 
+  
+lemma memb_filter_memb: ∀S,f,a,l. 
+  memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize 
+cases (b==a) normalize // @Hind
+qed.
+  
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true → 
+memb S x l = true ∧ (f x = true).
+/3/ qed.
+
+lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
+#S #f #x #l #fx elim l normalize //
+#b #tl #Hind cases (true_or_false (b==x)) #eqbx
+  [>(proj1 … (eqb_true … ) eqbx) >(proj2 … (eqb_true …) (refl … x))
+   >fx normalize >(proj2 … (eqb_true …) (refl … x)) normalize //
+  |>eqbx cases (f b) normalize [>eqbx normalize @Hind| @Hind]
+  ]
+qed. 
+
+
+