Zulip Chat Archive

Stream: new members

Topic: motive is not type correct


view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 07:30):

What about simp_rw [z]?

view this post on Zulip 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?

view this post on Zulip Chase Norman (Nov 05 2020 at 07:32):

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

view this post on Zulip Chase Norman (Nov 05 2020 at 07:33):

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

view this post on Zulip 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?

view this post on Zulip Yakov Pechersky (Nov 05 2020 at 07:36):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 09:25):

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

view this post on Zulip Johan Commelin (Nov 05 2020 at 09:26):

It's just that rw is being "silly"

view this post on Zulip 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.

view this post on Zulip 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. "

view this post on Zulip Chase Norman (Nov 05 2020 at 09:35):

I now realize how silly that made me sound.

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 09:35):

actually I think linarith might do this

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 09:36):

import tactic

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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 05 2020 at 09:38):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 21:19):

Do you have an #mwe?

view this post on Zulip Yury G. Kudryashov (Nov 05 2020 at 21:20):

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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Jan 17 2021 at 23:23):

Try simp_rw instead of rw?

view this post on Zulip 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