Zulip Chat Archive

Stream: new members

Topic: ring tactic timing out


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.

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

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.

Kenny Lau (May 29 2020 at 13:19):

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

Kenny Lau (May 29 2020 at 13:20):

but ring requires something stronger than defeq

Alex J. Best (May 29 2020 at 13:47):

You can try ring! sometimes for this.

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: Dec 20 2023 at 11:08 UTC