Why doesn't the ring tactic solve "0 = -a + a"?

Stream: general

[Ching-Tsun Chou]

I was doing the following exercise in section 2.5 of "Mathematics in Lean:

image.png

To my surprise, I found that the ring tactic does not solve the equalities at either step 1 or step 3. Why is that so?

The following is the context of this exercise:

image.png

[Kim Morrison]

Because you are working in Nat, which is a semiring not a ring.

[Kim Morrison]

Try omega instead.

[Ching-Tsun Chou]

Why am I working in Nat? The variables an and b are of type R, which is a StrictOrderedRing.

[Kim Morrison]

Please use a #mwe, not a screenshot.

[Kim Morrison]

(Looking at your first screenshot there is no information about where the variables live.)

[Ching-Tsun Chou]

Here is a MWE:

import Mathlib.Tactic
import Mathlib.Util.Delaborators
import Mathlib.Topology.MetricSpace.Basic

section
variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)

example (h : a ≤ b) : 0 ≤ b - a := by
--  sorry
 calc 0 = -a + a := by simp
      _ ≤ -a + b := by apply add_le_add_left h
      _ = b + -a := by rw [add_comm]
      _ = b - a := by { rw [← sub_eq_add_neg] }

end

[Ching-Tsun Chou]

My question is: why doesn't the ring tactic solve steps 1 and 3?

[Kim Morrison]

Not your question, but

import Mathlib.Tactic
import Mathlib.Util.Delaborators
import Mathlib.Topology.MetricSpace.Basic

section
variable {R : Type*} [StrictOrderedRing R]
variable (a b c : R)

example (h : a ≤ b) : 0 ≤ b - a := by
--  sorry
 calc 0 = -a + a := by abel
      _ ≤ -a + b := by apply add_le_add_left h
      _ = b + -a := by abel
      _ = b - a := by abel

end

does work.

[Ching-Tsun Chou]

That's a good point. But since a ring's + operation forms an abelian group, shouldn't the ring tactic be able to solve such goals as well?

[Kyle Miller]

ring likes commutative rings (I'm just copying the italics from the documentation when you hover over ring, it was a good reminder, since this example was puzzling me). Changing it to StrictOrderedCommRing makes it work.

[Ching-Tsun Chou]

Well, I tried noncomm_ring. It worked at step 3 but still fails at step 1.

[Ching-Tsun Chou]

In fact, noncomm_ring cannot prove "a = a + 0", either.

[Yan Yablonovskiy]

Ching-Tsun Chou said:

In fact, noncomm_ring cannot prove "a = a + 0", either.

This is probably irrelevant, but out of my curiosity -- how does Lean know here the 0 is the additive identity for R and not Nat/Int etc? It is inferred correctly from the type of a?

[Kyle Miller]

If you hover over 0 in the Infoview, you can see it's actually the more complicated @OfNat.ofNat R 0 Zero.toOfNat0 expression that says in which way 0 : Nat should be interpreted as an element of R.

[Kyle Miller]

It's a consequence of the elaboration process, where it does in this case get the type for the right-hand operand of + from the left-hand a

[Kyle Miller]

Worse @Ching-Tsun Chou , noncomm_ring doesn't work on that example even for commutative rings.

example {R : Type*} [CommRing R] (a b : R) : a + 0 = a := by noncomm_ring -- fails

[Kyle Miller]

Though if you follow its suggestion to use abel it does work.

[Ching-Tsun Chou]

Good to know the idiosyncrasies of these tactics.

[Johan Commelin]

Ching-Tsun Chou said:

In fact, noncomm_ring cannot prove "a = a + 0", either.

That sounds like a bug to me.

[Kim Morrison]

example : a + 0 = a := by noncomm_ring

prints "Try abel instead", so I think it is working fine.

[Ching-Tsun Chou]

@Kim Morrison , I don't quite understand your comment. Are you saying that noncomm_ring is not supposed to work on "a + 0 = a"? What exactly is noncomm_ring supposed to be capable of solving?
Furthermore, it seems that noncomm_ring "knows" that abel may work. Why doesn't it just try it?
Sorry for my naïveté. I am a new user.

[Kevin Buzzard]

(these are good questions, don't worry!)

[Kim Morrison]

I think the general design principle here is that if an "expensive" tactic notices that a "cheap" tactic suffices, it should work, but print a warning suggesting that you change the tactic script (e.g. how simpa using X suggests simp if it closes the goal without using X).

Here, I think noncomm_ring should be printing a warning, not an error (PR very welcome!)

[Kim Morrison]

That said, noncomm_ring is not particular expensive, so I guess we could just let it run. I would be a little sad to end up with a whole lot of noncomm_ring proofs in Mathlib where abel would suffice.

[Kim Morrison]

I think we should write a algebra? tactic that tries all of ring, noncomm_ring, module, abel, etc, and reports the first one that closes the goal!

[Kim Morrison]

(PR welcome! :-)

[Ching-Tsun Chou]

Thanks for the explanation! Unfortunately, I'm still a beginner and do not know how to write tactics yet.

[Ching-Tsun Chou]

Is there a combinator of some kind that can take a list of tactics and try them one by one until either one of them succeeds or none succeeds and a failure is declared?

[Johan Commelin]

Yes, indeed there is. It's called first. See for example Mathlib/Tactic/Ring/RingNF.lean

`(tactic| first | ring1 | try_this ring_nf) -- line 261

[Ching-Tsun Chou]

Thanks for the pointer!