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 (* destruct does not work *)
20 theorem not_eq_true_false : true ≠ false.
21 @nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
24 definition notb : bool → bool ≝
25 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
27 interpretation "boolean not" 'not x = (notb x).
29 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
32 | false ⇒ P true] → P (notb b).
33 #b #P elim b normalize // qed.
35 theorem notb_notb: ∀b:bool. notb (notb b) = b.
38 theorem injective_notb: injective bool bool notb.
41 theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2.
42 * * // #H @False_ind /2/
45 theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2.
46 * * normalize // #H @(not_to_not … not_eq_true_false) //
49 definition andb : bool → bool → bool ≝
50 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
52 interpretation "boolean and" 'and x y = (andb x y).
54 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
55 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
56 #b1 #b2 #P (elim b1) normalize // qed.
58 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
59 #b1 (cases b1) normalize // qed.
61 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
62 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
64 theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
67 definition orb : bool → bool → bool ≝
68 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
70 interpretation "boolean or" 'or x y = (orb x y).
72 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
73 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
74 #b1 #b2 #P (elim b1) normalize // qed.
76 lemma orb_true_r1: ∀b1,b2:bool.
77 b1 = true → (b1 ∨ b2) = true.
80 lemma orb_true_r2: ∀b1,b2:bool.
81 b2 = true → (b1 ∨ b2) = true.
82 #b1 #b2 #H >H cases b1 // qed.
84 lemma orb_true_l: ∀b1,b2:bool.
85 (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
88 definition xorb : bool → bool → bool ≝
91 [ true ⇒ match b2 with [ true ⇒ false | false ⇒ true ]
92 | false ⇒ match b2 with [ true ⇒ true | false ⇒ false ]].
94 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
95 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }.
96 notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46
97 for @{ match $e with [ true ⇒ $t | false ⇒ $f] }.
99 theorem bool_to_decidable_eq:
100 ∀b1,b2:bool. decidable (b1=b2).
101 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
103 theorem true_or_false:
104 ∀b:bool. b = true ∨ b = false.
105 #b (cases b) /2/ qed.