rewrite tactic failed

Stream: general

[Frédéric Le Roux]

In the following example the rewrite tactic fails, and I do not understand why. Note that if we insert an intro x before calling to rw, then it works fine. Is there a deep reason why rw is not able to "see" beyond ∀ x : X here?

variable (X : Type)
lemma definition.complement (A : set X) (x : X) : x ∈ set.compl A ↔ x ∉ A := by finish

example (A B : set X) (H : A = set.compl B) : ∀ x : X, x ∈ A ↔  x ∈ (set.compl B) :=
begin
    rw definition.complement,
end

Lean's response is

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 ∈ set.compl ?m_3

[Patrick Massot]

rw doesn't work under binder. simp and simp_rw do.

[Johan Commelin]

Should simp_rw be renamed to rw!?

[Kenny Lau]

rw! should be simp_rw except that each expression is only applied once

[Johan Commelin]

And what about (the nonexistent) simp_erw? Should that be named rw!#@$@!!?

[Patrick Massot]

Even better: someone should simply fix rw so that is works under binders. But it's probably more complicated than it sounds...

[Johan Commelin]

The downside is probably speed

[Rob Lewis]

Patrick Massot said:

Even better: someone should simply fix rw so that is works under binders. But it's probably more complicated than it sounds...

It's a completely different kind of rewriting. rw builds an eq.rec term to do the substitution. This can't be done under a binder from the "outside," because the thing you want to substitute doesn't exist.

[Rob Lewis]

The alternative is to walk into the term using congruence lemmas, which is what simp and simp_rw do.

[Patrick Massot]

These are all implementation details, we were discussing the user point of view.

[Kevin Buzzard]

Yes, users expect a rewrite tactic not an eq.rec tactic, and we have a stream of people asking the same question

[Johan Commelin]

Otoh, if one method is a lot slower than the other, than it makes sense to provide both. And it's nice if fast tactics have short names

[Johan Commelin]

(Kenny will complain that rw is slow anyway.)

[Kevin Buzzard]

I think he already did that earlier ;-)

[Frédéric Le Roux]

Thanks!