When using generalized rewriting, can I get rewrite H with H : f ≡ g to rewrite f x ≡ t to g x ≡ t?
If that’s not possible (as it seems), are there plans to make it possible?
I already know this doesn’t work in coq-stdpp and Iris, so one uses other tactics (here, usually, repeat f_equiv; apply H), tho they have their limitations; but I don’t even know how to google for this problem, let alone find any discussion or plans to address this.
To rewrite f x ≡ f y given x ≡ y I must declare that f is a Proper morphism for ≡, but here it seems I’d need a way to declare that the builtin “function application operator” is Proper for ≡ — which makes little sense.
It seems you’d need a way to declare that ≡ itself is a congruence for application, by proving that ∀ f g : A → B, f ≡ g → ∀ x, f x ≡ g x. Which can be ensured, for instance, by using a setoid on functions that validates extensionality:
Instance fun_equiv `{Equiv B} : Equiv (A → B) := λ f g, ∀ x, f x ≡ g x.
One way to get around this is to make a symbol for function application, e.g. $ like in Haskell, and declare that to be Proper. It isn’t ideal in general, but it should work out. I don’t know of anyone looking into supporting this, but it is the second time I’ve heard about this recently.
I wondered, but I discarded it (maybe too early) (a) as you imply by “not ideal”, then you need to use it everywhere. Or maybe only when needed in proofs, say for applications f $ a where f is not a top-level definition. And then, you’d need to control the expansion of $ carefully. Maybe
Definition apply {A B} (f: A -> B) a := f a.
Argument apply: simpl never.
Infix "$" := apply.
would make simpl and cbn leave it alone, yet keep f $ a and f a at least convertible, so that change (f $ a) with (f a) and viceversa work?
Re “supporting”, IIUC $ should work already, so now you’re talking of proper support? Iris people did agree they’re sad about this, so maybe that’s the 3rd request.
Yes, I think the use of apply with the notations and reduction settings that you propose is correct. In practice. My worry is that in practice, change will repeat the type of the term, so I’m not sure if this would actually be faster or slower than the “manual” application (which is what setoid_rewrite is doing).
This is mainly a compat issue AFAIR. setoid_rewrite will look for matches at the head of applications if I’m not mistaken. I think there’s even a flag in the ML code to control that, it would apparently be a good candidate for an option to make rewrite consider those candidates as well and satisfy 3 users
Uh? But how would it know that equiv f g implies forall a, equiv (f a) (g a)? What’s the typeclass instance to use? Or does setoid_rewrite have a special case for when they’re definitionally equal?
I was assuming that f is Proper for (pointwise_relation equiv) indeed, and f equiv g meant pointwise equality too. Usually that’s the case but might require some additional reasoning (e.g. if your equality on functions is only a PER).
@mattam82 I’m sure I’m missing something, but at least in Coq 8.8.2 setoid_rewrite doesn’t seem to help, even when all your assumptions are satisfied, as for coq-iris. And IIUC @robbert didn’t know how to fix this. Also, I’m not sure how the Proper instance should help — because f equiv g need not be lifted through any instance, but applied directly.
A small Iris-based example comes below. Functions in A -n> B are equiv-respecting. Crucially, rewrite Heq fails even when apply Heq succeeds, tho the workarounds usually are harder.
From iris.algebra Require Import ofe.
Section foo.
Context {A B C: ofeT} (f g : A -n> B) (h : B -n> C).
Instance: Proper (pointwise_relation _ (≡)) f := _.
Instance: Proper (pointwise_relation _ (≡)) g := _.
Instance: Proper (pointwise_relation _ (≡)) h := _.
Lemma foo x : f ≡ g → f x ≡ g x.
Proof.
intros Heq.
Fail rewrite Heq.
Fail setoid_rewrite Heq.
apply Heq. (* this work-around doesn't work in bigger contexts. *)
Qed.
(* Ditto here: *)
Lemma foo' : f ≡ g → ∀ x, f x ≡ g x.
Proof.
intros Heq.
Fail rewrite Heq.
Fail setoid_rewrite Heq.
apply Heq.
Qed.
Lemma bar x : f ≡ g → h (f x) ≡ h (g x).
Proof.
intros Heq.
Fail rewrite Heq.
Fail setoid_rewrite Heq.
Fail apply Heq. (* Of course *)
(* workaround: call stdpp's f_equiv by hand. *)
f_equiv. apply Heq.
Qed.
End foo.
