1 files changed, 139 insertions, 0 deletions
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
new file mode 100644
index 00000000..65353ed2
--- /dev/null
+++ b/theories/Classes/CEquivalence.v
@@ -0,0 +1,139 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \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 - University Paris Sud
+*)
+
+Require Import Coq.Program.Basics.
+Require Import Coq.Program.Tactics.
+
+Require Import Coq.Classes.Init.
+Require Import Relation_Definitions.
+Require Export Coq.Classes.CRelationClasses.
+Require Import Coq.Classes.CMorphisms.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Generalizable Variables A R eqA B S eqB.
+Local Obligation Tactic := try solve [simpl_crelation].
+
+Local Open Scope signature_scope.
+
+Definition equiv `{Equivalence A R} : crelation A := R.
+
+(** 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.
+
+Local Open Scope equiv_scope.
+
+(** Overloading for [PER]. *)
+
+Definition pequiv `{PER A R} : crelation A := R.
+
+(** 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.
+
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+
+  Next Obligation.
+  Proof. intros A R sa x y z Hxy Hyz.
+         now transitivity y.
+  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 `(eqa : Equivalence A (R : crelation A), 
+                          eqb : Equivalence B (R' : crelation B)) : Type :=
+    { morph : A -> B & respectful R R' morph morph }.
+
+  Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
+    Equivalence (fun (f g : respecting eqa eqb) => 
+                   forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)).
+
+  Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.
+
+  Next Obligation.
+  Proof. 
+    intros. intros f g h H H' x y Rxy.
+    unfold respecting in *. program_simpl. transitivity (g y); auto. firstorder.
+  Qed.
+
+End Respecting.
+
+(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+
+Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
+  Reflexive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_symmetric {A} `(symb : Symmetric B eqB) :
+  Symmetric (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_transitive {A} `(transb : Transitive B eqB) :
+  Transitive (pointwise_relation A eqB) | 9.
+Proof. firstorder. Qed.
+Instance pointwise_equivalence {A} `(eqb : Equivalence B eqB) :
+  Equivalence (pointwise_relation A eqB) | 9.
+Proof. split; apply _. Qed.