helm/software/matita/nlibrary/basics/bool.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/eq.ma".
  16 include "basics/functions.ma".
  17
  18 ninductive bool: Type ≝
  19   | true : bool
  20   | false : bool.
  21
  22 (*
  23 ntheorem bool_elim: \forall P:bool \to Prop. \forall b:bool.
  24   (b = true \to P true)
  25   \to (b = false \to P false)
  26   \to P b.
  27   intros 2 (P b).
  28   elim b;
  29   [ apply H; reflexivity
  30   | apply H1; reflexivity
  31   ]
  32 qed.*)
  33
  34 (* ndestrcut does not work *)
  35 ntheorem not_eq_true_false : true \neq false.
  36 #Heq; nchange with match true with [true ⇒ False|false ⇒ True];
  37 nrewrite > Heq; //; nqed.
  38
  39 ndefinition notb : bool → bool ≝
  40 \lambda b:bool. match b with
  41  [true ⇒ false
  42  |false ⇒ true ].
  43
  44 interpretation "boolean not" 'not x = (notb x).
  45
  46 ntheorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
  47 match b with
  48 [ true ⇒ P false
  49 | false ⇒ P true] → P (notb b).
  50 #b; #P; nelim b; nnormalize; //; nqed.
  51
  52 ntheorem notb_notb: ∀b:bool. notb (notb b) = b.
  53 #b; nelim b; //; nqed.
  54
  55 ntheorem injective_notb: injective bool bool notb.
  56 #b1; #b2; #H; //; nqed.
  57
  58 ndefinition andb : bool → bool → bool ≝
  59 \lambda b1,b2:bool. match b1 with
  60  [ true ⇒ b2
  61  | false ⇒ false ].
  62
  63 interpretation "boolean and" 'and x y = (andb x y).
  64
  65 ntheorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  66 match b1 with
  67  [ true ⇒ P b2
  68  | false ⇒ P false] → P (b1 ∧ b2).
  69 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
  70
  71 (*
  72 ntheorem and_true: ∀ a,b:bool.
  73 andb a b =true → a =true ∧ b= true.
  74 #a; #b; ncases a; nnormalize;#H;napply conj;//;
  75   [split
  76     [reflexivity|assumption]
  77   |apply False_ind.
  78    apply not_eq_true_false.
  79    apply sym_eq.
  80    assumption
  81   ]
  82 qed. *)
  83
  84 ntheorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
  85 #b1; ncases b1; nnormalize; //; nqed.
  86
  87 ntheorem andb_true_r: \forall b1,b2. (b1 ∧ b2) = true → b2 = true.
  88 #b1; ncases b1; nnormalize; //;
  89 #b2; ncases b2; //; nqed.
  90
  91 ndefinition orb : bool → bool → bool ≝
  92 λ b1,b2:bool.
  93  match b1 with
  94  [ true ⇒ true
  95  | false ⇒ b2].
  96
  97 interpretation "boolean or" 'or x y = (orb x y).
  98
  99 ntheorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
 100 match b1 with
 101  [ true ⇒ P true
 102  | false ⇒ P b2] → P (orb b1 b2).
 103 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
 104
 105 ndefinition if_then_else: ∀A:Type. bool → A → A → A ≝
 106 λA:Type.λb:bool.λ P,Q:A. match b with
 107  [ true ⇒ P
 108  | false  ⇒ Q].
 109
 110 ntheorem bool_to_decidable_eq:
 111  ∀b1,b2:bool. decidable (b1=b2).
 112 #b1; #b2; ncases b1; ncases b2; /2/;
 113 @2;/2/; nqed.
 114
 115 ntheorem true_or_false:
 116 ∀b:bool. b = true ∨ b = false.
 117 #b; ncases b; /2/; nqed.
 118
 119
 120 (*
 121 theorem P_x_to_P_x_to_eq:
 122  \forall A:Set. \forall P: A \to bool.
 123   \forall x:A. \forall p1,p2:P x = true. p1 = p2.
 124  intros.
 125  apply eq_to_eq_to_eq_p_q.
 126  exact bool_to_decidable_eq.
 127 qed.
 128
 129
 130 (* some basic properties of and - or*)
 131 theorem andb_sym: \forall A,B:bool.
 132 (A \land B) = (B \land A).
 133 intros.
 134 elim A;
 135   elim B;
 136     simplify;
 137     reflexivity.
 138 qed.
 139
 140 theorem andb_assoc: \forall A,B,C:bool.
 141 (A \land (B \land C)) = ((A \land B) \land C).
 142 intros.
 143 elim A;
 144   elim B;
 145     elim C;
 146       simplify;
 147       reflexivity.
 148 qed.
 149
 150 theorem orb_sym: \forall A,B:bool.
 151 (A \lor B) = (B \lor A).
 152 intros.
 153 elim A;
 154   elim B;
 155     simplify;
 156     reflexivity.
 157 qed.
 158
 159 theorem true_to_true_to_andb_true: \forall A,B:bool.
 160 A = true \to B = true \to (A \land B) = true.
 161 intros.
 162 rewrite > H.
 163 rewrite > H1.
 164 reflexivity.
 165 qed. *)