Zulip Chat Archive

Stream: new members

Topic: Lean doesn't find instance of something that's right there


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 22:38):

Weird problem -- I have my goal, which is (x ⋆ y) → (y ⋆ z) → (x ⋆ z) (for some operation ) and I have a hypothesis Hxy : x = y. But when I try rw Hxy, Lean tells me:

rewrite tactic failed, did not find instance of the pattern in the target expression
  x

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 22:39):

But... it's right there.

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:43):

Post a MWE

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:44):

Sometimes it's because you have two variables called x, sometimes it's because something needs to be done by type class inference and type class inference fails but the error mesage is that the rewrite failed, there are all sorts of reasons.

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:54):

Another reason it fails is that you can't rewrite under a binder. Does simp only [Hxy] work? As you can see, it's difficult to diagnose without a MWE.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 22:55):

Ok, I got the problem (it was the "two variables called x" thing) -- I had defined a symbol S for fin 2 and mid-way through the proof had done rw S at z y x, which caused two sets of variables x y z to be defined.

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:56):

rw is a fickle beast.

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 22:56):

(although I'm not sure why that happened -- usually when you do rw something at something, it just changes the statement, not create new ones.)

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:56):

It takes a while to get to know its foibles

view this post on Zulip Kevin Buzzard (Oct 15 2018 at 22:58):

example (n x y : ) (h : n > 0  x = y) : x + 1 = y + 2 :=
begin
  rw h,
  -- one goal became 2 -- we now need a proof of n > 0
  sorry,sorry
end

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 15 2018 at 23:02):

Yeah, I've encountered that before, but that actually makes sense (and is useful!). Treating rewrites differently based on whether they're done on a natural number or a proof is just weird.


Last updated: May 12 2021 at 05:19 UTC