rewrite tactic failed, motive is not type correct

Stream: new members

[David Renshaw]

I am stuck on the following example:

import data.pnat.basic

example
  (a : ℕ+ → ℤ)
  (n n1 : ℕ+)
  (hpos : 0 < (n1+1).val / 2)
  (hn1 : (n1 + 1).val / 2 = n.val) :
  a ⟨(n1+1).val / 2, hpos⟩ = a n :=
begin
  rw [hn1],
end

Lean reports:

rewrite tactic failed, motive is not type correct
  λ (_a : ℕ), a ⟨(n1 + 1).val / 2, hpos⟩ = a n = (a ⟨_a, hpos⟩ = a n)
state:
a : ℕ+ → ℤ,
n n1 : ℕ+,
hpos : 0 < (n1 + 1).val / 2,
hn1 : (n1 + 1).val / 2 = n.val
⊢ a ⟨(n1 + 1).val / 2, hpos⟩ = a n

How can I get that rewrite to work?

[Ruben Van de Velde]

Try simp_rw instead?

[David Renshaw]

nice!

[David Renshaw]

Why does rw fail?

[Yakov Pechersky]

Because rw is not powerful enough to rewrite under binders. And you have a hypothesis hn1 about (n1 + 1).val. And rw isn't rewriting that hypothesis when you're rewriting the goal.

[Yakov Pechersky]

So then you have a subtyped term where the value isn't matching the hypothesis about it. Which is the motive error.

[David Renshaw]

I don't fully follow what you are saying about binders, but it does make sense to me that a ⟨n.val, hpos⟩ = a n might not typecheck (and therefore my attempt to rewrite might fail).

[David Renshaw]

I don't see how sprinkling in some simp fixes the problem.

[Yakov Pechersky]

simp_rw is able to rewrite under binders. Consider the goal after the simp_rw step:

import data.pnat.basic

example
  (a : ℕ+ → ℤ)
  (n n1 : ℕ+)
  (hpos : 0 < (n1+1).val / 2)
  (hn1 : (n1 + 1).val / 2 = n.val) :
  a ⟨(n1+1).val / 2, hpos⟩ = a n :=
begin
  simp_rw [hn1],
  -- ⊢ a ⟨n.val, _⟩ = a n
end

[Yakov Pechersky]

You can see that the subtype property has changed to _, it is no longer hpos.

[Yakov Pechersky]

We can expose it like so:

import tactic
import data.pnat.basic

example
  (a : ℕ+ → ℤ)
  (n n1 : ℕ+)
  (hpos : 0 < (n1+1).val / 2)
  (hn1 : (n1 + 1).val / 2 = n.val) :
  a ⟨(n1+1).val / 2, hpos⟩ = a n :=
begin
  simp_rw [hn1],
  generalize_proofs hpos',
  /-
  a : ℕ+ → ℤ,
  n n1 : ℕ+,
  hpos : 0 < (n1 + 1).val / 2,
  hn1 : (n1 + 1).val / 2 = n.val,
  hpos' : 0 < n.val
  ⊢ a ⟨n.val, hpos'⟩ = a n
  -/
end

[David Renshaw]

can I invoke proof irrelevance sooner, and then still use rw?

[Yakov Pechersky]

I'm not sure what you mean. hpos and hpos' are only talking about the same term because of hn1.

[David Renshaw]

Does the _ imply that the proof term has been forgotten, or just that it is being suppressed in the pretty-printing?

[Yakov Pechersky]

suppressed

[Yakov Pechersky]

Consider this:

import tactic
import data.pnat.basic

example
  (a : ℕ+ → ℤ)
  (n n1 : ℕ+)
  (hpos : 0 < (n1+1).val / 2)
  (hn1 : (n1 + 1).val / 2 = n.val) :
  a ⟨(n1+1).val / 2, hpos⟩ = a n :=
begin
  rw hn1 at hpos,
  /-
  a : ℕ+ → ℤ,
  n n1 : ℕ+,
  hpos : 0 < (n1 + 1).val / 2,
  hn1 : (n1 + 1).val / 2 = n.val,
  hpos : 0 < n.val
  ⊢ a ⟨(n1 + 1).val / 2, hpos⟩ = a n
  -/

end

[Yakov Pechersky]

rewriting at hpos now gives us two (clashing name) hpos hypotheses. We can't rewrite the first one away because the subtype depends on it because it mentions the value.

[Yakov Pechersky]

And we can't follow up with some coupled rw that changes both the value and the old hpos to the new hpos. But simp_rw can!

[David Renshaw]

The relevant "binder" that we're talking about here is the one that comes from pnat being a dependent pair, right?

Pnat is:
Sigma x : Nat, 0 < x

[David Renshaw]

I think that makes sense to me now. Thanks for the explanation!

[Yakov Pechersky]

Yeah!

[Reid Barton]

Another strategy for this case is congr, ext, exact hn1