motive is not type correct

Stream: new members

[Chase Norman]

I have a goal of type l.nth_le (l.length - 2).succ bound = l.nth_le i i_bound and a hypothesis z of type i=0. When I use the tactic rw z, I get the following error rewrite tactic failed, motive is not type correct λ (_a : ℕ), l.nth_le (l.length - 2).succ bound = l.nth_le i i_bound = (l.nth_le (l.length - 2).succ bound = l.nth_le _a i_bound).

change fails to recognize it too. I also can't get set or congr to work. Any ideas?

[Yakov Pechersky]

What about simp_rw [z]?

[Yakov Pechersky]

But why do you have a goal that is the equality of equalities? Did you congr too deep? Or as the result of a convert?

[Chase Norman]

This worked! Thanks a bunch. I'm not sure what you mean by equality of equalities.

[Chase Norman]

I'm trying to show that two elements of a list are equal.

[Chase Norman]

Is there something I'm missing as far as how you came up with simp_rw? Is it just a general catch-all for these types of errors?

[Yakov Pechersky]

Hmm maybe it's just the error that has the _ = _ = (_ = _) structure

[Yakov Pechersky]

I've seen these motive errors a lot when working with lists or vectors with some length constraint. And that experience has taught me that simp_rw or just simp [...] works. In fact, simp_rw is just a wrapper around simp only [...] iirc.

[Yakov Pechersky]

simp is able to see through more layers than rw. There is some work going on to have a better, dependent-equality cognization dep_rw, but in the meantime, simp related tools will work.

[Yakov Pechersky]

Careful though, you can get some weird loops if you do simp_rw [<- vector.cons_head_tail v] for example.

[Kevin Buzzard]

The error _means_ that your goal contains a proof of something involving i, and when you try to change i to 0 with a rewrite it didn't change the proof, so the proof still mentioned i but it was now supposed to be a proof about 0, and Lean gets confused. It "didn't rewrite enough", in some sense. simp_rw tries harder to rewrite.

[Kevin Buzzard]

"Motive is not type correct" just means something like "this thing is supposed to be a pair (i,P) where P is a proof of something involving i, but you just presented me with (0,P) with P a proof of something involving i instead of 0, so (0,P) is not an object with a well-defined type as far as I can see"

[Chase Norman]

I'm surprised that the i = 0 is not enough for Lean to determine that proofs involving i also work for 0

[Johan Commelin]

It is... as you just noticed by using simp_rw

[Johan Commelin]

It's just that rw is being "silly"

[Kevin Buzzard]

Every tactic has some (often quite well-understood, and also often quite well-defined) domain where it works effectively, and outside this domain it might fail, and the reason for failure isn't because the tactic is stupid, it's because the tactic was not designed to work here.

[Kevin Buzzard]

You can see linarith failing on goals where to a mathematician it "should obviously work" but it doesn't work because it didn't use the hypothesis "x < 37" because it was part of a bigger hypothesis "x < 37 and y < 42". So you say "why didn't linarith just extract the hypothesis x<37 from the "and" hypothesis?" and the answer is "linarith doesn't do "and"". And you say "well doesn't that mean "linarith" is stupid?" and they basically reply "no, it means that splitting up "and" clauses is not linarith's job, and if we made it linarith's job then tomorrow you would ask it to start doing some other basic logic too. "

[Chase Norman]

I now realize how silly that made me sound.

[Kevin Buzzard]

actually I think linarith might do this

[Kevin Buzzard]

but you can see the point I'm making. The idea is that tactics do one job, and when they fail it's often because they were asked to do a job which they weren't designed to do.

[Kevin Buzzard]

import tactic

example (x y : ℕ) (h : x < 37 ∨ x < 37) :
  x < 38 :=
begin
  linarith -- fails
end

[Kevin Buzzard]

obviously "the general theory of inequalities" should solve this goal, but linarith doesn't because it won't do the cases on the "or".

[Kevin Buzzard]

import tactic

example (x y : ℕ) (h : x < 37 ∨ x < 37) :
  x < 38 :=
begin
  cases h;
  linarith -- works
end

[Kevin Buzzard]

There is a more primitive version of rewrite called ▸ and that fails in even more cases.

[Chase Norman]

I have another issue that is similar. The case seems simpler, but it's even more resistant to these tactics. My goal is int.of_nat {v : V | P.P v x y}.to_finset.card - int.of_nat {v : V | P.P v y x}.to_finset.card > 0 and I have int.of_nat {v : V | P.P v y x}.to_finset.card = 0. I hope to be able to achieve int.of_nat {v : V | P.P v x y}.to_finset.card - 0 > 0.

rw, congr', simp_rw all failing me.

[Yury G. Kudryashov]

Do you have an #mwe?

[Yury G. Kudryashov]

There can be different issues with hidden (implicit and typeclass) arguments.

[Lars Ericson]

At the last step here:

import data.rat.basic
import data.nat.basic
import data.num.prime
import tactic
import tactic.slim_check
open tactic
open rat
open nat

lemma mul_injective
        {a b : ℚ}
        {n m : ℕ}
        (ha : a.denom = 2 ^ n)
        (hb : b.denom = 2 ^ m):
        ∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
  cases a,
  cases b,
  simp at *,
  constructor,
  rw ha at a_cop,
  rw hb at b_cop,
  rw ha, -- error
end

the tactic state is:

n m : ℕ,
a_num : ℤ,
a_denom : ℕ,
a_pos : 0 < a_denom,
a_cop : a_num.nat_abs.coprime a_denom,
b_num : ℤ,
b_denom : ℕ,
b_pos : 0 < b_denom,
b_cop : b_num.nat_abs.coprime b_denom,
ha : a_denom = 2 ^ n,
hb : b_denom = 2 ^ m,
a_cop : a_num.nat_abs.coprime (2 ^ n),
b_cop : b_num.nat_abs.coprime (2 ^ m)
⊢ ({num := a_num, denom := a_denom, pos := a_pos, cop := a_cop} *
       {num := b_num, denom := b_denom, pos := b_pos, cop := b_cop}).denom =
    2 ^ ?m_1

I want to substitute 2^n for a_denom in the goal. Lean throws error

rewrite tactic failed, motive is not type correct
  λ (_a : ℕ),
    ({num := a_num, denom := a_denom, pos := a_pos, cop := a_cop} *
           {num := b_num, denom := b_denom, pos := b_pos, cop := b_cop}).denom =
        2 ^ ?m_1 =
      (({num := a_num, denom := _a, pos := a_pos, cop := a_cop} *
            {num := b_num, denom := b_denom, pos := b_pos, cop := b_cop}).denom =
         2 ^ ?m_1)

How do I get this rewrite to work?

How do I get the multiplication to be performed/expanded out in the goal so that I get a single {} structure instead of {} * {}?

Once I have a single {} in the goal, how can I rewrite that into either multiple goals or make an assertion that the resulting structure is a rational?

[Eric Wieser]

Try simp_rw instead of rw?

[Kyle Miller]

When you want do do a dependent rewrite of a variable (like ha : a_denom = 2 ^ n) something that tends to work is subst a_denom