How to utilize extensionality when rewriting

Using Coq
1

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?

2

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.

3

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_test3andforall_ext_prop_test4is possibly unrealistic stress-tests (andforall_ext_prop_test3` might work out of the box).

4

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

5

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