From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 15 Dec 2011 15:22:19 +0000 (+0000)
Subject: Splitted DeqSets in their own file. Notation for memb to hide the type.
X-Git-Tag: make_still_working~2002
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dec09d382f401b62b3ee183c9b60b883d0d33255;p=helm.git

Splitted DeqSets in their own file. Notation for memb to hide the type.
---

diff --git a/matita/matita/lib/basics/bool.ma b/matita/matita/lib/basics/bool.ma
index 98b14ad29..43a3369a3 100644
--- a/matita/matita/lib/basics/bool.ma
+++ b/matita/matita/lib/basics/bool.ma
@@ -95,23 +95,3 @@ theorem true_or_false:
 ∀b:bool. b = true ∨ b = 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)
-}.
-
-*)
diff --git a/matita/matita/lib/basics/deqsets.ma b/matita/matita/lib/basics/deqsets.ma
new file mode 100644
index 000000000..4d86c9f6c
--- /dev/null
+++ b/matita/matita/lib/basics/deqsets.ma
@@ -0,0 +1,103 @@
+(*
+    ||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 "basics/bool.ma".
+
+(****** 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).
+
+notation "\P H" non associative with precedence 90 
+  for @{(proj1 … (eqb_true ???) $H)}. 
+
+notation "\b H" non associative with precedence 90 
+  for @{(proj2 … (eqb_true ???) $H)}. 
+  
+lemma eqb_false: ∀S:DeqSet.∀a,b:S. 
+  (eqb ? a b) = false ↔ a ≠ b.
+#S #a #b % #H 
+  [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
+  |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
+  ]
+qed.
+ 
+notation "\Pf H" non associative with precedence 90 
+  for @{(proj1 … (eqb_false ???) $H)}. 
+
+notation "\bf H" non associative with precedence 90 
+  for @{(proj2 … (eqb_false ???) $H)}. 
+  
+lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
+#S #a #b cases (true_or_false (eqb ? a b)) #H
+  [%1 @(\P H) | %2 @(\Pf H)]
+qed.
+
+definition beqb ≝ λb1,b2.
+  match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
+lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
+#b1 #b2 cases b1 cases b2 normalize /2/
+qed. 
+
+definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+
+unification hint  0 ≔ ; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    bool ≡ carr X.
+    
+unification hint  0 ≔ b1,b2:bool; 
+    X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢ 
+    beqb b1 b2 ≡ eqb X b1 b2.
+    
+example exhint: ∀b:bool. (b == false) = true → b = false. 
+#b #H @(\P H).
+qed.
+
+(* pairs *)
+definition eq_pairs ≝
+  λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+  eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+  [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+  |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+  ]
+qed.
+
+definition DeqProd ≝ λA,B:DeqSet.
+  mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+  
+unification hint  0 ≔ C1,C2; 
+    T1 ≟ carr C1,
+    T2 ≟ carr C2,
+    X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢ 
+    T1×T2 ≡ carr X.
+
+unification hint  0 ≔ T1,T2,p1,p2; 
+    X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢ 
+    eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2. 
+  〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H).
\ No newline at end of file
diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 29d89ffee..f74714956 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -14,6 +14,7 @@
 
 include "basics/lists/list.ma".
 include "basics/sets.ma".
+include "basics/deqsets.ma".
 
 (********* search *********)
 
@@ -22,7 +23,10 @@ let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
   [ nil ⇒ false
   | cons a tl ⇒ (a == x) ∨ memb S x tl
   ].
-  
+
+notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
+interpretation "boolean membership" 'memb a l = (memb ? a l).
+
 lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
 #S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
 qed.