Is there a tactic similar to “erewrite” in Coq?

Stream: lean4

[David Deng]

For theorems and lemmas with uninstantiated variables that are universally quantified, rw will give an error

tactic 'rewrite' failed, pattern is a metavariable

whereas in Coq it would go through with erewrite.

For example , when I have a lemma that has the following type:

lemma mult_subst_bool : (e = exp.tt ∨ e = exp.ff) → mult_subst γ → γ e = e :=

where γ is a substitution that is invariant on boolean types, and if I do rw [mult_subst_bool] with a goal in the form of ... γ exp.tt ..., lean will give an error:

tactic 'rewrite' failed, pattern is a metavariable

It is possible to always instantiate the lemma fully and then do the rewrite, such as

 rw [@mult_subst_abs γ e]

but allowing some temporary binding and later resolving them would be quite helpful. I am wondering if lean has anything similar to Coq's erewrite that would allow leaving holes in the goal or hypothesis.

[Daniel Weber]

Do you have a #mwe ?

[Aaron Liu]

The code for the rw tactic uses key-matching. This means, when you are searching for the pattern f a₁ a₂ ... in the goal g b₁ b₂ ..., only test f a₁ a₂ ... =?= g b₁ b₂ ... if f is syntactically equal to g. Otherwise, repeat for each child of g b₁ b₂ .... This is probably done for performance reasons.

When you get the error

tactic 'rewrite' failed, pattern is a metavariable

that means the expression you are searching to replace is a metavariable ?a (for example, from the equation ?a = ?a + 0). This cannot be used in key-matching, since there is no information to go off of except for the type. The solution is to write in your arguments explicitly, but any proof obligations can (usually) still be delayed.

If you are interested in reading more, the implementation of the rewrite tactic is at docs#Lean.MVarId.rewrite, and replacing lhs by rhs is done at docs#Lean.Meta.kabstract.

[Daniel Weber]

Can you maybe imitate what's done for docs#map_add, using something like docs#DFunLike.coe as head?

[David Deng]

Aaron Liu said:

The code for the rw tactic uses key-matching. This means, when you are searching for the pattern f a₁ a₂ ... in the goal g b₁ b₂ ..., only test f a₁ a₂ ... =?= g b₁ b₂ ... if f is syntactically equal to g. Otherwise, repeat for each child of g b₁ b₂ .... This is probably done for performance reasons.

Thanks for the explanation and the pointer! It kind of makes sense that for performance reason, Lean wouldn't "attempt" to instantiate any metavariables. And that might be a difference between Coq and Lean. But where should I go if I want to learn more about key-matching? Is this rewriting process documented somewhere that might be easier to understand than its source code?

[Aaron Liu]

I learned this just by reading and modifying the source code, and I don't know anywhere else to learn more. Sorry I couldn't be of any help.

[David Deng]

Daniel Weber said:

Do you have a #mwe ?

For example, it would seem intuitive to have lean match ¬b with ¬ true in my goal, since it is the only possible occurrence, but it seems that rw is not able to do that. I am just wondering if there is a more "aggressive" rewrite tactic, or how to accomplish something similar.

#check ne_false_of_eq_true
-- ne_false_of_eq_true {b : Bool} : b = true → ¬b = false
example : (¬ true) = false := by
rw [ne_false_of_eq_true]
-- tactic 'rewrite' failed, equality or iff proof expected

[Kyle Miller]

The issue is that ne_false_of_eq_true is ¬(b = false), not an equality. The result of a rw lemma needs to be an equality or an iff

[Kyle Miller]

Regarding mult_subst_bool, there's a deeper reason it doesn't apply, and that's that the rewrite (with metavariables) is `?γ ?e ==> ?e, and matching ?γ ?e requires higher-order unification. It would be asking rw to take the approximate solution ?γ := γ rather than more exotic solutions such as ?γ := (fun x : Nat => γ) 22.

It's possible to configure things so that it would choose the approximate solution, but it's worth pointing out.

This does mean that you shouldn't need to supply e as well. I'd expect rw [@mult_subst_abs γ] to suffice (or rw [mult_subst_abs (γ := γ)])

[David Deng]

Kyle Miller said:

This does mean that you shouldn't need to supply e as well. I'd expect rw [@mult_subst_abs γ] to suffice (or rw [mult_subst_abs (γ := γ)])

Thanks for your insightful response.

1. I misread the notation in ne_false_of_eq_true, and that is not a good example -- let me try to figure out a better example.
2. You are also indeed correct that the e is not necessary.

It's possible to configure things so that it would choose the approximate solution, but it's worth pointing out.

It sounds like a quite useful feature that Coq allows to some extent by adding lemmas to its hint database. I am wondering what is particularly challenging about higher-order unification? And is it possible to do that in Lean?

[Kyle Miller]

The problem with higher-order unification is the non-uniqueness of solutions — unification tries to find the solution, not a solution (unless certain approximation modes are enabled; apply notably enables the approximation). If you've been exposed to @[elab_as_elim] yet, that's another example of Lean using an approximation for higher-order unification (it's an attribute that causes the application elaborator to process the expected type in a certain way to solve for the "motive" argument).

I don't know the research on higher-order unification. I've been told of systems that enumerate all possible solutions and take the first that works. This is hard to predict — Lean 4 takes a conservative approach, usually opting to fail instead of doing things that are not human predictable.