Proposition of fix for fun_Setoid

has the drawback to make rewritting an equivalence between functions
more complex (anon better than pointwise to avoid that?)

Models/ContinuousGraph.v

@@ -320,13 +320,13 @@ Proof.
 + intros ? ? Heq. apply Heq.
 + (* lift_compat *)
   intros [f [iso1 [Hiso1 Ht1]]] [g [iso2 [Hiso2 Ht2]]] Heq [] [] [Heq1 [Heq2 Heq3]].
-  cbn in *. repeat split.
+  cbn in Heq1, Heq2, Heq3. cbn. repeat split.
   - now apply Heq.
-  - rewrite <- (proj1 (iso_morphism iso1 _)), <- Hiso1,
-            <- (proj1 (iso_morphism iso2 _)), <- Hiso2.
+  - rewrite <- (proj1 (iso_morphism iso1 _)), <- (Hiso1 (src (snd x))).
+    rewrite <- (proj1 (iso_morphism iso2 _)), <- (Hiso2 (src (snd x0))).
     now apply Heq.
-  - rewrite <- (proj2 (iso_morphism iso1 _)), <- Hiso1,
-            <- (proj2 (iso_morphism iso2 _)), <- Hiso2.
+  - rewrite <- (proj2 (iso_morphism iso1 _)), <- (Hiso1 (tgt (snd x))),
+            <- (proj2 (iso_morphism iso2 _)), <- (Hiso2 (tgt (snd x0))).
     now apply Heq.
   - now rewrite <- 2 iso_threshold, Ht1, Ht2.
 Defined.

Util/SetoidDefs.v

@@ -19,13 +19,10 @@
 (**************************************************************************)
 
 
-Require Import Rbase.
-Require Import RelationPairs.
-Require Import SetoidDec.
+Require Import Rbase RelationPairs SetoidDec.
 Require Import Pactole.Util.Preliminary.
 Set Implicit Arguments.
 
-
 (* To avoid infinite loops, we use a breadth-first search... *)
 Typeclasses eauto := (bfs) 20.
 (* but we need to remove [eq_setoid] as it matches everything... *)
@@ -52,18 +49,14 @@ Lemma equiv_dec_refl {T U} {S : Setoid T} {E : EqDec S} :
 Proof using . intros. destruct_match; intuition. Qed.
 
 (** **  Setoid Definitions  **)
-
-Instance fun_Setoid A B `(Setoid B) : Setoid (A -> B) | 4.
-Proof. exists (fun f g : A -> B => forall x, f x == g x).
-split.
-+ repeat intro. reflexivity.
-+ intros ? ? Heq ?. symmetry. apply Heq.
-+ repeat intro. etransitivity; eauto.
-Defined.
-
-Instance fun_Setoid_pointwise_compat A B `{Setoid B} :
-  subrelation (@equiv _ (fun_Setoid A _)) (pointwise_relation _ equiv).
-Proof using . intros f g Hfg x. apply Hfg. Qed.
+Instance fun_Setoid (A B : Type) (SB : Setoid B) : Setoid (A -> B)
+  := {| equiv := pointwise_relation A (@equiv B SB);
+        setoid_equiv := Equivalence.pointwise_equivalence (@setoid_equiv B SB) |}.
+
+Instance fun_Setoid_respectful_compat (A B : Type) (SB : Setoid B) :
+  subrelation (@equiv (A->B) (fun_Setoid A SB))
+    (respectful (@eq A) (@equiv B SB)).
+Proof using . intros ?? H ???. subst. apply H. Qed.
 
 Notation "x =?= y" := (equiv_dec x y) (at level 70, no associativity).