diff options
Diffstat (limited to 'theories7/Bool/Sumbool.v')
-rw-r--r-- | theories7/Bool/Sumbool.v | 77 |
1 files changed, 0 insertions, 77 deletions
diff --git a/theories7/Bool/Sumbool.v b/theories7/Bool/Sumbool.v deleted file mode 100644 index 8d55cbb6..00000000 --- a/theories7/Bool/Sumbool.v +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* 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. |