grind needs help

Stream: lean4

[Michael Stoll]

Consider

import Mathlib

open Polynomial

example {f : ℝ[X]} {n : ℕ} (hf : IsMonicOfDegree f (n + 1)) :
    ∃ f₁ f₂ : ℝ[X], (IsMonicOfDegree f₁ 1 ∨ IsMonicOfDegree f₁ 2) ∧ f = f₁ * f₂ := by
  obtain ⟨f₁, hf₁m, hf₁i, f₂, hf₂⟩ :=
    exists_monic_irreducible_factor f <| not_isUnit_of_natDegree_pos f <|
      by grind [IsMonicOfDegree.natDegree_eq]
  have hdegpos := hf₁i.natDegree_pos
  have hdegle := hf₁i.natDegree_le_two
  have hf₁ : f₁.IsMonicOfDegree f₁.natDegree := ⟨rfl, hf₁m⟩
  refine ⟨f₁, f₂, ?_, hf₂⟩
  clear hf₂ hf f₂ hf₁i n f -- hf₁m
  set φ := f₁.IsMonicOfDegree -- without this, `grind` below fails, but not necessary when `clear`ing hf₁m
  have : f₁.natDegree = 1 ∨ f₁.natDegree = 2 := by omega -- without this, `grind` below fails
  grind

I would have expected grind to work without the two lines above it.
But what I find particularly strange is that the line set φ := f₁.IsMonicOfDegree is not necessary when clearing hf₁m first.

The whole thing seems to be very brittle: For example, using extract_goal after the clear tactic above leads to

import Mathlib

open Polynomial

example (f₁ : ℝ[X]) (_ : f₁.Monic) (hdegpos : 0 < f₁.natDegree) (hdegle : f₁.natDegree ≤ 2)
    (hf₁ : f₁.IsMonicOfDegree f₁.natDegree) :
    f₁.IsMonicOfDegree 1 ∨ f₁.IsMonicOfDegree 2 := by
  have : f₁.natDegree = 1 ∨ f₁.natDegree = 2 := by omega -- without this, `grind` below fails
  grind

which does work without the set ... line (but still needs omega to help).

(This is the reason why I was not able to come up with a Mathlib-free example, which I tried.)

[Michael Stoll]

Can this be caused by timeout issues or reaching some internal bounds?

[Michael Stoll]

In any case, I'd have expected this to work:

example {P : Nat → Prop} {m : Nat} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by
  grind -- does not work

[Marcus Rossel]

(deleted)

[Damiano Testa]

If you add

  have : m = 1 ∨ m = 2 := by grind

then grind helps itself!

[Michael Stoll]

But it should not really need that...

[Michael Stoll]

(The proof I'm using in production is interval_cases m <;> tauto, which is perhaps better anyway.)

[Damiano Testa]

Oh, I agree! I was just pointing out that grind does do something with or.

[Markus Himmel]

I'm not an expert on grind, but my understanding from https://lean-lang.org/doc/reference/latest/The--grind--tactic/Case-Analysis/ is that grind will only perform case analysis on things you explicitly tell it to perform case analysis on. This works:

attribute [grind cases] Nat in
example {P : Nat → Prop} {m : Nat} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by
  grind

[Michael Stoll]

example {P : Nat → Prop} {m : Nat} (hm₀ : 0 < m) (hm₂ : m ≤ 2) (h : P m) : P 1 ∨ P 2 := by
  grind [cases Nat]

is maybe even better.

Should cases Nat be on by default?

I guess there is a tension between ease-of-use and performance here, but my preference would tend towards ease-of-use. If I have to remember a dozen ways for how to get grind to do certain things, this is not much better than to have to remember as many tactics...

[Markus Himmel]

Michael Stoll said:

Should cases Nat be on by default?

My guess would be no; one of the reasons why grind works at all is because the tactic and the library annotations are very strict about keeping the search space small, and my guess is that having cases Nat always could slow grind down considerably on goals where you want the linear arithmetic solver to handle the Nat parts of the problem instead of just blindly case-bashing

[Michael Stoll]

Maybe for "small" intervals...

[Kim Morrison]

All of the above examples work on v4.27.0-rc1.