diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
-rw-r--r-- | theories/Init/Datatypes.v | 101 |
1 files changed, 93 insertions, 8 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 0163c01c..6040f58b 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,12 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) Set Implicit Arguments. Require Import Notations. Require Import Logic. +Declare ML Module "nat_syntax_plugin". + (** [unit] is a singleton datatype with sole inhabitant [tt] *) @@ -72,6 +74,16 @@ Hint Resolve andb_true_intro: bool. Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. +Hint Constructors eq_true : eq_true. + +(** Another way of interpreting booleans as propositions *) + +Definition is_true b := b = true. + +(** [is_true] can be activated as a coercion by + (Local) Coercion is_true : bool >-> Prop. +*) + (** Additional rewriting lemmas about [eq_true] *) Lemma eq_true_ind_r : @@ -94,7 +106,7 @@ Defined. (** [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; + Numbers in [nat] can be denoted using a decimal notation; e.g. [3%nat] abbreviates [S (S (S O))] *) Inductive nat : Set := @@ -114,8 +126,8 @@ Inductive Empty_set : Set :=. sole inhabitant is denoted [refl_identity A a] *) Inductive identity (A:Type) (a:A) : A -> Type := - refl_identity : identity (A:=A) a a. -Hint Resolve refl_identity: core. + identity_refl : identity a a. +Hint Resolve identity_refl: core. Implicit Arguments identity_ind [A]. Implicit Arguments identity_rec [A]. @@ -162,7 +174,7 @@ Section projections. Definition snd (p:A * B) := match p with | (x, y) => y end. -End projections. +End projections. Hint Resolve pair inl inr: core. @@ -177,13 +189,13 @@ Lemma injective_projections : fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2. Proof. destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd. - rewrite Hfst; rewrite Hsnd; reflexivity. + rewrite Hfst; rewrite Hsnd; reflexivity. Qed. -Definition prod_uncurry (A B C:Type) (f:prod A B -> C) +Definition prod_uncurry (A B C:Type) (f:prod A B -> C) (x:A) (y:B) : C := f (pair x y). -Definition prod_curry (A B C:Type) (f:A -> B -> C) +Definition prod_curry (A B C:Type) (f:A -> B -> C) (p:prod A B) : C := match p with | pair x y => f x y end. @@ -202,11 +214,84 @@ Definition CompOpp (r:comparison) := | Gt => Lt end. +Lemma CompOpp_involutive : forall c, CompOpp (CompOpp c) = c. +Proof. + destruct c; reflexivity. +Qed. + +Lemma CompOpp_inj : forall c c', CompOpp c = CompOpp c' -> c = c'. +Proof. + destruct c; destruct c'; auto; discriminate. +Qed. + +Lemma CompOpp_iff : forall c c', CompOpp c = c' <-> c = CompOpp c'. +Proof. + split; intros; apply CompOpp_inj; rewrite CompOpp_involutive; auto. +Qed. + +(** The [CompSpec] inductive will be used to relate a [compare] function + (returning a comparison answer) and some equality and order predicates. + Interest: [CompSpec] behave nicely with [case] and [destruct]. *) + +Inductive CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := + | CompEq : eq x y -> CompSpec eq lt x y Eq + | CompLt : lt x y -> CompSpec eq lt x y Lt + | CompGt : lt y x -> CompSpec eq lt x y Gt. +Hint Constructors CompSpec. + +(** For having clean interfaces after extraction, [CompSpec] is declared + in Prop. For some situations, it is nonetheless useful to have a + version in Type. Interestingly, these two versions are equivalent. +*) + +Inductive CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := + | CompEqT : eq x y -> CompSpecT eq lt x y Eq + | CompLtT : lt x y -> CompSpecT eq lt x y Lt + | CompGtT : lt y x -> CompSpecT eq lt x y Gt. +Hint Constructors CompSpecT. + +Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, + CompSpec eq lt x y c -> CompSpecT eq lt x y c. +Proof. + destruct c; intros H; constructor; inversion_clear H; auto. +Defined. + (** Identity *) Definition ID := forall A:Type, A -> A. Definition id : ID := fun A x => x. +(** Polymorphic lists and some operations *) + +Inductive list (A : Type) : Type := + | nil : list A + | cons : A -> list A -> list A. + +Implicit Arguments nil [A]. +Infix "::" := cons (at level 60, right associativity) : list_scope. +Delimit Scope list_scope with list. +Bind Scope list_scope with list. + +Local Open Scope list_scope. + +Definition length (A : Type) : list A -> nat := + fix length l := + match l with + | nil => O + | _ :: l' => S (length l') + end. + +(** Concatenation of two lists *) + +Definition app (A : Type) : list A -> list A -> list A := + fix app l m := + match l with + | nil => m + | a :: l1 => a :: app l1 m + end. + +Infix "++" := app (right associativity, at level 60) : list_scope. + (* begin hide *) (* Compatibility *) |