Library Bool_ext

Require Import Bool.
Export Bool.

Lemma negb_false_is_true : forall x, negb x = false -> x = true.

Lemma negb_true_is_false : forall x, negb x = true -> x = false.

Definition bool_eq (a b : bool) : bool :=
  match (a, b) with
    | (true, true) => true
    | (false, false) => true
    | _ => false
  end.


Lemma bool_eq_refl: forall a, bool_eq a a = true.

Lemma bool_eq_eq: forall a b, bool_eq a b = true -> a = b.

Lemma bool_eq_classic: forall a b, bool_eq a b = true \/ bool_eq a b = false.

Lemma bool_eq_false_not_eq : forall a b, bool_eq a b = false -> a <> b.

Lemma not_eq_false_bool_eq : forall a b, a <> b -> bool_eq a b = false.

Definition andb_option (a b : option bool) :=
  match a with
    | None => None
    | Some a' => match b with
                   | None => None
                   | Some b' => Some (andb a' b')
                 end
  end.

Definition orb_option (a b : option bool) :=
  match a with
    | None => None
    | Some a' => match b with
                   | None => None
                   | Some b' => Some (orb a' b')
                 end
  end.