Fix Makefile bug, using .v instead of .vo and document SetoidDec.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10447 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 49 insertions, 29 deletions

diff --git a/Makefile.common b/Makefile.common
index a9a6ca8fa4..82afd575d8 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -707,8 +707,8 @@ SETOIDSVO:= theories/Setoids/Setoid_tac.vo theories/Setoids/Setoid_Prop.vo theor
 
 UNICODEVO:= theories/Unicode/Utf8.vo
 
-CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.v \
-	theories/Classes/SetoidDec.v
+CLASSESVO:= theories/Classes/Init.vo theories/Classes/SetoidClass.vo theories/Classes/SetoidTactics.vo \
+	theories/Classes/SetoidDec.vo
 
 THEORIESVO:=\
   $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index cd96269f8f..a9f2ae6de9 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -7,7 +7,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Certified Haskell Prelude.
+(* Decidable setoid equality theory.
+ *
  * Author: Matthieu Sozeau
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
@@ -19,17 +20,31 @@ Unset Strict Implicit.
 
 Require Import Coq.Classes.SetoidClass.
 
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
 Class [ Setoid A R ] => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =!= y }.
 
+(** We define the [==] overloaded notation for deciding equality. It does not take precedence
+   of [==] defined in the type scope, hence we can have both at the same time. *)
+
 Infix "==" := equiv_dec (no associativity, at level 70).
 
+(** Use program to solve some obligations. *)
+
 Require Import Coq.Program.Program.
 
+(** Invert the branches. *)
+
 Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =!= y } + { x == y } :=
   if x == y then right else left.
 
-Infix "<>" := nequiv_dec (no associativity, at level 70).
+(** Overloaded notation for inequality. *)
+
+Infix "=!=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
 
 Definition equiv_decb [ EqDec A R ] (x y : A) : bool :=
   if x == y then true else false.
@@ -57,11 +72,11 @@ Program Instance bool_eqdec : EqDec bool eq :=
 Program Instance unit_eqdec : EqDec unit eq :=
   equiv_dec x y := left.
 
-Next Obligation.
-Proof.
-  destruct x ; destruct y.
-  reflexivity.
-Qed.
+  Next Obligation.
+  Proof.
+    destruct x ; destruct y.
+    reflexivity.
+  Qed.
 
 Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq :=
   equiv_dec x y := 
@@ -72,7 +87,11 @@ Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq
       else right
     else right.
 
-Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates.
+  Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates.
+
+(** Objects of function spaces with countable domains like bool have decidable equality. *)
+
+Require Import Coq.Program.FunctionalExtensionality.
 
 Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
   equiv_dec f g := 
@@ -81,20 +100,18 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
       else right
     else right.
 
-Solve Obligations using unfold equiv ; program_simpl.
-
-Require Import Coq.Program.FunctionalExtensionality.
-
-Next Obligation.
-Proof.
-  unfold equiv.
-  extensionality x.
-  destruct x ; auto.
-Qed.
-
-Next Obligation.
-Proof.
-  unfold equiv in *.
-  red ; intro ; subst.
-  discriminates.
-Qed.
+  Solve Obligations using unfold equiv ; program_simpl.
+
+  Next Obligation.
+  Proof.
+    unfold equiv.
+    extensionality x.
+    destruct x ; auto.
+  Qed.
+  
+  Next Obligation.
+  Proof.
+    unfold equiv in *.
+    red ; intro ; subst.
+    discriminates.
+  Qed.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 65b2968ccd..540ac184e6 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -7,7 +7,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Certified Haskell Prelude.
+(* Tactics for typeclass-based setoids.
+ *
  * Author: Matthieu Sozeau
  * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
  *              91405 Orsay, France *)
@@ -21,7 +22,8 @@ Unset Strict Implicit.
 
 Require Export Coq.Classes.SetoidClass.
 
-Ltac rew H := clrewrite H.
+(* Application of the extensionality axiom to turn a goal on leibinz equality to 
+   a setoid equivalence. *)
 
 Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y.
 Proof.
@@ -31,6 +33,7 @@ Qed.
 Implicit Arguments setoideq_eq [[a] [eqa] [sa]].
 
 (** Application of the extensionality principle for setoids. *)
+
 Ltac setoideq_ext :=
   match goal with
     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y)