1 files changed, 181 insertions, 0 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
new file mode 100644
index 00000000..a9bdaa8f
--- /dev/null
+++ b/theories/Classes/SetoidClass.v
@@ -0,0 +1,181 @@
+(* -*- 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.
+ 
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+   91405 Orsay, France *)
+
+(* $Id: SetoidClass.v 11065 2008-06-06 22:39:43Z msozeau $ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Require Import Coq.Program.Program.
+
+Require Import Coq.Classes.Init.
+Require Export Coq.Classes.RelationClasses.
+Require Export Coq.Classes.Morphisms.
+Require Import Coq.Classes.Functions.
+
+(** A setoid wraps an equivalence. *)
+
+Class Setoid A :=
+  equiv : relation A ;
+  setoid_equiv :> Equivalence A equiv.
+
+Typeclasses unfold equiv.
+
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(*   equivalence_setoid : Setoid A := *)
+(*   equiv := eqA ; setoid_equiv := eqa. *)
+
+(** Shortcuts to make proof search easier. *)
+
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
+
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
+(** Standard setoids. *)
+
+(* Program Instance eq_setoid : Setoid A := *)
+(*   equiv := eq ; setoid_equiv := eq_equivalence. *)
+
+Program Instance iff_setoid : Setoid Prop :=
+  equiv := iff ; setoid_equiv := iff_equivalence.
+
+(** 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 => substitute 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 [ Setoid 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 ; eauto).
+  contradiction.
+Qed.
+
+Lemma equiv_nequiv_trans : forall [ Setoid 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 ; eauto).
+  contradiction.
+Qed.
+
+Ltac setoid_simplify_one :=
+  match goal with
+    | [ H : (?x == ?x)%type |- _ ] => clear H
+    | [ H : (?x == ?y)%type |- _ ] => clsubst H
+    | [ |- (?x =/= ?y)%type ] => let name:=fresh "Hneq" in intro name
+  end.
+
+Ltac setoid_simplify := repeat setoid_simplify_one.
+
+Ltac setoidify_tac :=
+  match goal with
+    | [ s : Setoid ?A, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
+    | [ s : Setoid ?A |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+  end.
+
+Ltac setoidify := repeat setoidify_tac.
+
+(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
+
+Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
+  trans_sym_morphism.
+
+(** Add this very useful instance in the database. *)
+
+Implicit Arguments setoid_morphism [[!sa]].
+Existing Instance setoid_morphism.
+
+Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
+  Reflexive_partial_app_morphism.
+
+Existing Instance setoid_partial_app_morphism.
+
+Definition type_eq : relation Type :=
+  fun x y => x = y.
+
+Program Instance type_equivalence : Equivalence Type type_eq.
+
+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) Basics.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 setoids don't require reflexivity so we can build a partial setoid on the function space. *)
+
+Class PartialSetoid (carrier : Type) :=
+  pequiv : relation carrier ;
+  pequiv_prf :> PER carrier pequiv.
+
+(** Overloaded notation for partial setoid equivalence. *)
+
+Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
+
+(** Reset the default Program tactic. *)
+
+Ltac obligations_tactic ::= program_simpl.