1 files changed, 66 insertions, 256 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index f61b4a415..78e53aa01 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -22,72 +22,48 @@ Require Import Coq.Classes.Init.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-(** We first define setoids on a carrier, it amounts to an equivalence relation. 
-   Now [equiv] is overloaded for every [Setoid].
-*)
+Require Export Coq.Classes.Relations.
 
-Require Export Coq.Relations.Relations.
+(** A setoid wraps an equivalence. *)
 
-Class Setoid (carrier : Type) (equiv : relation carrier) :=
-  equiv_prf : equivalence carrier equiv.
+Class Setoid A :=
+  equiv : relation A ;
+  setoid_equiv :> Equivalence A equiv.
 
-(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
+(** Shortcuts to make proof search easier. *)
 
-Definition equiv [ Setoid A R ] : _ := R.
+Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(** Subset objects should be first coerced to their underlying type, but that notation doesn't work in the standard case then. *)
+Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-(* 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.
+Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
+Proof. eauto with typeclass_instances. Qed.
 
-Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
+(** Standard setoids. *)
 
-Definition equiv_refl [ s : Setoid A R ] : forall x : A, R x x := equiv_refl _ _ equiv_prf.
-Definition equiv_sym [ s : Setoid A R ] : forall x y : A, R x y -> R y x := equiv_sym _ _ equiv_prf.
-Definition equiv_trans [ s : Setoid A R ] : forall x y z : A, R x y -> R y z -> R x z := equiv_trans _ _ equiv_prf.
+Program Instance eq_setoid : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
 
-Lemma nequiv_sym : forall [ s : Setoid A R ] (x y : A), x =/= y -> y =/= x.
-Proof.
-  intros ; red ; intros.
-  apply equiv_sym in H0...
-  apply (H H0).
-Qed.
-
-(** Tactics to do some progress on the goal, called by the user. *)
-
-Ltac do_setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ |- ?R ?X _ ] => apply (equiv_refl (R:=R) X)
-    | [ |- ?R ?A ?X _ ] => apply (equiv_refl (R:=R A) X)
-    | [ |- ?R ?A ?B ?X _ ] => apply (equiv_refl (R:=R A B) X)
-    | [ |- ?R ?A ?B ?C ?X _ ] => apply (equiv_refl (R:=R A B C) X)
-  end.
+Program Instance iff_setoid : Setoid Prop :=
+  equiv := iff ; setoid_equiv := iff_equivalence.
 
-Ltac refl := do_setoid_refl.
+(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
-Ltac do_setoid_sym := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Y ] => apply (equiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- not (@equiv ?A ?R ?s ?X ?Y) ] => apply (nequiv_sym (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y))
-    | [ |- ?R ?X ?Y ] => apply (equiv_sym (R:=R) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?X ?Y ] => apply (equiv_sym (R:=R A) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?X ?Y ] => apply (equiv_sym (R:=R A B) (x:=Y) (y:=X))
-    | [ |- ?R ?A ?B ?C ?X ?Y ] => apply (equiv_sym (R:=R A B C) (x:=Y) (y:=X))
-  end.
+(** 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. *)
 
-Ltac sym := do_setoid_sym.
+Notation " x == y " := (equiv x y) (at level 70, no associativity) : type_scope.
 
-Ltac do_setoid_trans Y := 
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?X ?Z ] => apply (equiv_trans (R:=R) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?X ?Z ] => apply (equiv_trans (R:=R A) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?X ?Z ] => apply (equiv_trans (R:=R A B) (x:=X) (y:=Y) (z:=Z))
-    | [ |- ?R ?A ?B ?C ?X ?Z ] => apply (equiv_trans (R:=R A B C) (x:=X) (y:=Y) (z:=Z))
-  end.
+Notation " x =/= y " := (~ x == y) (at level 70, no associativity) : type_scope.
 
-Ltac trans y := do_setoid_trans y.
+Lemma nequiv_sym : forall [ s : Setoid A ] (x y : A), x =/= y -> y =/= x.
+Proof with auto.
+  intros ; red ; intros.
+  apply H.
+  sym...
+Qed.
 
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
@@ -106,66 +82,24 @@ Ltac clsubst_nofail :=
 
 Tactic Notation "clsubst" "*" := clsubst_nofail.
 
-(** Tactics to immediately solve the goal without user help. *)
-
-Ltac setoid_refl :=
-  match goal with
-    | [ |- @equiv ?A ?R ?s ?X _ ] => apply (equiv_refl (A:=A) (R:=R) (s:=s) X)
-    | [ H : ?X =/= ?X |- _ ] => elim H ; setoid_refl
-  end.
-
-Ltac setoid_sym := 
-  match goal with
-    | [ H : ?X == ?Y |- ?Y == ?X ] => apply (equiv_sym (x:=X) (y:=Y) H)
-    | [ H : ?X =/= ?Y |- ?Y =/= ?X ] => apply (nequiv_sym (x:=X) (y:=Y) H)
-  end.
-
-Ltac setoid_trans := 
-  match goal with
-    | [ H : ?X == ?Y, H' : ?Y == ?Z |- @equiv ?A ?R ?s ?X ?Z ] => apply (equiv_trans (A:=A) (R:=R) (s:=s) (x:=X) (y:=Y) (z:=Z) H H')
-  end.
-
-(** To immediatly solve a goal on setoid equality. *)
-
-Ltac setoid_tac := setoid_refl || setoid_sym || setoid_trans.
-
 Lemma nequiv_equiv : forall [ Setoid A ] (x y z : A), x =/= y -> y == z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(z == y) by setoid_sym.
-  assert(x == y) by setoid_trans.
+  assert(z == y) by relation_sym.
+  assert(x == y) by relation_trans.
   contradiction.
 Qed.
 
 Lemma equiv_nequiv : forall [ Setoid A ] (x y z : A), x == y -> y =/= z -> x =/= z.
 Proof.
   intros; intro. 
-  assert(y == x) by setoid_sym.
-  assert(y == z) by setoid_trans.
+  assert(y == x) by relation_sym.
+  assert(y == z) by relation_trans.
   contradiction.
 Qed.
 
 Open Scope type_scope.
 
-(** Need to fix fresh to not fail if some arguments are not identifiers. *)
-(* Ltac setoid_sat ::= *)
-(*   match goal with *)
-(*     | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" y x in add_hypothesis name (equiv_sym H) *)
-(*     | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" y x in add_hypothesis name (nequiv_sym H) *)
-(*     | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" x z in add_hypothesis name (equiv_trans H H') *)
-(*     | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (equiv_nequiv H H') *)
-(*     | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" x z in add_hypothesis name (nequiv_equiv H H') *)
-(*   end. *)
-
-Ltac setoid_sat :=
-  match goal with
-    | [ H : ?x == ?y |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_sym H)
-    | [ H : ?x =/= ?y |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_sym H)
-    | [ H : ?x == ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Heq" in add_hypothesis name (equiv_trans H H')
-    | [ H : ?x == ?y, H' : ?y =/= ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (equiv_nequiv H H')
-    | [ H : ?x =/= ?y, H' : ?y == ?z |- _ ] => let name:=fresh "Hneq" in add_hypothesis name (nequiv_equiv H H')
-  end.
-
 Ltac setoid_simplify_one :=
   match goal with
     | [ H : ?x == ?x |- _ ] => clear H
@@ -175,192 +109,68 @@ Ltac setoid_simplify_one :=
 
 Ltac setoid_simplify := repeat setoid_simplify_one.
 
-Ltac setoid_saturate := repeat setoid_sat.
-
 Ltac setoidify_tac :=
   match goal with
-    | [ s : Setoid ?A ?R, H : ?R ?x ?y |- _ ] => change R with (@equiv A R s) in H
-    | [ s : Setoid ?A ?R |- context C [ ?R ?x ?y ] ] => change (R x y) with (@equiv A R s x y)
+    | [ 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.
 
-Definition respectful [ sa : Setoid a eqa, sb : Setoid b eqb ] 
-  (m : a -> b) : Prop :=
-  forall x y, eqa x y -> eqb (m x) (m y).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => 
-  Morphism (m : a -> b) :=
-  respect : respectful m.
-
-(** Here we build a setoid instance for functions which relates respectful ones only. *)
-
-Definition respecting [ Setoid a R, Setoid b R' ] : Type := 
-  { morph : a -> b | respectful morph }.
-
-Ltac obligations_tactic ::= try red ; program_simpl ; try tauto.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => 
-  arrow_setoid : 
-  Setoid ({ morph : a -> b | respectful morph })
-
-  (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-
-  Next Obligation.
-  Proof.
-    trans (y x0) ; eauto.
-    apply H.
-    refl.
-  Qed.
-
-  Next Obligation.
-  Proof.
-    sym ; apply H.
-    sym ; auto.
-  Qed.
-
-(** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
-   some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
-
-Definition binary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, Setoid c eqc ]
-  (m : a -> b -> c) : Prop :=
-  forall x y, eqa x y -> 
-    forall z w, eqb z w -> eqc (m x z) (m y w).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc ] => 
-  BinaryMorphism (m : a -> b -> c) :=
-  respect2 : binary_respectful m.
-
-Definition ternary_respectful [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, Setoid d eqd ]
-  (m : a -> b -> c -> d) : Prop :=
-  forall x y, eqa x y -> forall z w, eqb z w -> forall u v, eqc u v -> eqd (m x z u) (m y w v).
-
-Class [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc, sd : Setoid d eqd ] => 
-  TernaryMorphism (m : a -> b -> c -> d) :=
-  respect3 : ternary_respectful m.
-
-(** Definition of the usual morphisms in [Prop]. *)
-
-Program Instance iff_setoid : Setoid Prop iff :=
-  equiv_prf := @Build_equivalence _ _ iff_refl iff_trans iff_sym.
-
-Program Instance not_morphism : Morphism Prop iff Prop iff not.
-
-Program Instance and_morphism : ? BinaryMorphism iff_setoid iff_setoid iff_setoid and.
-
-(* We make the setoids implicit, they're always [iff] *)
-
-Implicit Arguments Enriching BinaryMorphism [[!sa] [!sb] [!sc]].
-
-Program Instance or_morphism : ? BinaryMorphism or.
-
-Definition impl (A B : Prop) := A -> B.
-
-Program Instance impl_morphism : ? BinaryMorphism impl.
-
-Next Obligation.
-Proof.
-  unfold impl. tauto.
-Qed.
-
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
-Program Instance [ Setoid a R ] => setoid_morphism : ? BinaryMorphism R.
+Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv :=
+  trans_sym_morphism.
 
-Next Obligation.
-Proof with auto.
-  split ; intros.
-  trans x. sym... trans z...
-  trans y... trans w... sym...
-Qed.
-  
-Definition iff_morphism : BinaryMorphism iff := setoid_morphism.
+(** Add this very useful instance in the database. *)
 
-Existing Instance iff_morphism.
+Implicit Arguments setoid_morphism [[!sa]].
+Existing Instance setoid_morphism.
 
-Implicit Arguments eq [[A]].
+Definition type_eq : relation Type :=
+  fun x y => x = y.
 
-Program Instance eq_setoid : Setoid A eq :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+Program Instance type_equivalence : Equivalence Type type_eq.
 
-Program Instance eq_morphism : BinaryMorphism A eq A eq Prop iff eq.
+  Solve Obligations using constructor ; unfold type_eq ; program_simpl.
 
-Program Instance arrow_morphism : BinaryMorphism A eq B eq C eq m.
+Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Implicit Arguments arrow_morphism [[A] [B] [C]].
+Ltac obligations_tactic ::= morphism_tac.
 
-Program Instance type_setoid : Setoid Type (fun x y => x = y) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
+(** 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. *)
 
-Lemma setoid_subst : forall (x y : Type), x == y -> x -> y.
-Proof.
-  intros.
-  rewrite <- H.
-  apply X.
-Qed.
+Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Lemma prop_setoid_subst : forall (x y : Prop), x == y -> x -> y.
-Proof.
-  intros.
-  clrewrite <- H.
-  apply H0.
-Qed.
+Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
 
-Program Instance [ sa : Setoid a eqa, sb : Setoid b eqb, sc : Setoid c eqc,
-  mg : ? Morphism sb sc g, mf : ? Morphism sa sb f ] => 
-  compose_morphism : ? Morphism sa sc (fun x => g (f x)).
+(* 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. *)
+    
 
-Next Obligation.
-Proof.
-  apply (respect (m0:=mg)).
-  apply (respect (m0:=mf)).
-  assumption.
-Qed.
+(* 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) (equiv : relation carrier) :=
-  pequiv_prf : PER carrier equiv.
+Class PartialSetoid (carrier : Type) :=
+  pequiv : relation carrier ;
+  pequiv_prf :> PER carrier pequiv.
 
 (** Overloaded notation for partial setoid equivalence. *)
 
-Definition pequiv [ PartialSetoid A R ] : _ := R.
-
 Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
-Definition pequiv_sym [ s : PartialSetoid A R ] : forall x y : A, R x y -> R y x := per_sym _ _ pequiv_prf.
-Definition pequiv_trans [ s : PartialSetoid A R ] : forall x y z : A, R x y -> R y z -> R x z := per_trans _ _ pequiv_prf.
-
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_partial_setoid : 
-  PartialSetoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  pequiv_prf := Build_PER _ _ _ _.
-
-Next Obligation.
-Proof.
-  sym.
-  apply H.
-  sym ; assumption.
-Qed.
-
-Next Obligation.
-Proof.
-  trans (y x0).
-  apply H ; auto.
-  trans y0 ; auto.
-  sym ; auto.
-  apply H0 ; auto.
-Qed.
-
-(** The following is not definable. *)
-(*
-Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
-  Setoid (a -> b)
-  (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
-  equiv_prf := Build_equivalence _ _ _ _ _.
-*)
-
 (** Reset the default Program tactic. *)
 
 Ltac obligations_tactic ::= program_simpl.