 # How to utilize extensionality when rewriting

This is an issue that I’ve come up to time and time again, and I was wondering if there was any solution. In general, I have a term that looks like `∀x, <expression>`, and I want to rewrite in a part of the expression. I understand that this is not generally doable in Coq, but I use propositional and functional extensionality, and using those I can prove myself that `(∀x, <expression>) = (∀x, <rewritten expression)`, and can then rewrite using that. However, sometimes the expressions get really complicated and the proofs get really cluttered and hard to read when I have to write out the entire expressions myself. Is there any kind of system I can set up to make it as simple as rewriting?

There are a few techniques, but I couldn’t advise one over the other since I master none of them. Here are some references to the relevant documentations:

• Setoid rewriting allows to rewrite up to an equivalence relation provided that all type formers respect that relation (which must be proven beforehand)
• The under tactic allows to locally open a binder using an extensionality lemma (this is particularly useful if you don’t want to assume functional extensionality globally, but that does not seem to be a problem for you)
• There is an `extensionality x` tactic in the stdlib that does a similar job as under using the functional extensionality axiom.
• In specfic cases you can also use Ltac’s `match goal with` together with second order patterns `@?ident` to instantiate funext with a subexpression of your goal.

Hope it helps.

Setoid rewriting can indeed help, and maybe even with a few generic instances.

Maybe the following lemmas would help abstracting the use of propositional/functional extensionality.

``````From Coq Require Import FunctionalExtensionality PropExtensionality.

Lemma forall_ext {T : Type} {A B : T -> Type} :
(forall x: T, A x = B x) ->
(forall x: T, A x) = forall x: T, B x.
Proof.
intros HpwEq.
assert (A = B) as Heq. { extensionality x. apply HpwEq. }
now rewrite Heq.
Qed.

Lemma forall_ext_prop {T : Type} {A B : T -> Prop} :
(forall x: T, A x <-> B x) ->
(forall x: T, A x) = forall x: T, B x.
Proof.
intros Hequiv.
assert (A = B) as Heq. {
extensionality x. apply propositional_extensionality, Hequiv.
}
now rewrite Heq.
Qed.
``````

What’s still annoying is that you must still use `rewrite (forall_ext_prop (your equivalence lemma))`, and the equivalence lemma must be for the whole expression.
But it seems setoid rewriting can help! You need the following instances (and apparently can skip `forall_ext_prop`, since its effects arise from the composition)

``````From Coq Require Import Setoid Morphisms.

Instance proper_all T : Proper (pointwise_relation T eq ==> eq) (all (A := T)).
Proof.
intros x y Heq.
apply forall_ext, Heq.
Qed.
Instance propext_subrel : subrelation iff eq.
Proof. intros A B Hequiv. apply propositional_extensionality, Hequiv. Qed.
``````

Here are a couple of tests:

``````(* Could be an Instance, but it's not needed. *)
Lemma test_proper_all_iff T : Proper (pointwise_relation T iff ==> eq) (all (A := T)).
Proof. now intros ?? ->. Qed. (* This uses the rewrite tactic, which already uses setoid rewriting. *)

Lemma forall_ext_prop_test {T : Type} {A B : T -> Prop} :
(forall x: T, A x <-> B x) ->
(forall x: T, A x) = forall x: T, B x.
Proof. intros Heq. setoid_rewrite Heq. easy. Qed. (* Here we need [setoid_rewrite] because we're actually going under binders *)

Lemma forall_ext_prop_test2 {T U : Type} {A B : T -> U} (C : U -> Prop) :
(forall x: T, A x = B x) ->
(forall x: T, C (A x)) = forall x: T, C (B x).
Proof. intros H. setoid_rewrite H. easy. Qed.

Lemma forall_ext_prop_test3 {T U : Type} {A B : T -> Prop}
(C : Prop -> Prop) `{!Proper (iff ==> iff) C}:
(forall x: T, A x <-> B x) ->
(forall x: T, C (A x)) = forall x: T, C (B x).
Proof. intros H. setoid_rewrite H. easy. Qed.

Lemma forall_ext_prop_test4 {T U : Type} {A B : T -> Prop}
(C : Prop -> Prop) :
(forall x: T, A x <-> B x) ->
(forall x: T, C (A x)) = forall x: T, C (B x).
Proof.
intros Heqv.
assert (forall x: T, A x = B x) as Heq. now setoid_rewrite Heqv.
setoid_rewrite Heq. easy.
Qed.
``````

To know which instances to write, I wrote `forall_ext_prop_test` and looked at the error from `setoid_rewrite H. `forall_ext_prop_test3`and`forall_ext_prop_test4`is possibly unrealistic stress-tests (and`forall_ext_prop_test3` might work out of the box).

BTW, maybe something like those instances would belong in the stdlib, but I haven’t tested them enough for it.

Thank you both of you. `under` worked alright, and the setoid rewriting that Blaisorblade showed worked after defining one more instance.