## Stream: new members

### Topic: motive is not type correct

#### Chase Norman (Nov 05 2020 at 07:25):

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 (Nov 05 2020 at 07:30):

What about simp_rw [z]?

#### Yakov Pechersky (Nov 05 2020 at 07:32):

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 (Nov 05 2020 at 07:32):

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

#### Chase Norman (Nov 05 2020 at 07:33):

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

#### Chase Norman (Nov 05 2020 at 07:33):

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 (Nov 05 2020 at 07:36):

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

#### Yakov Pechersky (Nov 05 2020 at 07:36):

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 (Nov 05 2020 at 07:37):

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 (Nov 05 2020 at 07:37):

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

#### Kevin Buzzard (Nov 05 2020 at 09:04):

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 (Nov 05 2020 at 09:06):

"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 (Nov 05 2020 at 09:17):

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

#### Johan Commelin (Nov 05 2020 at 09:25):

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

#### Johan Commelin (Nov 05 2020 at 09:26):

It's just that rw is being "silly"

#### Kevin Buzzard (Nov 05 2020 at 09:32):

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 (Nov 05 2020 at 09:34):

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 (Nov 05 2020 at 09:35):

I now realize how silly that made me sound.

#### Kevin Buzzard (Nov 05 2020 at 09:35):

actually I think linarith might do this

#### Kevin Buzzard (Nov 05 2020 at 09:35):

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 (Nov 05 2020 at 09:36):

import tactic

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


#### Kevin Buzzard (Nov 05 2020 at 09:37):

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 (Nov 05 2020 at 09:37):

import tactic

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


#### Kevin Buzzard (Nov 05 2020 at 09:38):

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

#### Chase Norman (Nov 05 2020 at 19:11):

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 (Nov 05 2020 at 21:19):

Do you have an #mwe?

#### Yury G. Kudryashov (Nov 05 2020 at 21:20):

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

#### Lars Ericson (Jan 17 2021 at 22:26):

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 (Jan 17 2021 at 23:23):

Try simp_rw instead of rw?

#### Kyle Miller (Jan 17 2021 at 23:39):

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

Last updated: May 12 2021 at 05:19 UTC