Fix bugs that were reopened due to the change of setoid

implementation. Mostly syntax changes when declaring parametric
relations, but also some declarations were relying on "default"
relations on some carrier. Added a new DefaultRelation type class that
allows to do that, falling back to the last declared Equivalence
relation by default. This will be bound to Add Relation in the next
commit. 

Also, move the "left" and "right" notations in Program.Utils to "in_left" and
"in_right" to avoid clashes with existing scripts.

Minor change to record to allow choosing the name of the argument for
the record in projections to avoid possible incompatibilities.


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

7 files changed, 132 insertions, 93 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index da302ea9d0..a19f8da82d 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -22,6 +22,7 @@ Require Import Coq.Program.Program.
 Require Import Coq.Classes.Init.
 Require Export Coq.Classes.Relations.
 Require Export Coq.Classes.Morphisms.
+Require Export Coq.Classes.SetoidTactics.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -47,7 +48,7 @@ Proof. eauto with typeclass_instances. Qed.
 Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope.
 
 Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope.
-
+  
 Open Local Scope equiv_scope.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
@@ -67,66 +68,6 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-Ltac setoidreplace H t :=
-  let Heq := fresh "Heq" in
-    cut(H) ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | unfold equiv ; t ].
-
-Ltac setoidreplacein H H' t :=
-  let Heq := fresh "Heq" in
-    cut(H) ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | unfold equiv ; t ].
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
-  setoidreplace (x === y) idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
-  setoidreplacein (x === y) id idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
-  setoidreplace (x === y) ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
-  setoidreplacein (x === y) id ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
-  setoidreplace (rel x y) idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
-  "using" "relation" constr(rel) "by" tactic(t) :=
-  setoidreplace (rel x y) ltac:t.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) 
-  "using" "relation" constr(rel) :=
-  setoidreplacein (rel x y) id idtac.
-
-Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
-  "using" "relation" constr(rel) "by" tactic(t) :=
-  setoidreplacein (rel x y) id ltac:t.
-
-
-Ltac red_subst_eq_morphism concl :=
-  match concl with
-    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
-    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
-    | _ => idtac
-  end.
-
-Ltac destruct_morphism :=
-  match goal with
-    | [ |- @Morphism ?A ?R ?m ] => constructor
-  end.
-
-Ltac reverse_arrows x :=
-  match x with
-    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
-    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
-    | _ => idtac
-  end.
-
-Ltac add_morphism_tactic := (try destruct_morphism) ;
-  match goal with
-    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
-  end.
-  
 Lemma nequiv_equiv_trans : forall [ ! Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
 Proof with auto.
   intros; intro.
@@ -196,21 +137,17 @@ Program Instance iff_impl_id_morphism :
 Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
   pequiv_prf :> PER carrier pequiv.
 
+Definition pequiv [ PartialEquivalence A R ] : relation A := R.
+
 (** Overloaded notation for partial equiv equivalence. *)
 
-(* Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. *)
+Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.
 
-(** Default relation on a given support. *)
-
-Class DefaultRelation A := default_relation : relation A.
-
 (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
 
 Instance [ ! Equivalence A R ] => 
-  equivalence_default : DefaultRelation A | 4 := 
-  default_relation := R.
-
+  equivalence_default : DefaultRelation A R | 4.
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v
index b14647d065..530f21264b 100644
--- a/theories/Classes/Relations.v
+++ b/theories/Classes/Relations.v
@@ -24,6 +24,17 @@ Unset Strict Implicit.
 
 Notation "'relation' A " := (A -> A -> Prop) (at level 0).
 
+(** Default relation on a given support. *)
+
+Class DefaultRelation A (R : relation A).
+
+(** To search for the default relation, just call [default_relation]. *)
+
+Definition default_relation [ DefaultRelation A R ] : relation A := R.
+
+(** A notation for applying the default relation to [x] and [y]. *)
+Notation " x ===def y " := (default_relation x y) (at level 70, no associativity).
+
 Definition inverse A (R : relation A) : relation A := fun x y => R y x.
 
 Lemma inverse_inverse : forall A (R : relation A), inverse (inverse R) = R.
diff --git a/theories/Classes/SetoidAxioms.v b/theories/Classes/SetoidAxioms.v
new file mode 100644
index 0000000000..6b7881c9f2
--- /dev/null
+++ b/theories/Classes/SetoidAxioms.v
@@ -0,0 +1,35 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Extensionality axioms that can be used when reasoning with setoids.
+ *
+ * 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 $ *)
+
+Require Import Coq.Program.Program.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.SetoidClass.
+
+(* Application of the extensionality axiom to turn a goal on leibinz equality to 
+   a setoid equivalence. *)
+
+Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+
+(** Application of the extensionality principle for setoids. *)
+
+Ltac setoid_extensionality :=
+  match goal with
+    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
+  end.
\ No newline at end of file
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8a435b4493..86a2bef80f 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -50,6 +50,8 @@ Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
 
 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).
@@ -87,7 +89,7 @@ Program Instance bool_eqdec : EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
 Program Instance unit_eqdec : EqDec (@eq_setoid unit) :=
-  equiv_dec x y := left.
+  equiv_dec x y := in_left.
 
   Next Obligation.
   Proof.
@@ -101,9 +103,9 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] =>
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
     if x1 == y1 then 
-      if x2 == y2 then left
-      else right
-    else right.
+      if x2 == y2 then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using unfold complement ; program_simpl.
 
@@ -114,9 +116,9 @@ Require Import Coq.Program.FunctionalExtensionality.
 Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
-      if f false == g false then left
-      else right
-    else right.
+      if f false == g false then in_left
+      else in_right
+    else in_right.
 
   Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
 
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 1277dcda9a..c71db69952 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -15,21 +15,80 @@
 
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
-Require Import Coq.Program.Program.
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Require Export Coq.Classes.SetoidClass.
+(** The setoid_replace tactics in Ltac, defined in terms of default relations [===def] and
+   the setoid_rewrite tactic. *)
 
-(* Application of the extensionality axiom to turn a goal on leibinz equality to 
-   a setoid equivalence. *)
+Ltac setoidreplace H t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq ; clear Heq | t ].
 
-Axiom setoideq_eq : forall [ sa : Setoid a ] (x y : a), x == y -> x = y.
+Ltac setoidreplacein H H' t :=
+  let Heq := fresh "Heq" in
+    cut(H) ; unfold default_relation ; [ intro Heq ; setoid_rewrite Heq in H' ; clear Heq | t ].
 
-(** Application of the extensionality principle for setoids. *)
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) :=
+  setoidreplace (x ===def y) idtac.
 
-Ltac setoid_extensionality :=
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) :=
+  setoidreplacein (x ===def y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic(t) :=
+  setoidreplace (x ===def y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic(t) :=
+  setoidreplacein (x ===def y) id ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) :=
+  setoidreplace (rel x y) idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) 
+  "using" "relation" constr(rel) "by" tactic(t) :=
+  setoidreplace (rel x y) ltac:t.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) 
+  "using" "relation" constr(rel) :=
+  setoidreplacein (rel x y) id idtac.
+
+Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id)
+  "using" "relation" constr(rel) "by" tactic(t) :=
+  setoidreplacein (rel x y) id ltac:t.
+
+(** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back
+   to the user to discharge the proof. It essentially amounts to unfold the right amount of [respectful] calls
+   and substitute leibniz equalities. One can redefine it using [Ltac add_morphism_tactic ::= t]. *)
+
+Require Import Coq.Program.Tactics.
+
+Ltac red_subst_eq_morphism concl :=
+  match concl with
+    | @Logic.eq ?A ==> ?R' => red ; intros ; subst ; red_subst_eq_morphism R'
+    | ?R ==> ?R' => red ; intros ; red_subst_eq_morphism R'
+    | _ => idtac
+  end.
+
+Ltac destruct_morphism :=
   match goal with
-    [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
-  end.
\ No newline at end of file
+    | [ |- @Morphism ?A ?R ?m ] => constructor
+  end.
+
+Ltac reverse_arrows x :=
+  match x with
+    | @Logic.eq ?A ==> ?R' => revert_last ; reverse_arrows R'
+    | ?R ==> ?R' => do 3 revert_last ; reverse_arrows R'
+    | _ => idtac
+  end.
+
+Ltac default_add_morphism_tactic :=
+  (try destruct_morphism) ;
+  match goal with
+    | [ |- (?x ==> ?y) _ _ ] => red_subst_eq_morphism (x ==> y) ; reverse_arrows (x ==> y)
+  end.
+
+Ltac add_morphism_tactic := default_add_morphism_tactic.
+
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index c514d3234d..184e3c3678 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -61,16 +61,10 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0).
 
 (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
 
-
-(** These type arguments should be infered from the context. *)
-
-Implicit Arguments left [[A]].
-Implicit Arguments right [[B]].
-
 (** Hide proofs and generates obligations when put in a term. *)
 
-Notation left := (left _ _).
-Notation right := (right _ _).
+Notation "'in_left'" := (@left _ _ _) : program_scope.
+Notation "'in_right'" := (@right _ _ _) : program_scope.
 
 (** Extraction directives *)
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index ff8033eeb4..6bcbbf6b70 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,6 +21,7 @@ Require Import Zbool.
 Require Import Omega.
 Require Import ZArithRing.
 Require Import Zcomplements.
+Require Export Setoid.
 Open Local Scope Z_scope.
 
 (** * Definitions of Euclidian operations *)