# 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: May 13 2021 at 21:12 UTC