diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r-- | theories/Init/Datatypes.v | 182 |
1 files changed, 115 insertions, 67 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index deadec43..41f6b70b 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -1,25 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Datatypes.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Set Implicit Arguments. Require Import Notations. Require Import Logic. Declare ML Module "nat_syntax_plugin". +(********************************************************************) +(** * Datatypes with zero and one element *) + +(** [Empty_set] is a datatype with no inhabitant *) + +Inductive Empty_set : Set :=. (** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. + +(********************************************************************) +(** * The boolean datatype *) + (** [bool] is the datatype of the boolean values [true] and [false] *) Inductive bool : Set := @@ -53,9 +61,7 @@ Definition negb (b:bool) := if b then false else true. Infix "||" := orb : bool_scope. Infix "&&" := andb : bool_scope. -(*******************************) -(** * Properties of [andb] *) -(*******************************) +(** Basic properties of [andb] *) Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true. Proof. @@ -104,6 +110,22 @@ Proof. intros P b H H0; destruct H0 in H; assumption. Defined. +(** The [BoolSpec] inductive will be used to relate a [boolean] value + and two propositions corresponding respectively to the [true] + case and the [false] case. + Interest: [BoolSpec] behave nicely with [case] and [destruct]. + See also [Bool.reflect] when [Q = ~P]. +*) + +Inductive BoolSpec (P Q : Prop) : bool -> Prop := + | BoolSpecT : P -> BoolSpec P Q true + | BoolSpecF : Q -> BoolSpec P Q false. +Hint Constructors BoolSpec. + + +(********************************************************************) +(** * Peano natural numbers *) + (** [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; @@ -115,23 +137,11 @@ Inductive nat : Set := Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. -Arguments Scope S [nat_scope]. +Arguments S _%nat. -(** [Empty_set] has no inhabitant *) -Inductive Empty_set : Set :=. - -(** [identity A a] is the family of datatypes on [A] whose sole non-empty - member is the singleton datatype [identity A a a] whose - sole inhabitant is denoted [refl_identity A a] *) - -Inductive identity (A:Type) (a:A) : A -> Type := - identity_refl : identity a a. -Hint Resolve identity_refl: core. - -Implicit Arguments identity_ind [A]. -Implicit Arguments identity_rec [A]. -Implicit Arguments identity_rect [A]. +(********************************************************************) +(** * Container datatypes *) (** [option A] is the extension of [A] with an extra element [None] *) @@ -139,7 +149,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. -Implicit Arguments None [A]. +Arguments None [A]. Definition option_map (A B:Type) (f:A->B) o := match o with @@ -155,6 +165,9 @@ Inductive sum (A B:Type) : Type := Notation "x + y" := (sum x y) : type_scope. +Arguments inl {A B} _ , [A] B _. +Arguments inr {A B} _ , A [B] _. + (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) @@ -166,6 +179,8 @@ Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. +Arguments pair {A B} _ _. + Section projections. Variables A B : Type. Definition fst (p:A * B) := match p with @@ -200,7 +215,40 @@ Definition prod_curry (A B C:Type) (f:A -> B -> C) | pair x y => f x y end. -(** Comparison *) +(** Polymorphic lists and some operations *) + +Inductive list (A : Type) : Type := + | nil : list A + | cons : A -> list A -> list A. + +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. + + +(********************************************************************) +(** * The comparison datatype *) Inductive comparison : Set := | Eq : comparison @@ -229,68 +277,68 @@ 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]. *) +(** The [CompareSpec] inductive relates a [comparison] value with three + propositions, one for each possible case. Typically, it can be used to + specify a comparison function via some equality and order predicates. + Interest: [CompareSpec] 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. +Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := + | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq + | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt + | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. +Hint Constructors CompareSpec. -(** For having clean interfaces after extraction, [CompSpec] is declared +(** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a - version in Type. Interestingly, these two versions are equivalent. -*) + 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. +Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := + | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq + | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt + | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. +Hint Constructors CompareSpecT. -Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, - CompSpec eq lt x y c -> CompSpecT eq lt x y c. +Lemma CompareSpec2Type : forall Peq Plt Pgt c, + CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. Proof. destruct c; intros H; constructor; inversion_clear H; auto. Defined. -(** Identity *) +(** As an alternate formulation, one may also directly refer to predicates + [eq] and [lt] for specifying a comparison, rather that fully-applied + propositions. This [CompSpec] is now a particular case of [CompareSpec]. *) -Definition ID := forall A:Type, A -> A. -Definition id : ID := fun A x => x. +Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := + CompareSpec (eq x y) (lt x y) (lt y x). +Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := + CompareSpecT (eq x y) (lt x y) (lt y x). +Hint Unfold CompSpec CompSpecT. -(** Polymorphic lists and some operations *) +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. intros. apply CompareSpec2Type; assumption. Defined. -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. +(******************************************************************) +(** * Misc Other Datatypes *) -Local Open Scope list_scope. +(** [identity A a] is the family of datatypes on [A] whose sole non-empty + member is the singleton datatype [identity A a a] whose + sole inhabitant is denoted [refl_identity A a] *) -Definition length (A : Type) : list A -> nat := - fix length l := - match l with - | nil => O - | _ :: l' => S (length l') - end. +Inductive identity (A:Type) (a:A) : A -> Type := + identity_refl : identity a a. +Hint Resolve identity_refl: core. -(** Concatenation of two lists *) +Arguments identity_ind [A] a P f y i. +Arguments identity_rec [A] a P f y i. +Arguments identity_rect [A] a P f y i. -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. +(** Identity type *) + +Definition ID := forall A:Type, A -> A. +Definition id : ID := fun A x => x. -Infix "++" := app (right associativity, at level 60) : list_scope. (* begin hide *) |