Document CHANGES in setoid rewrite, move DefaultRelation to

SetoidTactics and document it. Cleanup Classes.Equivalence.
Minor fixes to the Program doc.


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

6 files changed, 137 insertions, 113 deletions

diff --git a/CHANGES b/CHANGES
index 25822d4920..506da926d0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -90,8 +90,8 @@ Notations and implicit arguments
 - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
   Implicit", "Set Strongly Strict Implicit" and "Set Printing Implicit
   Defensive" for controlling inference and use of implicit arguments.
-- New modifiers in "Implicit Arguments" to force an implicit argument to
-  be maximally inserted and/or forced if it is not seen as inferable.
+- New modifier in "Implicit Arguments" to force an implicit argument to
+  be maximally inserted.
 - New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
   (DOC TODO?)
 - New options Global and Local to "Implicit Arguments" for section
@@ -147,10 +147,12 @@ Tactics
   intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
   is still legal but equivalent to intros ?a ?b.
 - New intro pattern "{A,B,C}" synonym to "(A,(B,C))"
+- rewrite now supports "by" to solve side-conditions and "at" to select
+  occurrences.
 - New syntax "rewrite A,B" for "rewrite A; rewrite B"
 - New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
-- New tactic "dependent induction H [ generalizing id_1 .. id_n ]" to do 
-  induction-inversion on instantiated inductive families à la BasicElim.
+- New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" 
+  to do induction-inversion on instantiated inductive families à la BasicElim.
 - Tactic "apply" now able to reason modulo unfolding of constants
   (possible source of incompatibility in situations where apply may fail, 
   e.g. as argument of a try or a repeat and in a ltac function);
@@ -160,24 +162,6 @@ Tactics
   matching lemma among the components of the conjunction; tactic apply also
   able to apply lemmas of conclusion an empty type.
 
-Type Classes
-
-- New "Class", "Instance" and "Program Instance" commands to define
-  classes and instances documented in the reference manual.  
-- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " 
-  for binding type classes, usable everywhere.  
-- New command " Print Classes " and " Print Instances some_class " to
-  print tables for typeclasses.  
-- New default eauto hint database "typeclass_instances" used by the default
-  typeclass instance search tactic.  
-- New theories directory "theories/Classes" for standard typeclasses 
-  declarations. Module Classes.Relations is a typeclass port of 
-  Relation_Definitions.
-- New experimental "setoid" rewriting tactic based on typeclasses.
-  Classes.Morphisms declares standard morphisms, Classes.Equivalence declares 
-  the new Setoid typeclass and some derived tactics (source of
-  incompatibilities: 1- Setoid has to be required first 2- ...)
-  
 Program
 
 - Moved useful tactics in theories/Program and documented them.
@@ -194,10 +178,89 @@ Program
   iff they can be automatically solved by the default tactic.
 - New command "Preterm [ of id ]" to see the actual term fed to Coq for
   debugging purposes.
+- New option "Transparent Obligations" to force the declaration of 
+  all obligations as transparent.
 - Changed the notations "left" and "right" to "in_left" and "in_right" to hide 
   the proofs in standard disjunctions, to avoid breaking existing scripts when 
   importing Program. Also, put them in program_scope.
+
+Type Classes
+
+- New "Class", "Instance" and "Program Instance" commands to define
+  classes and instances documented in the reference manual.  
+- New binding construct " [ Class_1 param_1 .. param_n, Class_2 ... ] " 
+  for binding type classes, usable everywhere.  
+- New command " Print Classes " and " Print Instances some_class " to
+  print tables for typeclasses.  
+- New default eauto hint database "typeclass_instances" used by the default
+  typeclass instance search tactic.  
+- New theories directory "theories/Classes" for standard typeclasses 
+  declarations. Module Classes.RelationClasses is a typeclass port of 
+  Relation_Definitions plus a generic development of algebra on 
+  n-ary heterogeneous predicates.
   
+Setoid rewriting
+
+- Complete (and still experimental) rewrite of the tactic
+  based on typeclasses. The old interface and semantics are
+  almost entirely respected, except:
+
+  - Import Setoid is now mandatory to be able to call setoid_replace
+  and declare morphisms.
+
+  - "-->", "++>" and "==>" are now right associative notations
+  declared at level 55 in scope signature_scope.
+  Their introduction may break existing scripts that defined 
+  them as notations with different levels.
+  
+  - One needs to use [Typeclasses unfold [cst]] if [cst] is used
+  as an abbreviation hiding products in types of morphisms,
+  e.g. if ones redefines [relation] and declares morphisms 
+  whose type mentions [relation].
+
+  - The [setoid_rewrite]'s semantics change when rewriting with
+  a lemma: it can rewrite two different instantiations of the lemma
+  at once. Use [setoid_rewrite H at 1] for (almost) the usual semantics.
+  [setoid_rewrite] will also try to rewrite under binders now, and can
+  succeed on different terms than before. In particular, it will unify under 
+  let-bound variables. When called through [rewrite], the semantics are
+  unchanged though.
+
+  - [Add Morphism term : id] has different semantics when used with
+  parametric morphism: it will try to find a relation on the parameters
+  too. The behavior has also changed with respect to default relations:
+  the most recently declared Setoid/Relation will be used, the documentation
+  explains how to customize this behavior.
+
+  - Parametric Relation and Morphism are declared differently, using the
+  new [Add Parametric] commands, documented in the manual.
+
+  - Setoid_Theory is now an alias to Equivalence, scripts building objects
+  of type Setoid_Theory need to unfold (or "red") the definitions
+  of Reflexive, Symmetric and Transitive in order to get the same goals 
+  as before. Scripts which introduced variables explicitely will not break.
+
+  - The order of subgoals when doing [setoid_rewrite] with side-conditions
+  is always the same: first the new goal, then the conditions.
+
+- New standard library modules Classes.Morphisms declares
+  standard morphisms on refl/sym/trans relations.
+  Classes.Morphisms_Prop declares morphisms on propositional 
+  connectives and Classes.Morphisms_Relations on generalized predicate
+  connectives. Classes.Equivalence declares notations and tactics
+  related to equivalences and Classes.SetoidTactics defines the
+  setoid_replace tactics and some support for the "Add *" interface,
+  notably the tactic applied automatically before each "Add Morphism"
+  proof.
+
+- User-defined subrelations are supported, as well as higher-order morphisms
+  and rewriting under binders. The tactic is also extensible entirely in Ltac.
+  The documentation has been updated to cover these features.
+
+- [setoid_rewrite] and [rewrite] now support the [at] modifier to select 
+  occurrences to rewrite, and both use the [setoid_rewrite] code, even when
+  rewriting with leibniz equality if occurrences are specified.
+
 Tools
 
 - CoqIDE font defaults to monospace so as indentation to be meaningful.
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index c1295349da..5fe218fa50 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -80,7 +80,6 @@ will be first rewrote to:
 If you do specify a {\tt return} or {\tt in} clause the typechecker will
 fall back directly to \Coq's usual typing of dependent pattern-matching.
 
-
 The next two commands are similar to their standard counterparts
 Definition (see Section~\ref{Simpl-definitions}) and Fixpoint (see Section~\ref{Fixpoint}) in that
 they define constants. However, they may require the user to prove some
@@ -201,7 +200,7 @@ Otherwise the proof will be started with the elobarted version as a goal.
 The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
   Hypothesis}, {\tt Axiom} etc...
 
-\subsection{Solving obligations}
+\section{Solving obligations}
 The following commands are available to manipulate obligations. The
 optional identifier is used when multiple functions have unsolved
 obligations (e.g. when defining mutually recursive blocks). The optional
@@ -212,9 +211,6 @@ tactic is replaced by the default one if not specified.
   Sets the default obligation
   solving tactic applied to all obligations automatically, whether to
   solve them or when starting to prove one, e.g. using {\tt Next}.
-\item {\tt Set Transparent Obligations}
-  Force all obligations to be declared as transparent, otherwise let the
-  system infer which obligations can be declared opaque.
 \item {\tt Obligations [of \ident]}\comindex{Obligations} Displays all remaining
   obligations.
 \item {\tt Obligation num [of \ident]}\comindex{Obligation} Start the proof of
@@ -233,6 +229,9 @@ tactic is replaced by the default one if not specified.
 \item {\tt Preterm [of \ident]}\comindex{Preterm} 
   Shows the term that will be fed to
   the kernel once the obligations are solved. Useful for debugging.
+\item {\tt Set Transparent Obligations}\comindex{Set Transparent Obligations}
+  Force all obligations to be declared as transparent, otherwise let the
+  system infer which obligations can be declared opaque.
 \end{itemize}
 
 The module {\tt Coq.Program.Tactics} defines the default tactic for solving
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a54de8b8a7..96b3aff76f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -502,7 +502,7 @@ let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep
 let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful")
 
 let equivalence = lazy (gen_constant ["Classes"; "RelationClasses"] "Equivalence")
-let default_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "DefaultRelation")
+let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultRelation")
 
 let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
 let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
@@ -1144,7 +1144,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
   match (refl,symm,trans) with 
       (None, None, None) -> 
-	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.DefaultRelation"
+	let instance = declare_instance a aeq n "Coq.Classes.SetoidTactics.DefaultRelation"
 	in ignore(anew_instance binders instance [])
     | (Some lemma1, None, None) -> 
 	ignore (declare_instance_refl binders a aeq n lemma1)
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 6270fb43ba..5e34a44379 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -7,11 +7,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Typeclass-based setoids, tactics and standard instances.
+(* Typeclass-based setoids. Definitions on [Equivalence].
  
    Author: Matthieu Sozeau
    Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
-   91405 Orsay, France *)
+   91405 Orsay, France *) 
 
 (* $Id$ *)
 
@@ -28,18 +28,29 @@ Unset Strict Implicit.
 
 Open Local Scope signature_scope.
 
-(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
-
-Instance [ Equivalence A R ] => 
-  equivalence_default : DefaultRelation A R | 4.
-
 Definition equiv [ Equivalence A R ] : relation A := R.
 
 Typeclasses unfold @equiv.
 
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+
+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.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv [ PER A R ] : relation A := R.
 
+Typeclasses unfold @pequiv.
+
+(** Overloaded notation for partial equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
-(* (** Shortcuts to make proof search possible (unification won't unfold equiv). *) *)
+(** Shortcuts to make proof search easier. *)
 
 Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv.
 
@@ -57,34 +68,7 @@ Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv.
     transitivity y ; auto.
   Qed.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
-
-(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
-(* Notation " x == y " := (equiv (x :>) (y :>)) (at level 70, no associativity) : type_scope. *)
-
-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.
-
-Lemma nequiv_equiv_trans : forall [ Equivalence A ] (x y z : A), x =/= y -> y === z -> x =/= z.
-Proof with auto.
-  intros; intro.
-  assert(z === y) by (symmetry ; auto).
-  assert(x === y) by (transitivity z ; auto).
-  contradiction.
-Qed.
-
-Lemma equiv_nequiv_trans : forall [ Equivalence A ] (x y z : A), x === y -> y =/= z -> x =/= z.
-Proof.
-  intros; intro. 
-  assert(y === x) by (symmetry ; auto).
-  assert(y === z) by (transitivity x ; auto).
-  contradiction.
-Qed.
-
-(** Use the [substitute] command which substitutes an applied relation in every hypothesis. *)
+(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
 Ltac setoid_subst H := 
   match type of H with
@@ -101,6 +85,8 @@ Ltac setoid_subst_nofail :=
 
 Tactic Notation "subst" "*" := subst_no_fail ; setoid_subst_nofail.
 
+(** Simplify the goal w.r.t. equivalence. *)
+
 Ltac equiv_simplify_one :=
   match goal with
     | [ H : ?x === ?x |- _ ] => clear H
@@ -111,6 +97,9 @@ Ltac equiv_simplify_one :=
 
 Ltac equiv_simplify := repeat equiv_simplify_one.
 
+(** "reify" relations which are equivalences to applications of the overloaded [equiv] method
+   for easy recognition in tactics. *)
+
 Ltac equivify_tac :=
   match goal with
     | [ s : Equivalence ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
@@ -119,43 +108,6 @@ Ltac equivify_tac :=
 
 Ltac equivify := repeat equivify_tac.
 
-(** Every equivalence relation gives rise to a morphism, as it is Transitive and Symmetric. *)
-
-(* Instance [ sa : Equivalence ] => equiv_morphism : Morphism (equiv ++> equiv ++> iff) equiv := *)
-(*   respect := respect. *)
-
-(* (** The partial application too as it is Reflexive. *) *)
-
-(* Instance [ sa : Equivalence A ] (x : A) =>  *)
-(*   equiv_partial_app_morphism : Morphism (equiv ++> iff) (equiv x) := *)
-(*   respect := respect.  *)
-
-(** Instance not exported by default, as comparing types for equivalence may be unintentional. *)
-
-Section Type_Equivalence.
-
-  Definition type_eq : relation Type :=
-    fun x y => x = y.
-  
-  Program Instance type_equivalence : Equivalence Type type_eq.
-  
-  Next Obligation. 
-  Proof. unfold type_eq in *. subst. reflexivity. Qed.
-
-End Type_Equivalence.
-
-(** Partial equivs don't require reflexivity so we can build a partial equiv on the function space. *)
-
-Class PartialEquivalence (carrier : Type) (pequiv : relation carrier) :=
-  pequiv_prf :> PER carrier pequiv.
-
-Definition pequiv [ PartialEquivalence A R ] : relation A := R.
-Typeclasses unfold @pequiv.
-
-(** Overloaded notation for partial equiv equivalence. *)
-
-Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scope.
-
 Section Respecting.
 
   (** Here we build an equivalence instance for functions which relates respectful ones only, 
@@ -180,12 +132,13 @@ Section Respecting.
 
 End Respecting.
 
-(** The default equivalence on function spaces. *)
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
 
 Program Instance [ Equivalence A eqA ] => 
-  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA).
+  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9.
 
   Next Obligation.
   Proof.
     transitivity (y x0) ; auto.
   Qed.
+
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index ebbd887c2a..6a002d97a8 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -21,14 +21,6 @@ Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 Require Export Coq.Relations.Relation_Definitions.
 
-(** Default relation on a given support. *)
-
-Class DefaultRelation A (R : relation A).
-
-Definition default_relation [ DefaultRelation A R ] := R.
-
-(** To search for the default relation, just call [default_relation]. *)
-
 Notation inverse R := (flip (R:relation _) : relation _).
 
 Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 03195e083d..8752f649bc 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -24,7 +24,24 @@ Require Export Coq.Relations.Relation_Definitions.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** The setoid_replace tactics in Ltac, defined in terms of default relations [===def] and
+(** Default relation on a given support. Can be used by tactics
+   to find a sensible default relation on any carrier. Users can 
+   declare an [Instance A RA] anywhere to declare default relations.
+   This is also done by the [Declare Relation A RA] command with no
+   parameters for backward compatibility. *)
+
+Class DefaultRelation A (R : relation A).
+
+(** To search for the default relation, just call [default_relation]. *)
+
+Definition default_relation [ DefaultRelation A R ] := R.
+
+(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *)
+
+Instance [ Equivalence A R ] => 
+  equivalence_default : DefaultRelation A R | 4.
+
+(** The setoid_replace tactics in Ltac, defined in terms of default relations and
    the setoid_rewrite tactic. *)
 
 Ltac setoidreplace H t :=