Cannot rewrite using hypotheses with universal quantifiers

[oskgo]

The following example fails with nothing to rewrite, when the hypothesis is clearly matching the if conditional:

op P (x y: bool): bool.

lemma foo x: (forall y, P x y) => x = 
  if (forall y, P x y) then x else witness.
proof.
move => H. 
rewrite H.

There are multiple workarounds. In this simple example you can just use smt, but that requires the goal to be immediately solvable. One can also get around it by using pose to abstract away the conditional.

The simplest workaround I found that should usually work is using rewrite -eqT in H to get (forall y, P x y) = true instead.

[fdupress]

I think this is a more general issue when rewriting any Boolean expression that is not an equality. It's just that it does exactly what the user intends in most cases.

But if we can narrow down which behaviour of matching is getting in the way, perhaps we can make it user-controllable?

[strub]

Here, the system tries to rewrite P x _. A solution would be to support rewrite @H.