Any high-powered tactics for these MIL chapter 2 examples?

Stream: new members

[Isak Colboubrani]

For a demonstration to my fellow undergraduates, I first show how to solve some MIL exercises from "first principles" and then how to solve them using "high-powered tactics."

Is it correct to claim that the following four examples from MIL Chapter 2 currently cannot be solved in one step using a Mathlib zero-argument high-powered tactic (think ring, simp, etc.)? (Of course, they can be solved with exact? as shown below, which is nice—and one might even consider exact? high-powered in its own right.)

import Mathlib

example (R : Type) [Ring R] (a : R) : 2 * a = a + a := by
  exact _root_.two_mul a
example (R : Type) [Ring R] (a b : R) : a - b = a + -b := by
  exact sub_eq_add_neg a b
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : -a = b := by
  exact neg_eq_of_add_eq_zero_right h
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : a = -b := by
  exact eq_neg_of_add_eq_zero_left h

[Etienne Marion]

The first two are solved by noncomm_ring. I'm not sure but I don't see how a single tactic could solve the last two. Tactics like ring, simp etc. are mostly about rewriting to get a simpler expression, but in this case it's more than just basic rewriting, you need a non trivial lemma which cannot be triggered by the tactic itself.

[Kevin Buzzard]

Yeah hint solves these because it tries exact?. I agree, I cannot think offhand of a tactic which does "polyrith for additive abelian groups" -- abel doesn't look at hypotheses, I believe.

[Philippe Duchon]

So [Ring R] says R is a not-necessarily-commutative ring, but the corresponding tactic is noncomm_ring while ring requires commutativity? This is not that intuitive!

[Kevin Buzzard]

Yes everything you say is correct :-)

[Kevin Buzzard]

And mostly this is for historical reasons.

[Kyle Miller]

Maybe you want [CommRing R] instead of [Ring R] for your examples? (I suppose though that if you're wanting to show MIL exercises you can't just change the problem!)

[Isak Colboubrani]

@Kyle Miller That's a good suggestion, and I did consider it. However, while it would enable me to use polyrith, I believe there's a clear pedagogical advantage in keeping everything fully aligned with MIL. This approach lets my audience see that the demo is truly based on a "nothing-up-my-sleeve" method; in other words, I haven't adjusted the examples to make the current tactics appear more (or less) impressive than they really are.

[Isak Colboubrani]

@Etienne Marion Great, noncomm_ring successfully handles the first two cases—thanks a lot!

Now I'm left with only the following two examples from MIL Chapter 2, which currently can't be solved in a single step using a zero-argument, high-powered Mathlib tactic:

import Mathlib
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : -a = b := by
  exact neg_eq_of_add_eq_zero_right h
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : a = -b := by
  exact eq_neg_of_add_eq_zero_left h

[Aaron Liu]

Does exact? count?

[Isak Colboubrani]

@Aaron Liu See my original message:

Is it correct to claim that the following four examples from MIL Chapter 2 currently cannot be solved in one step using a Mathlib zero-argument high-powered tactic (think ring, simp, etc.)? (Of course, they can be solved with exact? as shown below, which is nice—and one might even consider exact? high-powered in its own right.)

[Isak Colboubrani]

I found that the final two examples from MIL chapter 2 can be solved in a single step using a zero-argument Mathlib tactic. rw_search does the job!

import Mathlib
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : -a = b := by
  rw_search
example (R : Type) [Ring R] (a b : R) (h : a + b = 0) : a = -b := by
  rw_search

I'm thrilled that all the examples in MIL chapter 2 can be proved using zero-argument Mathlib tactics—it makes for a great demo.

Is there any reason why rw_search isn't more widely used or discussed? Judging by the Zulip history, it doesn't seem to be very well known.

[Kyle Miller]

Why are you accepting rw_search and not exact?? Both of these tactics are similar in that they search through the whole library for lemmas that will close the goal, and then propose a replacement.

[Isak Colboubrani]

@Kyle Miller That's a really good question; it doesn't make any sense at all. I mistakenly believed that exact? only provided a suggestion (which one would then accept using the "Try this: […]" prompt to get to exact […]) and did not close the goal itself.

I'm not sure where I got that idea (perhaps the question mark misled me), but exact? indeed closes the goal and requires no arguments, so it should absolutely be accepted. I apologize to @Aaron Liu and @Kevin Buzzard for overlooking your correct suggestion of exact? earlier in this thread—I wasn’t paying attention at the time :big_smile:

[Kyle Miller]

The idea with these two tactics is that they're really slow, so they give you a way to "cache" the result by replacing themselves with something equivalent (and hopefully faster) :-)

[Kyle Miller]

I think rw? replaced rw_search, but I'm not sure what the current state is.

[Ruben Van de Velde]

No, rw_search can find chains of rewrites, unlike rw?

[Jireh Loreaux]

Philippe Duchon said:

So [Ring R] says R is a not-necessarily-commutative ring, but the corresponding tactic is noncomm_ring while ring requires commutativity? This is not that intuitive!

True, but ring will now give you a message with these suggestions when it fails to close the goal, so it's not too bad.

[Isak Colboubrani]

Is it correct to claim that the following four example inequalities (from MIL chapter 2 section 3) currently cannot be solved in one step using a Mathlib zero-argument high-powered tactic (think linarith, rw?, rw_search, etc.)?

import Mathlib

example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + Real.exp c + e < b + Real.exp d + e := by sorry
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by sorry
example (a b : ℝ) : |a*b| ≤ (a^2 + b^2)/2 := by sorry
example (a b : ℝ) (h : a ≤ b) : Real.log (1 + Real.exp a) ≤ Real.log (1 + Real.exp b) := by sorry

[Jireh Loreaux]

gcongr solves (2) and (4), and it almost solves (1). It only doesn't because gcongr is "picky" for performance reasons. But if you give it an intermediate goal it can do it.

[Jireh Loreaux]

import Mathlib

example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : c < d) : a + Real.exp c + e < b + Real.exp d + e := by
  calc _ ≤ b + Real.exp c + e := by gcongr
    _ < b + Real.exp d + e := by gcongr
example (a b c : ℝ) (h : a ≤ b) : c - Real.exp b ≤ c - Real.exp a := by gcongr
example (a b : ℝ) : |a*b| ≤ (a^2 + b^2)/2 := by sorry
example (a b : ℝ) (h : a ≤ b) : Real.log (1 + Real.exp a) ≤ Real.log (1 + Real.exp b) := by gcongr

[Isak Colboubrani]

Thanks, that's a great find! I completely overlooked gcongr.

Would it be possible for teach hint to suggest using gcongr in cases like this, similar to how it recommends linarith when applicable?

[Jireh Loreaux]

just register_hint gcongr

[Jireh Loreaux]

You can probably PR that to Mathlib in a suitable place (I'm not sure where at the moment).

[Isak Colboubrani]

Very nice. I didn't know it was that easy!

[Isak Colboubrani]

These are the current instances of register_hint:

Mathlib/Tactic/Common.lean:register_hint split
Mathlib/Tactic/Common.lean:register_hint intro
Mathlib/Tactic/Common.lean:register_hint aesop
Mathlib/Tactic/Common.lean:register_hint simp_all?
Mathlib/Tactic/Common.lean:register_hint exact?
Mathlib/Tactic/Common.lean:register_hint decide
Mathlib/Tactic/Common.lean:register_hint omega
Mathlib/Tactic/Linarith.lean:register_hint linarith

[Isak Colboubrani]

Should norm_num be included in that list as well?

If so, it seems that norm_num would need to be modified so that it fails when no rules are applied. Do you think that's a problematic change? Could it potentially cause any issues?

[Kevin Buzzard]

The longer the list, the longer it will take hint to fail, but I don't recall seeing anyone complaining that hint takes a long time, so I would try making a PR adding the options you want to see

[Kevin Buzzard]

I don't think intro fails when it does nothing?

[Damiano Testa]

I think that intro may fail, but intros does not.