mise sous CVS

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@318 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 48 insertions, 0 deletions

diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v
new file mode 100644
index 000000000..a7d600289
--- /dev/null
+++ b/theories/Bool/Sumbool.v
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(* 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 *)
+
+Lemma sumbool_of_bool : (b:bool) {b=true}+{b=false}.
+Proof.
+  Induction b; Auto.
+Save.
+
+Hints Resolve sumbool_of_bool : bool.
+
+(* pourquoi ce machin-la est dans BOOL et pas dans LOGIC ?  Papageno *)
+
+(* Logic connectives on type sumbool *)
+
+Section connectives.
+
+Variables A,B,C,D : Prop.
+
+Hypothesis H1 : {A}+{B}.
+Hypothesis H2 : {C}+{D}.
+
+Lemma sumbool_and : {A/\C}+{B\/D}.
+Proof.
+Case H1; Case H2; Auto.
+Save.
+
+Lemma sumbool_or : {A\/C}+{B/\D}.
+Proof.
+Case H1; Case H2; Auto.
+Save.
+
+Lemma sumbool_not : {B}+{A}.
+Proof.
+Case H1; Auto.
+Save.
+
+End connectives.
+
+Hints Resolve sumbool_and sumbool_or sumbool_not : core.