From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 9 Dec 2011 10:43:51 +0000 (+0000)
Subject: list.ma moved inside lists.
X-Git-Tag: make_still_working~2038
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=844794906f5a9f97406d72b5305ce13fb75acf94;p=helm.git

list.ma moved inside lists.
Minor integrations.
---

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index ce857937c..7b2606485 100644
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -52,6 +52,9 @@ theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
 
+theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
+/3/ qed.
+
 definition orb : bool → bool → bool ≝
 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
  
@@ -61,9 +64,24 @@ theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
+lemma orb_true_r1: ∀b1,b2:bool. 
+  b1 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H // qed.
+
+lemma orb_true_r2: ∀b1,b2:bool. 
+  b2 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H cases b1 // qed.
+
+lemma orb_true_l: ∀b1,b2:bool. 
+  (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
+* normalize /2/ qed.
+
 definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ 
 λA.λb.λ P,Q:A. match b with [ true ⇒ P | false  ⇒ Q].
 
+notation "'if' term 19 e 'then' term 19 t 'else' term 19 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
+interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
+
 theorem bool_to_decidable_eq: 
   ∀b1,b2:bool. decidable (b1=b2).
 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
@@ -73,3 +91,22 @@ theorem true_or_false:
 #b (cases b) /2/ qed.
 
 
+(****** DeqSet: a set with a decidbale equality ******)
+
+record DeqSet : Type[1] ≝ { carr :> Type[0];
+   eqb: carr → carr → bool;
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+}.
+
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+
+(****** EnumSet: a DeqSet with an enumeration function  ******
+
+record EnumSet : Type[1] ≝ { carr :> DeqSet;
+   enum: carr 
+   eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+}.
+
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
deleted file mode 100644
index eaf89510a..000000000
--- a/matita/matita/lib/basics/list.ma
+++ /dev/null
@@ -1,218 +0,0 @@
-(*
-    ||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).
-
-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).
-
-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/sets.ma b/matita/matita/lib/basics/sets.ma
index 622025d79..bb077e653 100644
--- a/matita/matita/lib/basics/sets.ma
+++ b/matita/matita/lib/basics/sets.ma
@@ -27,8 +27,14 @@ interpretation "union" 'union a b = (union ? a b).
 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
-interpretation "subset" 'subseteq a b = (intersection ? a b).
+interpretation "subset" 'subseteq a b = (subset ? a b).
 
 (* extensional equality *)
 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
@@ -51,6 +57,22 @@ lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
   B =1 C  → A ∪ B =1 A ∪ C.
 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
   
+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
+  A =1 C  → A ∩ B =1 C ∩ B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+  
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
+  B =1 C  → A ∩ B =1 A ∩ C.
+#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
+  A =1 C  → A - B =1 C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+  
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
+  B =1 C  → A - B =1 A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
 (* set equalities *)
 lemma union_comm : ∀U.∀A,B:U →Prop. 
   A ∪ B =1 B ∪ A.
@@ -73,4 +95,19 @@ lemma cap_idemp: ∀U.∀A:U →Prop.
   A ∩ A =1 A.
 #U #A #a % [* // | /2/] qed. 
 
+(*distributivities *)
 
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+  
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) - C =1 (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+
+(* substraction *)
+lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+#U #A #B #w normalize /2/
+qed.
\ No newline at end of file
diff --git a/matita/matita/lib/basics/types.ma b/matita/matita/lib/basics/types.ma
index 08b99a8cb..f35dde531 100644
--- a/matita/matita/lib/basics/types.ma
+++ b/matita/matita/lib/basics/types.ma
@@ -42,6 +42,12 @@ theorem eq_pair_fst_snd: ∀A,B.∀p:A × B.
   p = 〈 \fst p, \snd p 〉.
 #A #B #p (cases p) // qed.
 
+lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+// qed.
+
+lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+// qed.
+
 (* sum *)
 inductive Sum (A,B:Type[0]) : Type[0] ≝
   inl : A → Sum A B