diff options
Diffstat (limited to 'theories/Bool/Sumbool.v')
| -rw-r--r-- | theories/Bool/Sumbool.v | 49 |
1 files changed, 21 insertions, 28 deletions
diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 2842437d..0da72f56 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Sumbool.v 7235 2005-07-15 17:11:57Z coq $ i*) +(*i $Id: Sumbool.v 9245 2006-10-17 12:53:34Z notin $ 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 @@ -16,7 +16,6 @@ (** A boolean is either [true] or [false], and this is decidable *) Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. -Proof. destruct b; auto. Defined. @@ -25,41 +24,36 @@ 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. + 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. + destruct 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. + 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. @@ -71,8 +65,7 @@ Hint Immediate sumbool_not : core. Definition bool_of_sumbool : forall 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 ]. + intros A B H. + elim H; intro; [exists true | exists false]; assumption. Defined. Implicit Arguments bool_of_sumbool.
\ No newline at end of file |