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 napply nmk; #Heq;
  37 nchange with match true with [true ⇒ False|false ⇒ True];
  38 nrewrite > Heq; //; nqed.
  39
  40 ndefinition notb : bool → bool ≝
  41 \lambda b:bool. match b with
  42  [true ⇒ false
  43  |false ⇒ true ].
  44
  45 interpretation "boolean not" 'not x = (notb x).
  46
  47 ntheorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
  48 match b with
  49 [ true ⇒ P false
  50 | false ⇒ P true] → P (notb b).
  51 #b; #P; nelim b; nnormalize; //; nqed.
  52
  53 ntheorem notb_notb: ∀b:bool. notb (notb b) = b.
  54 #b; nelim b; //; nqed.
  55
  56 ntheorem injective_notb: injective bool bool notb.
  57 #b1; #b2; #H; //; nqed.
  58
  59 ndefinition andb : bool → bool → bool ≝
  60 \lambda b1,b2:bool. match b1 with
  61  [ true ⇒ b2
  62  | false ⇒ false ].
  63
  64 interpretation "boolean and" 'and x y = (andb x y).
  65
  66 ntheorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
  67 match b1 with
  68  [ true ⇒ P b2
  69  | false ⇒ P false] → P (b1 ∧ b2).
  70 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
  71
  72 (*
  73 ntheorem and_true: ∀ a,b:bool.
  74 andb a b =true → a =true ∧ b= true.
  75 #a; #b; ncases a; nnormalize;#H;napply conj;//;
  76   [split
  77     [reflexivity|assumption]
  78   |apply False_ind.
  79    apply not_eq_true_false.
  80    apply sym_eq.
  81    assumption
  82   ]
  83 qed. *)
  84
  85 ntheorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
  86 #b1; ncases b1; nnormalize; //; nqed.
  87
  88 ntheorem andb_true_r: \forall b1,b2. (b1 ∧ b2) = true → b2 = true.
  89 #b1; ncases b1; nnormalize; //;
  90 #b2; ncases b2; //; nqed.
  91
  92 ndefinition orb : bool → bool → bool ≝
  93 λ b1,b2:bool.
  94  match b1 with
  95  [ true ⇒ true
  96  | false ⇒ b2].
  97
  98 interpretation "boolean or" 'or x y = (orb x y).
  99
 100 ntheorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
 101 match b1 with
 102  [ true ⇒ P true
 103  | false ⇒ P b2] → P (orb b1 b2).
 104 #b1; #b2; #P; nelim b1; nnormalize; //; nqed.
 105
 106 ndefinition if_then_else: ∀A:Type. bool → A → A → A ≝
 107 λA:Type.λb:bool.λ P,Q:A. match b with
 108  [ true ⇒ P
 109  | false  ⇒ Q].
 110
 111 (*
 112 ntheorem fff: false ≠ true.
 113 /2/;
 114 //; nqed. *)
 115
 116 ntheorem bool_to_decidable_eq:
 117  ∀b1,b2:bool. decidable (b1=b2).
 118 #b1; #b2; ncases b1; ncases b2; /2/;
 119 @2;/3/; nqed.
 120
 121 ntheorem true_or_false:
 122 ∀b:bool. b = true ∨ b = false.
 123 #b; ncases b; /2/; nqed.
 124
 125
 126 (*
 127 theorem P_x_to_P_x_to_eq:
 128  \forall A:Set. \forall P: A \to bool.
 129   \forall x:A. \forall p1,p2:P x = true. p1 = p2.
 130  intros.
 131  apply eq_to_eq_to_eq_p_q.
 132  exact bool_to_decidable_eq.
 133 qed.
 134
 135
 136 (* some basic properties of and - or*)
 137 theorem andb_sym: \forall A,B:bool.
 138 (A \land B) = (B \land A).
 139 intros.
 140 elim A;
 141   elim B;
 142     simplify;
 143     reflexivity.
 144 qed.
 145
 146 theorem andb_assoc: \forall A,B,C:bool.
 147 (A \land (B \land C)) = ((A \land B) \land C).
 148 intros.
 149 elim A;
 150   elim B;
 151     elim C;
 152       simplify;
 153       reflexivity.
 154 qed.
 155
 156 theorem orb_sym: \forall A,B:bool.
 157 (A \lor B) = (B \lor A).
 158 intros.
 159 elim A;
 160   elim B;
 161     simplify;
 162     reflexivity.
 163 qed.
 164
 165 theorem true_to_true_to_andb_true: \forall A,B:bool.
 166 A = true \to B = true \to (A \land B) = true.
 167 intros.
 168 rewrite > H.
 169 rewrite > H1.
 170 reflexivity.
 171 qed. *)