16
$\begingroup$

Sometimes, trying to use rw in Lean, we get an error saying

motive is not type correct

What does this mean? Often simp_rw succeeds, so what we want to rewrite can be rewritten and the end: why rw is not enough?

$\endgroup$
2
  • $\begingroup$ Have you tried searching in the Zulip chat? It already contains a lot of helpful info. But it's worth discussing whether we should also have some of the answers here though. $\endgroup$
    – Trebor
    Mar 16, 2022 at 11:50
  • 6
    $\begingroup$ Yes, there are several explanation on Zulip. I feel it is worth to also have one here. $\endgroup$
    – Ricky
    Mar 16, 2022 at 11:57

1 Answer 1

15
$\begingroup$

This tends to show up when trying to rewrite a term that appears as a dependent argument.


To understand this, let’s see how rw actually works, by way of a small example:

I’m using list.last with type

list.last {α : Type u} (l : list α) : l ≠ list.nil → α

as an example for a function with a dependent argument: The second argument is a proof that mentions the first argument l.

Let’s try to prove the following lemma:

open list

example (α : Type*) (l : list α) (h1 : l ≠ nil) (x : α) (hx : l = [x]) :
  last l h1 = x :=
begin

We might want to start to rewrite with that equality, but

  rw hx,

fails with

rewrite tactic failed, motive is not type correct
  λ (_a : list α), l.last h1 = x = (_a.last h1 = x)

And the error message sheds more light into why it fails: The rw tactic takes the goal, which is

l.last h1 = x

finds the occurrences of the left-hand side of the equality, i.e. l, and then tries to equate the goal as we have it with the goal where l is replaced by a parameter _a. Adding one set of parenthesis clarifies things maybe a bit:

  λ (_a : list α), (l.last h1 = x) = (_a.last h1 = x)

Normally rw can use this function to turn the equality given to it (hx) into an equality between the existing goal and the goal you’d expect after the rw, but it doesn’t even get that far: The expression above is not type-correct! In _a.last h1, the h1 is still l ≠ nil, but it now should be _a ≠ nil.


Unfortunately, rw is too limited to take care of this automatically. Work-arounds are, as you say

  • use simp_rw, which is able to generalize goals even in these cases.

    But has it’s own shortcomings – you cannot rewrite with equalities like l = head l @ tail l that mention the LHS on the RHS. This is because simp_rw is based on simp, and as a simplification rule, this would be bad.

  • use simp only [hx] {single_pass := tt}, which is similar to simp_rw, but doesn’t complain about such looping rewrites.

  • If the equality has just a variable on one of its side (as it does here), then

    subst hx
    

    works nicely.

  • If the dependent argument that gets in the way is a local hypothesis (such as the hx here), it can help to move it into the goal;

    revert h1, rw hx, intro h1,
    

    works here, and may work in your case. But it may not always be possible to revert all relevant hypotheses.

  • If none of these help, you can try to extract a helper lemma where the thing you want to replace is a variable, use subst to prove that lemma quite directly, and then use that lemma.

$\endgroup$
5
  • $\begingroup$ revert h1, rw hx also works in this case :) $\endgroup$
    – Junyan Xu
    Mar 16, 2022 at 21:07
  • $\begingroup$ Is that a universally applicable workaround, or something that works sometimes? $\endgroup$ Mar 16, 2022 at 21:26
  • $\begingroup$ Does simp only [hx] {single_pass := tt} avoid the shortcomings of simp_rw hx? $\endgroup$
    – Eric
    Mar 16, 2022 at 23:38
  • $\begingroup$ Ah, right, you suggested that. I’ll add it. What I find surprising: Why does simp only not complain about hx not being a suitable simplification lemma? $\endgroup$ Mar 17, 2022 at 16:06
  • 1
    $\begingroup$ I couldn't find a good example of this, but I have also judiciously used for this; instead of the rws as I usually would, I'd do replace old_id : (exact_term_I_want) := h ▸old_id; really tedious but it works well. For the goal, I guess you can use change_to in a similar way. $\endgroup$ Mar 18, 2022 at 13:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.