What does the "motive is not type correct" error mean in Lean?

Question

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?

Answer 1

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.