Zulip Chat Archive

Stream: new members

Topic: ring tactic timing out


view this post on Zulip Jack J Garzella (May 29 2020 at 03:58):

I'm not sure if this is a bug, or if it's me not understanding what computation is. Here is my #mwe:
The following works fine

open polynomial
example {R : Type u} [comm_ring R] (a : R) :
(X - C a) = (X + C (-a)) :=
begin
have e : (X - C a) = (X + C (-a)),
by { simp [map_neg], ring },
exact e
end

But if I use the following:

open polynomial
example {R : Type u} [comm_ring R] (a : R) :
(X - C a) = (X + C (-a)) :=
begin
let f := (X - C a),
have e : f = (X + C (-a)),
by { simp [map_neg], ring },
exact e
end

I get (deterministic) timeout.

view this post on Zulip Shing Tak Lam (May 29 2020 at 04:12):

If you look at the goal after simp [map_neg] in the second one (delete the ring), you have ⊢ f = X + -C a, which ring can't do anything about. If you give simp f, then ring can solve it.

example {R : Type u} [comm_ring R] (a : R) :
(X - C a) = (X + C (-a)) :=
begin
  let f := (X - C a),
  have e : f = (X + C (-a)),
  by { simp [map_neg, f], ring },
  exact e
end

view this post on Zulip Jack J Garzella (May 29 2020 at 13:13):

Thanks so much! The only part I still don't get is why exact e is able to correctly prove the theorem, when e has type f = (X + C (-a)) and not type (X - C a) = (X + C (-a)). This seems to be exactly the same issue that ring is worrying about, replacing something with another thing which is definitionally equal.

view this post on Zulip Kenny Lau (May 29 2020 at 13:19):

f is defeq to X - C a so exact (which only cares about defeq) works

view this post on Zulip Kenny Lau (May 29 2020 at 13:20):

but ring requires something stronger than defeq

view this post on Zulip Alex J. Best (May 29 2020 at 13:47):

You can try ring! sometimes for this.

view this post on Zulip Kevin Buzzard (May 29 2020 at 14:46):

Some tactics work up to definitional equality, and some up to syntactic equality ("literally pressing the same buttons on your keyboard in the same order, modulo variable renaming" equality). exact is a good example of one which works up to definitional equality, and rw is a good example of one which works up to syntactic equality.


Last updated: May 13 2021 at 21:12 UTC