Namespaces for ring lemmas

Stream: general

[Michael Stoll]

There is

 theorem neg_add_eq_sub {α : Type u_1} [subtraction_comm_monoid α] (a b : α) :
-a + b = b - a

in the root name space and defined in algebra.group.basic, but

 theorem tactic.ring.add_neg_eq_sub {α : Type u_1} [add_group α] (a b : α) :
a + -b = a - b

in the tactic.ring namespace and defined in tactic.ring.
Is there a (good) reason for this asymmetry?
(There are a few other statements in tactic.ring that look like they should be in algebra.group.basic or a similar file.)

[Ruben Van de Velde]

You can ignore the lemmas in thetactic.ring namespace, they only exist to be used by the ring tactic

[Michael Stoll]

But add_neg_eq_sub does not seem to exist somewhere else (and I just needed it).

[Michael Stoll]

suggest told me that the statement is tactic.ring.....

[Yaël Dillies]

docs#sub_eq_add_neg

[Michael Stoll]

Thanks. Why is neg_add_eq_sub in the other direction?

[Yaël Dillies]

docs#sub_eq_neg_add also exists. Not sure why neg_add_eq_sub is reversed.

[Eric Wieser]

Tactics often come with peculiarly stated lemmas simply because it's much easier to run the elaborator outside the tactic than it is to build complex term mode proofs within it

[Eric Wieser]

(in my experience, largely due to `(_) notation not working with universe metavariables)

[Yaël Dillies]

That explains docs#tactic.ring.add_neg_eq_sub, not docs#neg_add_eq_sub.

[Mario Carneiro]

Eric Wieser said:

Tactics often come with peculiarly stated lemmas simply because it's much easier to run the elaborator outside the tactic than it is to build complex term mode proofs within it

It's also significantly more efficient. In many cases you don't even need to call the elaborator at all, you just call expr constructors directly

[Eric Wieser]

Ah, the point being that everything is elaborated once at startup rather than on each tactic invocation?