Backtrack changes on eauto, move specialized version of eauto in

class_tactics for further customizations. Add Equivalence.v for
typeclass definitions on equivalences and clrewrite.v test-suite for
clrewrite. Debugging the tactic I found missing morphisms that are now
in Morphisms.v and removed some that made proof search fail or take too
long, not sure it's complete however.


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

2 files changed, 204 insertions, 11 deletions

diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
new file mode 100644
index 0000000000..bd525e0356
--- /dev/null
+++ b/theories/Classes/Equivalence.v
@@ -0,0 +1,157 @@
+(* -*- 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        *)
+(************************************************************************)
+
+(* Typeclass-based setoids, tactics and standard instances.
+   TODO: explain clrewrite, clsubstitute and so on.
+ 
+   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.
+Require Import Coq.Classes.Init.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Export Coq.Classes.Relations.
+Require Export Coq.Classes.Morphisms.
+
+Definition equiv [ Equivalence A R ] : relation A := R.
+
+(** Shortcuts to make proof search possible (unification won't unfold equiv). *)
+
+Definition equivalence_refl [ sa : Equivalence A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition equivalence_sym [ sa : Equivalence A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition equivalence_trans [ sa : Equivalence A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. 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) : type_scope.
+
+Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : type_scope.
+
+(** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
+
+Ltac clsubst H := 
+  match type of H with
+    ?x == ?y => clsubstitute H ; clear H x
+  end.
+
+Ltac clsubst_nofail :=
+  match goal with
+    | [ H : ?x == ?y |- _ ] => clsubst H ; clsubst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+Tactic Notation "clsubst" "*" := clsubst_nofail.
+
+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 relation_sym.
+  assert(x == y) by relation_trans.
+  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 relation_sym.
+  assert(y == z) by relation_trans.
+  contradiction.
+Qed.
+
+Open Scope type_scope.
+
+Ltac equiv_simplify_one :=
+  match goal with
+    | [ H : ?x == ?x |- _ ] => clear H
+    | [ H : ?x == ?y |- _ ] => clsubst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+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)
+  end.
+
+Ltac equivify := repeat equivify_tac.
+
+(** Every equivalence relation gives rise to a morphism, as it is transitive and symmetric. *)
+
+Instance [ sa : Equivalence A ] => 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. 
+
+Definition type_eq : relation Type :=
+  fun x y => x = y.
+
+Program Instance type_equivalence : Equivalence Type type_eq.
+
+  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
+
+Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
+
+Ltac obligations_tactic ::= morphism_tac.
+
+(** These are morphisms used to rewrite at the top level of a proof, 
+   using [iff_impl_id_morphism] if the proof is in [Prop] and
+   [eq_arrow_id_morphism] if it is in Type. *)
+
+Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
+
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
+
+(* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
+
+(* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
+(*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)
+(*   compose_morphism : ? Morphism (compose_respect R R') (g o f). *)
+
+(* Next Obligation. *)
+(* Proof. *)
+(*   apply (respect (m0:=mg)). *)
+(*   apply (respect (m0:=mf)). *)
+(*   assumption. *)
+(* Qed. *)
+
+(** 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.
+
+(** Overloaded notation for partial equiv equivalence. *)
+
+(* Infix "=~=" := pequiv (at level 70, no associativity) : type_scope. *)
+
+(** Reset the default Program tactic. *)
+
+Ltac obligations_tactic ::= program_simpl.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 72db276e4a..3ba6c1824b 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -16,7 +16,6 @@
 (* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)
 
 Require Import Coq.Program.Program.
-Require Import Coq.Classes.Init.
 Require Export Coq.Classes.Relations.
 
 Set Implicit Arguments.
@@ -130,6 +129,10 @@ Program Instance (A : Type) (R : relation A) `B` (R' : relation B)
     destruct respect with x y x0 y0 ; auto.
   Qed.
 
+(** Logical implication [impl] is a morphism for logical equivalence. *)
+
+Program Instance iff_iff_iff_impl_morphism : ? Morphism (iff ++> iff ++> iff) impl.
+
 (** The complement of a relation conserves its morphisms. *)
 
 Program Instance `A` (RA : relation A) [ ? Morphism (RA ++> RA ++> iff) R ] => 
@@ -257,20 +260,20 @@ Program Instance [ Equivalence A R ] (x : A) =>
 
 (** With symmetric relations, variance is no issue ! *)
 
-Program Instance [ Symmetric A R ] B (R' : relation B) 
-  [ Morphism _ (R ++> R') m ] => 
-  sym_contra_morphism : ? Morphism (R --> R') m.
+(* Program Instance (A B : Type) (R : relation A) (R' : relation B) *)
+(*   [ Morphism _ (R ++> R') m ] [ Symmetric A R ] =>  *)
+(*   sym_contra_morphism : ? Morphism (R --> R') m. *)
 
-  Next Obligation.
-  Proof with auto.
-    repeat (red ; intros). apply respect.
-    sym...
-  Qed.
+(*   Next Obligation. *)
+(*   Proof with auto. *)
+(*     repeat (red ; intros). apply respect. *)
+(*     sym... *)
+(*   Qed. *)
 
 (** [R] is reflexive, hence we can build the needed proof. *)
 
-Program Instance [ Reflexive A R ] B (R' : relation B)
-  [ ? Morphism (R ++> R') m ] (x : A) =>
+Program Instance (A B : Type) (R : relation A) (R' : relation B)
+  [ ? Morphism (R ++> R') m ] [ Reflexive A R ] (x : A) =>
   reflexive_partial_app_morphism : ? Morphism R' (m x).
 
   Next Obligation.
@@ -280,6 +283,27 @@ Program Instance [ Reflexive A R ] B (R' : relation B)
     refl.
   Qed.
 
+(** Every transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof
+   to get an [R y z] goal. *)
+
+Program Instance [ Transitive A R ] => 
+  trans_co_eq_inv_impl_morphism : ? Morphism (R ++> eq ++> inverse impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans y...
+    subst x0...
+  Qed.
+
+Program Instance [ Transitive A R ] => 
+  trans_contra_eq_inv_impl_morphism : ? Morphism (R --> eq ++> impl) R.
+
+  Next Obligation.
+  Proof with auto.
+    trans x...
+    subst x0...
+  Qed.
+
 (** Every symmetric and transitive relation gives rise to an equivariant morphism. *)
 
 Program Instance [ Transitive A R, Symmetric A R ] => 
@@ -326,6 +350,12 @@ Program Instance and_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) and.
 
 Program Instance and_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) and.
 
+Program Instance and_inverse_impl_iff_morphism : 
+  ? Morphism (inverse impl ++> iff ++> inverse impl) and.
+
+Program Instance and_iff_inverse_impl_morphism : 
+  ? Morphism (iff ++> inverse impl ++> inverse impl) and.
+
 Program Instance and_iff_morphism : ? Morphism (iff ++> iff ++> iff) and.
 
 (** Logical disjunction. *)
@@ -334,4 +364,10 @@ Program Instance or_impl_iff_morphism : ? Morphism (impl ++> iff ++> impl) or.
 
 Program Instance or_iff_impl_morphism : ? Morphism (iff ++> impl ++> impl) or.
 
+Program Instance or_inverse_impl_iff_morphism :
+  ? Morphism (inverse impl ++> iff ++> inverse impl) or.
+
+Program Instance or_iff_inverse_impl_morphism : 
+  ? Morphism (iff ++> inverse impl ++> inverse impl) or.
+
 Program Instance or_iff_morphism : ? Morphism (iff ++> iff ++> iff) or.