1 files changed, 144 insertions, 0 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
new file mode 100644
index 00000000..70bf3483
--- /dev/null
+++ b/theories/Classes/Equivalence.v
@@ -0,0 +1,144 @@
+(* -*- 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. Definitions on [Equivalence].
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *) 
+
+(* $Id: Equivalence.v 10919 2008-05-11 22:04:26Z msozeau $ *)
+
+Require Export Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
+Require Import Coq.Classes.RelationClasses.
+Require Export Coq.Classes.Morphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Open Local Scope signature_scope.
+
+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 easier. *)
+
+Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv.
+
+Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv.
+
+  Next Obligation.
+  Proof.
+    symmetry ; auto.
+  Qed.
+
+Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv.
+
+  Next Obligation.
+  Proof.
+    transitivity y ; auto.
+  Qed.
+
+(** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
+
+Ltac setoid_subst H := 
+  match type of H with
+    ?x === ?y => substitute H ; clear H x
+  end.
+
+Ltac setoid_subst_nofail :=
+  match goal with
+    | [ H : ?x === ?y |- _ ] => setoid_subst H ; setoid_subst_nofail
+    | _ => idtac
+  end.
+  
+(** [subst*] will try its best at substituting every equality in the goal. *)
+
+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
+    | [ H : ?x === ?y |- _ ] => setoid_subst H
+    | [ |- ?x =/= ?y ] => let name:=fresh "Hneq" in intro name
+    | [ |- ~ ?x === ?y ] => let name:=fresh "Hneq" in intro name
+  end.
+
+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
+    | [ 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.
+
+Section Respecting.
+
+  (** Here we build an equivalence instance for functions which relates respectful ones only, 
+     we do not export it. *)
+
+  Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := 
+    { morph : A -> B | respectful R R' morph morph }.
+  
+  Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] :
+    Equivalence respecting
+    (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+
+  Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    unfold respecting in *. program_simpl. red in H2,H3,H4. 
+    transitivity (y x0) ; auto.
+    transitivity (y y0) ; auto.
+    symmetry. auto.
+  Qed.
+
+End Respecting.
+
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+
+Program Instance pointwise_equivalence [ Equivalence A eqA ] :
+  Equivalence (B -> A) (pointwise_relation eqA) | 9.
+
+  Next Obligation.
+  Proof.
+    transitivity (y x0) ; auto.
+  Qed.
+