# Library Coq.Bool.Sumbool

``` ```
Here are collected some results about the type sumbool (see INIT/Specif.v) `sumbool A B`, which is written `{A}+{B}`, is the informative disjunction "A or B", where A and B are logical propositions. Its extraction is isomorphic to the type of booleans.
``` ```
A boolean is either `true` or `false`, and this is decidable
``` Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}.   destruct b; auto. Defined. Hint Resolve sumbool_of_bool: bool. Definition bool_eq_rec :   forall (b:bool) (P:bool -> Set),     (b = true -> P true) -> (b = false -> P false) -> P b.   destruct b; auto. Defined. Definition bool_eq_ind :   forall (b:bool) (P:bool -> Prop),     (b = true -> P true) -> (b = false -> P false) -> P b.   destruct b; auto. Defined. ```
Logic connectives on type `sumbool`
``` Section connectives.   Variables A B C D : Prop.   Hypothesis H1 : {A} + {B}.   Hypothesis H2 : {C} + {D}.   Definition sumbool_and : {A /\ C} + {B \/ D}.     case H1; case H2; auto.   Defined.   Definition sumbool_or : {A \/ C} + {B /\ D}.     case H1; case H2; auto.   Defined.   Definition sumbool_not : {B} + {A}.     case H1; auto.   Defined. End connectives. Hint Resolve sumbool_and sumbool_or: core. Hint Immediate sumbool_not : core. ```
Any decidability function in type `sumbool` can be turned into a function returning a boolean with the corresponding specification:
``` Definition bool_of_sumbool :   forall A B:Prop, {A} + {B} -> {b : bool | if b then A else B}.   intros A B H.   elim H; intro; [exists true | exists false]; assumption. Defined. Implicit Arguments bool_of_sumbool. ```