matita/matita/lib/basics/bool.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_______________________________________________________________ *)
  11
  12 include "basics/relations.ma".
  13
  14 (********** bool **********)
  15 inductive bool: Type[0] ≝
  16   | true : bool
  17   | false : bool.
  18
  19 theorem not_eq_true_false : true ≠ false.
  20 @nmk #Heq destruct
  21 qed.
  22
  23 definition notb : bool → bool ≝
  24 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
  25
  26 interpretation "boolean not" 'not x = (notb x).
  27
  28 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
  29 match b with
  30 [ true ⇒ P false
  31 | false ⇒ P true] → P (notb b).
  32 #b #P elim b normalize // qed.
  33
  34 theorem notb_notb: ∀b:bool. notb (notb b) = b.
  35 #b elim b // qed.
  36
  37 theorem injective_notb: injective bool bool notb.
  38 #b1 #b2 #H // qed.
  39
  40 theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2.
  41 * * // #H @False_ind /2/
  42 qed.
  43
  44 theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2.
  45 * * normalize // #_ @(not_to_not … not_eq_true_false) //
  46 qed.
  47
  48 definition andb : bool → bool → bool ≝
  49 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
  50
  51 interpretation "boolean and" 'and x y = (andb x y).
  52
  53 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  54 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
  55 #b1 #b2 #P (elim b1) normalize // qed.
  56
  57 theorem true_to_andb_true: ∀b1,b2. b1 = true → b2 = true → (b1 ∧ b2) = true.
  58 #b1 cases b1 normalize //
  59 qed.
  60
  61 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
  62 #b1 (cases b1) normalize // qed.
  63
  64 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
  65 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
  66
  67 theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
  68 /3/ qed.
  69
  70 definition orb : bool → bool → bool ≝
  71 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
  72
  73 interpretation "boolean or" 'or x y = (orb x y).
  74
  75 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  76 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
  77 #b1 #b2 #P (elim b1) normalize // qed.
  78
  79 lemma orb_true_r1: ∀b1,b2:bool.
  80   b1 = true → (b1 ∨ b2) = true.
  81 #b1 #b2 #H >H // qed.
  82
  83 lemma orb_true_r2: ∀b1,b2:bool.
  84   b2 = true → (b1 ∨ b2) = true.
  85 #b1 #b2 #H >H cases b1 // qed.
  86
  87 lemma orb_true_l: ∀b1,b2:bool.
  88   (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
  89 * normalize /2/ qed.
  90
  91 definition xorb : bool → bool → bool ≝
  92 λb1,b2:bool.
  93  match b1 with
  94   [ true ⇒  match b2 with [ true ⇒ false | false ⇒ true ]
  95   | false ⇒  match b2 with [ true ⇒ true | false ⇒ false ]].
  96
  97 notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
  98  for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
  99 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
 100  for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
 101
 102 theorem bool_to_decidable_eq:
 103   ∀b1,b2:bool. decidable (b1=b2).
 104 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
 105
 106 theorem true_or_false:
 107 ∀b:bool. b = true ∨ b = false.
 108 #b (cases b) /2/ qed.
 109
 110