weblib/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 (* destruct does not work *)
  20 theorem not_eq_true_false : true ≠ false.
  21 @nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
  22 >Heq // qed.
  23
  24 definition notb : bool → bool ≝
  25 λ b:bool. match b with [true ⇒ false|false ⇒ true ].
  26
  27 interpretation "boolean not" 'not x = (notb x).
  28
  29 theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
  30 match b with
  31 [ true ⇒ P false
  32 | false ⇒ P true] → P (notb b).
  33 #b #P elim b normalize // qed.
  34
  35 theorem notb_notb: ∀b:bool. notb (notb b) = b.
  36 #b elim b // qed.
  37
  38 theorem injective_notb: injective bool bool notb.
  39 #b1 #b2 #H // qed.
  40
  41 definition andb : bool → bool → bool ≝
  42 λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
  43
  44 interpretation "boolean and" 'and x y = (andb x y).
  45
  46 theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  47 match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
  48 #b1 #b2 #P (elim b1) normalize // qed.
  49
  50 theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
  51 #b1 (cases b1) normalize // qed.
  52
  53 theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
  54 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
  55
  56 definition orb : bool → bool → bool ≝
  57 λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
  58
  59 interpretation "boolean or" 'or x y = (orb x y).
  60
  61 theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  62 match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
  63 #b1 #b2 #P (elim b1) normalize // qed.
  64
  65 definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝
  66 λA.λb.λ P,Q:A. match b with [ true ⇒ P | false  ⇒ Q].
  67
  68 theorem bool_to_decidable_eq:
  69   ∀b1,b2:bool. decidable (b1=b2).
  70 #b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
  71
  72 theorem true_or_false:
  73 ∀b:bool. b = true ∨ b = false.
  74 #b (cases b) /2/ qed.
  75
  76