## 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