How to express that two equivalence relations can setoid rewrite across each other (Coq)

Question

I am looking for a way to express that two equivalence relations are compatible and can (setoid) rewrite across each other. As an example here's an ordinary proof I wrote that a left inverse implies injectivity

Definition injection {A B : Type} (f : A -> B) :=
  forall a1 a2, f a1 = f a2 -> a1 = a2.

Definition left_inverse {A B : Type} (f : A -> B) :=
  exists finv: B -> A, forall a: A, finv (f a) = a.

Lemma injection_left_inverse {A B : Type}: forall (f: A -> B), left_inverse f -> injection f.
Proof.
  unfold left_inverse, injection.
  intros.
  destruct H as [finv H'].
  assert (H'': finv (f a1) = a1) by (apply H').
  rewrite <- H''.
  rewrite H0.
  rewrite H'.
  reflexivity.
Qed.

I'd like to extended to something like this:

Definition injection' {A B : Type} (f : A -> B) (Arel: relation A) (Brel: relation B) :=
  forall a1 a2, Brel (f a1) (f a2) -> Arel a1 a2.

Definition left_inverse' {A B : Type} (f : A -> B) (Arel: relation A) (Brel: relation B) :=
  exists finv: B -> A, forall a: A, Arel (finv (f a)) a.

Lemma injection_left_inverse' {A B : Type}: forall (f: A -> B) (Arel: relation A) (Brel: relation B), 
  left_inverse' f Arel Brel -> injection' f Arel Brel.
Proof.
Admitted.

where Arel and Brel are some equivalence relations that critically are potentially different but compatible in a way that they should be able to rewrite across each other.

This last part is what I don't know how to express. For a single equivalence relation, I know that I can use Add Parametric Relation to allow rewriting, but I don't know how to express that these relations are compatible. I assume it is some use of Proper, but I haven't been able to figure it out exactly.

Answer 1

As additional hypotheses to the theorem, you need Equivalence Arel, which implies Proper (Arel ==> Arel ==> iff) Arel (so Arel can rewrite under itself) and Proper (Arel ==> Brel) f (that f is actually a well-defined function out of "A/Arel" into "B/Brel"). Further, you similarly need to modify the definition left_inverse' to say that the presented left inverse is in fact a well defined function.

(* IMO you should also put Arel and Brel before f in the parameter list *)
Definition left_inverse' {A B : Type} (f : A -> B) (Arel: relation A) (Brel: relation B) :=
  exists finv: B -> A, Proper (Brel ==> Arel) finv /\ forall a: A, Arel (finv (f a)) a.

The proof should now go through.

• That you need to assume (some of) the relations involved are actually equivalences should not be surprising.
• In general, for any object x : T in a setoid-based proof, you also need a proof that it is actually a "well-defined" element of that type, which means you need Proper Trel x, where Trel is some relation that follows the structure of T. In this case, over the course of the proof you have the objects f : A -> B and finv : B -> A, so you need Proper (A ==> B) f, Proper (B ==> A) finv. For elements x : A, you actually get Proper Arel x from reflexivity of Arel.