ring tactic timing out

Stream: new members

[Jack J Garzella]

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]

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]

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]

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

[Kenny Lau]

but ring requires something stronger than defeq

[Alex J. Best]

You can try ring! sometimes for this.

[Kevin Buzzard]

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.