6 files changed, 150 insertions, 34 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
new file mode 100644
index 000000000..085023720
--- /dev/null
+++ b/theories/Classes/EquivDec.v
@@ -0,0 +1,138 @@
+(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Decidable equivalences.
+ *
+ * Author: Matthieu Sozeau
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ *              91405 Orsay, France *)
+
+(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** Export notations. *)
+
+Require Export Coq.Classes.Equivalence.
+
+(** The [DecidableSetoid] class asserts decidability of a [Setoid]. It can be useful in proofs to reason more 
+   classically. *)
+
+Require Import Coq.Logic.Decidable.
+
+Open Scope equiv_scope.
+
+Class [ Equivalence A ] => DecidableEquivalence :=
+  setoid_decidable : forall x y : A, decidable (x === y).
+
+(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
+
+Class [ Equivalence A ] => 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. *)
+
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+
+Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
+  match x with
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
+  end.
+
+Require Import Coq.Program.Program.
+
+Open Local Scope program_scope.
+
+(** Invert the branches. *)
+
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y } := swap_sumbool (x == y).
+
+(** Overloaded notation for inequality. *)
+
+Infix "=/=" := nequiv_dec (no associativity, at level 70).
+
+(** Define boolean versions, losing the logical information. *)
+
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
+  if x == y then true else false.
+
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
+  negb (equiv_decb x y).
+
+Infix "==b" := equiv_decb (no associativity, at level 70).
+Infix "<>b" := nequiv_decb (no associativity, at level 70).
+
+(** Decidable leibniz equality instances. *)
+
+Require Import Coq.Arith.Peano_dec.
+
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance nat_eq_eqdec : ! EqDec nat eq :=
+  equiv_dec := eq_nat_dec.
+
+Require Import Coq.Bool.Bool.
+
+Program Instance bool_eqdec : ! EqDec bool eq :=
+  equiv_dec := bool_dec.
+
+Program Instance unit_eqdec : ! EqDec unit eq :=
+  equiv_dec x y := in_left.
+
+  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 := 
+    dest x as (x1, x2) in 
+    dest y as (y1, y2) in 
+    if x1 == y1 then 
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using unfold complement, equiv ; program_simpl.
+
+Program Instance [ EqDec A eq, EqDec B eq ] => 
+  sum_eqdec : ! EqDec (sum A B) eq :=
+  equiv_dec x y := 
+    match x, y with
+      | inl a, inl b => if a == b then in_left else in_right
+      | inr a, inr b => if a == b then in_left else in_right
+      | inl _, inr _ | inr _, inl _ => in_right
+    end.
+
+  Solve Obligations using unfold complement, equiv ; program_simpl.
+
+(** 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 := 
+    if f true == g true then
+      if f false == g false then in_left
+      else in_right
+    else in_right.
+
+  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
+
+  Next Obligation.
+  Proof.
+    red.
+    extensionality x.
+    destruct x ; auto.
+  Qed.
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 00519ecf4..a4c97fc82 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -109,8 +109,8 @@ Ltac equiv_simplify := repeat equiv_simplify_one.
 
 Ltac equivify_tac :=
   match goal with
-    | [ s : Equivalence ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Equivalence ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+    | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Equivalence ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
   end.
 
 Ltac equivify := repeat equivify_tac.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index eda2aecaa..b4b217e38 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -453,8 +453,7 @@ Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : r
   inverse (R ==> R') ==rel (inverse R ==> inverse R').
 Proof.
   intros.
-  unfold inverse, flip.
-  unfold respectful.
+  unfold flip, respectful.
   split ; intros ; intuition.
 Qed.
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0ca074589..009ee1e86 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -36,7 +36,9 @@ Definition default_relation [ DefaultRelation A R ] : relation A := R.
 
 Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
 
-Definition inverse {A} : relation A -> relation A := flip.
+Notation "'inverse' R" := (flip (R:relation _) : relation _) (at level 0).
+
+(* Definition inverse {A} : relation A -> relation A := flip. *)
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
 
@@ -93,26 +95,6 @@ Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R).
 
   Solve Obligations using unfold flip ; program_simpl ; clapply transitivity.
 
-(** Have to do it again for Prop. *)
-
-Program Instance [ Reflexive A (R : relation A) ] => inverse_Reflexive : Reflexive (inverse R) :=
-  reflexivity := reflexivity (R:=R).
-
-Program Instance [ Irreflexive A (R : relation A) ] => inverse_Irreflexive : Irreflexive (inverse R) :=
-  irreflexivity := irreflexivity (R:=R).
-
-Program Instance [ Symmetric A (R : relation A) ] => inverse_Symmetric : Symmetric (inverse R).
-
-  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply Symmetric.
-
-Program Instance [ Asymmetric A (R : relation A) ] => inverse_Asymmetric : Asymmetric (inverse R).
-  
-  Solve Obligations using program_simpl ; unfold inverse, flip in * ; intros ; clapply asymmetry.
-
-Program Instance [ Transitive A (R : relation A) ] => inverse_Transitive : Transitive (inverse R).
-
-  Solve Obligations using unfold inverse, flip ; program_simpl ; clapply transitivity.
-
 Program Instance [ Reflexive A (R : relation A) ] => 
   Reflexive_complement_Irreflexive : Irreflexive (complement R).
 
@@ -148,7 +130,7 @@ Tactic Notation "apply" "*" constr(t) :=
     refine (t _ _ _ _ _) | refine (t _ _ _ _ _ _) | refine (t _ _ _ _ _ _ _) ].
 
 Ltac simpl_relation :=
-  unfold inverse, flip, impl, arrow ; try reduce ; program_simpl ;
+  unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
 Ltac obligations_tactic ::= simpl_relation.
@@ -213,12 +195,11 @@ Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) :=
 Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] => 
   flip_antiSymmetric : Antisymmetric eq (flip R).
 
-Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq (R : relation A) ] => 
-  inverse_antiSymmetric : Antisymmetric eq (inverse R).
-
-(** Leibinz equality [eq] is an equivalence relation. *)
+(** Leibinz equality [eq] is an equivalence relation.
+   The instance has low priority as it is always applicable 
+   if only the type is constrained. *)
 
-Program Instance eq_equivalence : Equivalence A (@eq A).
+Program Instance eq_equivalence : Equivalence A (@eq A) | 10.
 
 (** Logical equivalence [iff] is an equivalence relation. *)
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d4da4b8df..d370ffa44 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism.
+  Reflexive_partial_app_morphism x.
 
 Existing Instance setoid_partial_app_morphism.
 
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 26e1ab244..835294ce3 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -40,8 +40,6 @@ Class [ Setoid A ] => EqDec :=
 
 Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
 
-(** Use program to solve some obligations. *)
-
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
     | left H => @right _ _ H