rewrite within lambda with respect to an equivalence relation

Question

The question is, if I know that forall x, f x ≡ g x (where ≡ is some equivalence relation, and f, g, are functions), what is the correct Proper instance which will let me rewrite f with g in some larger term linked by the equivalence relation?

Assume functional extensionality is available if required - which I guess will be required for this?

Some sample code to demonstrate the question better:

Require Import Setoid.
(** Feel free to assume FunExt *)
Require Import FunctionalExtensionality.
Section FOOBAR.
  Variable T: Type.
  Variable f: T -> T.
  Variable g: T -> T.

  Variable t0: T.
  Variable combiner: (T -> T) -> T -> T.

  Variable equiv: T -> T -> Prop.
  Infix "≡" := equiv (at level 50).

  Axiom equivalence_equiv: Equivalence equiv.


  Axiom F_EQUIV_G_EXT: forall (t: T), f t ≡ g t.

  (** Check that coq can resolve the Equivalence instance **)
  Theorem equivalence_works: t0 ≡ t0.
  Proof.
    reflexivity.
  Qed.

  Theorem rewrite_in_lambda:
    combiner (fun t => f t) t0 ≡
    combiner (fun t => g t) t0.
  Proof.
    intros.
    (* I wish to replace x with y.
    What are the Proper rules  I need for this to happen? *)
    rewrite F_EQUIV_G_EXT.
  Abort.
End FOOBAR.

The proof goes through if we can replace f with g, but I'm not sure how to do that. What additional power do I need for my equivalence relation for this to succeed?

Answer 1

The solution is to use pointwise_relation from the coq stdlib: Link here

I also copy-pasted the definition in case the link bitrots:

 Definition pointwise_relation (R : relation B) : relation (A -> B) :=
    fun f g => forall a, R (f a) (g a).

So, we wish for a proper instance of the form:

Axiom proper: Proper (pointwise_relation T equiv ==> equiv ==> equiv) combiner.

That is, if the first function is pointwise equal, and the second argument is equal, then the result is equal.

Here is the full code listing which compiles:

Require Import Setoid.
Require Import Relation_Definitions.
Require Import Morphisms.

(** Feel free to assume FunExt *)
Require Import FunctionalExtensionality.
Section FOOBAR.
  Variable T: Type.
  Variable x: T -> T.
  Variable y: T -> T.

  Variable t0: T.
  Variable combiner: (T -> T) -> T -> T.

  Variable equiv: T -> T -> Prop.
  Infix "≡" := equiv (at level 50).

  Axiom equivalence_equiv: Equivalence equiv.
  Axiom proper: Proper (pointwise_relation T equiv ==> equiv ==> equiv) combiner.

  Axiom X_EQUIV_Y_EXT: forall (t: T), x t ≡ y t.

  (** Check that coq can resolve the Equivalence instance **)
  Theorem equivalence_works: t0 ≡ t0.
  Proof.
    reflexivity.
  Qed.

  Theorem rewrite_in_lambda:
    combiner (fun t => x t) t0 ≡
    combiner (fun t => y t) t0.
  Proof.
    intros.
    (* I wish to replace x with y.
    What are the Proper rules  I need for this to happen? *)
    setoid_rewrite X_EQUIV_Y_EXT.
    reflexivity.
  Qed.
End FOOBAR.