2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/relations.ma".
14 (********** bool **********)
15 inductive bool: Type[0] ≝
19 theorem not_eq_true_false : true ≠ false.
23 definition notb : bool → bool ≝
24 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
26 interpretation "boolean not" 'not x = (notb x).
28 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
31 | false ⇒ P true] → P (notb b).
32 #b #P elim b normalize // qed.
34 theorem notb_notb: ∀b:bool. notb (notb b) = b.
37 theorem injective_notb: injective bool bool notb.
40 definition andb : bool → bool → bool ≝
41 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
43 interpretation "boolean and" 'and x y = (andb x y).
45 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
46 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
47 #b1 #b2 #P (elim b1) normalize // qed.
49 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
50 #b1 (cases b1) normalize // qed.
52 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
53 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
55 theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
58 definition orb : bool → bool → bool ≝
59 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
61 interpretation "boolean or" 'or x y = (orb x y).
63 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
64 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
65 #b1 #b2 #P (elim b1) normalize // qed.
67 lemma orb_true_r1: ∀b1,b2:bool.
68 b1 = true → (b1 ∨ b2) = true.
71 lemma orb_true_r2: ∀b1,b2:bool.
72 b2 = true → (b1 ∨ b2) = true.
73 #b1 #b2 #H >H cases b1 // qed.
75 lemma orb_true_l: ∀b1,b2:bool.
76 (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
79 definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝
80 λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q].
82 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 }.
83 interpretation "if_then_else" 'if_then_else e t f = (if_then_else ? e t f).
85 theorem bool_to_decidable_eq:
86 ∀b1,b2:bool. decidable (b1=b2).
87 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
89 theorem true_or_false:
90 ∀b:bool. b = true ∨ b = false.
94 (****** DeqSet: a set with a decidbale equality ******)
96 record DeqSet : Type[1] ≝ { carr :> Type[0];
97 eqb: carr → carr → bool;
98 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
101 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
102 interpretation "eqb" 'eqb a b = (eqb ? a b).
105 (****** EnumSet: a DeqSet with an enumeration function ******
107 record EnumSet : Type[1] ≝ { carr :> DeqSet;
109 eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)