Zulip Chat Archive

Stream: new members

Topic: ring tactic error


view this post on Zulip Yakov Pechersky (Jul 26 2020 at 21:30):

What's going on here? Shouldn't ring just no-op here and not break? It used to work:

import data.matrix.notation

open_locale big_operators

-- this used to work
example {R : Type*} [field R] :  f : fin 2  R,  x : fin 2, f x = f 0 + f 1 :=
begin
  intro f,
  calc
   x : fin 2, f x = _ + _ : rfl
  ...              = f 0 + f 1 : by { simp, ring, refl }
end

-- this works now
example {R : Type*} [field R] :  f : fin 2  R,  x : fin 2, f x = f 0 + f 1 :=
begin
  intro f,
  calc
   x : fin 2, f x = _ + _ : rfl
  ...              = f 0 + f 1 : by { simpa }
end

view this post on Zulip Yakov Pechersky (Jul 26 2020 at 21:35):

Specifically, I had code at https://github.com/pechersky/e222/blob/fa698275f1b4dc98a502866b5dfe2eb341ac8e79/src/test2.lean#L74, using mathlib commit 490a09b04288034ab4e12a5456ee09698bdff797 but I cannot locate that commit now...

view this post on Zulip Rob Lewis (Jul 26 2020 at 22:10):

You need import tactic.ring

view this post on Zulip Rob Lewis (Jul 26 2020 at 22:11):

There were prs recently refining the import hierarchy, it's probably not imported by data.matrix.notation anymore.


Last updated: May 08 2021 at 10:12 UTC