1 files changed, 77 insertions, 0 deletions
diff --git a/theories7/Bool/Sumbool.v b/theories7/Bool/Sumbool.v
new file mode 100644
index 00000000..8d55cbb6
--- /dev/null
+++ b/theories7/Bool/Sumbool.v
@@ -0,0 +1,77 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Sumbool.v,v 1.1.2.1 2004/07/16 19:31:25 herbelin Exp $ i*)
+
+(** 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 : (b:bool) {b=true}+{b=false}.
+Proof.
+  NewDestruct b; Auto.
+Defined.
+
+Hints Resolve sumbool_of_bool : bool.
+
+Definition bool_eq_rec : (b:bool)(P:bool->Set)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+NewDestruct b; Auto.
+Defined.
+
+Definition bool_eq_ind : (b:bool)(P:bool->Prop)
+                    ((b=true)->(P true))->((b=false)->(P false))->(P b).
+NewDestruct b; Auto.
+Defined.
+
+
+(*i pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno i*)
+
+(** 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}.
+Proof.
+Case H1; Case H2; Auto.
+Defined.
+
+Definition sumbool_or : {A\/C}+{B/\D}.
+Proof.
+Case H1; Case H2; Auto.
+Defined.
+
+Definition sumbool_not : {B}+{A}.
+Proof.
+Case H1; Auto.
+Defined.
+
+End connectives.
+
+Hints Resolve sumbool_and sumbool_or 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 : 
+  (A,B:Prop) {A}+{B} -> { b:bool | if b then A else B }.
+Proof.
+Intros A B H.
+Elim H; [ Intro; Exists true; Assumption
+        | Intro; Exists false; Assumption ].
+Defined.
+Implicits bool_of_sumbool.