diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
-rw-r--r-- | theories/Init/Datatypes.v | 60 |
1 files changed, 58 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 56dc7e95..e5e6fd23 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Datatypes.v 11073 2008-06-08 20:24:51Z herbelin $ i*) Set Implicit Arguments. @@ -26,6 +26,52 @@ Inductive bool : Set := Add Printing If bool. +Delimit Scope bool_scope with bool. + +Bind Scope bool_scope with bool. + +(** Basic boolean operators *) + +Definition andb (b1 b2:bool) : bool := if b1 then b2 else false. + +Definition orb (b1 b2:bool) : bool := if b1 then true else b2. + +Definition implb (b1 b2:bool) : bool := if b1 then b2 else true. + +Definition xorb (b1 b2:bool) : bool := + match b1, b2 with + | true, true => false + | true, false => true + | false, true => true + | false, false => false + end. + +Definition negb (b:bool) := if b then false else true. + +Infix "||" := orb : bool_scope. +Infix "&&" := andb : bool_scope. + +(*******************************) +(** * Properties of [andb] *) +(*******************************) + +Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. +Proof. + destruct a; destruct b; intros; split; try (reflexivity || discriminate). +Qed. +Hint Resolve andb_prop: bool v62. + +Lemma andb_true_intro : + forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true. +Proof. + destruct b1; destruct b2; simpl in |- *; tauto || auto with bool. +Qed. +Hint Resolve andb_true_intro: bool v62. + +(** Interpretation of booleans as propositions *) + +Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. + (** [nat] is the datatype of natural numbers built from [O] and successor [S]; note that the constructor name is the letter O. Numbers in [nat] can be denoted using a decimal notation; @@ -70,7 +116,7 @@ Definition option_map (A B:Type) (f:A->B) o := end. (** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *) -(* Syntax defined in Specif.v *) + Inductive sum (A B:Type) : Type := | inl : A -> sum A B | inr : B -> sum A B. @@ -82,6 +128,7 @@ Notation "x + y" := (sum x y) : type_scope. Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. + Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. @@ -135,6 +182,13 @@ Definition CompOpp (r:comparison) := | Gt => Lt end. +(** Identity *) + +Definition ID := forall A:Type, A -> A. +Definition id : ID := fun A x => x. + +(* begin hide *) + (* Compatibility *) Notation prodT := prod (only parsing). @@ -146,3 +200,5 @@ Notation fstT := fst (only parsing). Notation sndT := snd (only parsing). Notation prodT_uncurry := prod_uncurry (only parsing). Notation prodT_curry := prod_curry (only parsing). + +(* end hide *) |