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 *)