grind in a demo

Stream: lean4

[Floris van Doorn]

I often give a proof of the infinitude of primes in a demo. I tag some lemmas with aesop so that the proof goes a bit more smoothly (mostly hidden from the audience), and then my proof looks something like this:

import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Order.Preorder.Finite

namespace Nat
set_option pp.showLetValues true

alias ⟨_, dvd_of_dvd_add_right⟩ := Nat.dvd_add_iff_right
alias ⟨_, Prime.dvd_factorial_of_le⟩ := Prime.dvd_factorial

attribute [aesop safe apply]
  Set.infinite_of_forall_exists_gt
  Prime.dvd_factorial_of_le
attribute [aesop safe forward]
  factorial_ne_zero
  dvd_of_dvd_add_right
  Nat.minFac_dvd
attribute [simp] and_comm



theorem euclids_theorem :
    { p : ℕ | Prime p }.Infinite := by
  suffices ∀ n : ℕ, ∃ p > n, Prime p
    by aesop
  intro (n : ℕ)
  let N := n ! + 1
  let p := minFac N
  have : Prime p := by
    refine minFac_prime ?_
    aesop
  have : p > n := by
    by_contra! h
    have : p ∣ n ! := by aesop
    have : p ∣ n ! + 1 := by aesop
    aesop
  use p

[Floris van Doorn]

I tried to use grind today instead of aesop, and it mostly works:

import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Order.Preorder.Finite

namespace Nat
set_option pp.showLetValues true

attribute [grind]
  Nat.factorial_ne_zero
  minFac_dvd
  Prime.dvd_factorial
  minFac_eq_one_iff
  dvd_one

attribute [grind =_] Nat.dvd_add_iff_right

attribute [grind ←] Set.infinite_of_forall_exists_gt -- doesn't seem to work

theorem euclids_theorem' :
    { p : ℕ | Prime p }.Infinite := by
  suffices ∀ n : ℕ, ∃ p > n, Prime p
    by grind
  intro (n : ℕ)
  let N := n ! + 1
  let p := minFac N
  have : Prime p := by
    refine minFac_prime ?_
    grind
  have : p > n := by
    by_contra! h
    have : p ∣ n ! := by grind
    have : p ∣ n ! + 1 := by grind
    grind
  use p

[Floris van Doorn]

However, the first grind fails, where it (mostly) has to apply docs#Set.infinite_of_forall_exists_gt. Is this outside the scope of grind (maybe because there is very little to key on in its hypothesis) or am I doing something else wrong?

[Bhavik Mehta]

Perhaps you already saw this, but the diagnostics are giving some more information. First, if you change[grind ←] to [grind? ←], it tells you what it's keyed on:
Set.infinite_of_forall_exists_gt: [@Set.Infinite #4 #2]
Looking at the diagnostic tab from grind's output, it has done an ematching instance using that theorem, but then the Issues tab says

  [issue] failed to create E-match local theorem for
        ∀ (n : ℕ), ∃ p, n + 1 ≤ p ∧ Prime p

So I'm guessing that it matched correctly, but couldn't do anything about it? Anecdotally, I've seen grind sometimes failing for higher-order goals which are otherwise simple, like this, but I'm not sure.

[Chris Henson]

For me, this clarifies the kind of reasoning not currently supported:

import Mathlib.Data.Nat.Prime.Factorial
import Mathlib.Order.Preorder.Finite

namespace Nat
set_option pp.showLetValues true

theorem suffice (h : ∀ n : ℕ, ∃ p > n, Prime p) : { p : ℕ | Prime p }.Infinite := by
  simp_all only [gt_iff_lt]
  have ex (a : ℕ) : ∃ b ∈ {p | Prime p}, a < b := by
    simp only [and_comm, Set.mem_setOf_eq]
    -- `grind` won't work here, but `aesop` will do `simp_all only`
    exact h a
  apply Set.infinite_of_forall_exists_gt
  intro a
  simp only [Set.mem_setOf_eq] at *
  -- `grind` won't work here, but `aesop` will do `simp_all only`
  exact ex a

(there is a config Lean.Grind.Config.lookahead whose docstring is just a TODO, I have wondered if it might correspond to this sort of thing in the future...)

[Floris van Doorn]

@Chris Henson I don't think that identifies the problem. This already fails:

import Mathlib.Order.Preorder.Finite

attribute [grind] Set.infinite_of_forall_exists_gt

lemma foo {s : Set ℕ} (h : ∀ a, ∃ b ∈ s, a < b) : s.Infinite := by
  grind -- fails
  -- apply? -- works

[Floris van Doorn]

@Bhavik Mehta Thanks for your message. I saw most of that output, and I wasn't quite sure what the issue meant or what consequences it had.

[Floris van Doorn]

It's not clear to me in which case grind fails to create E-match local theorems. E.g. in the example below why do 1+4 work but 2+3 fail?

import Mathlib.Order.Preorder.Finite

def P (s : Set ℕ) (x y : ℕ) : Prop := x + y ∈ s
def Q (s : Set ℕ) (x : ℕ) : Prop := x ∈ s

/- uncomment only one example at a time -/
-- 1: works
-- @[grind] lemma foo {s : Set ℕ} (h : ∃ x < 3, Q s x) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∃ x < 3, Q s x) : s.Infinite := by grind

-- 2: fails
-- @[grind] lemma foo {s : Set ℕ} (h : ∃ n, ∃ x < n, Q s x) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∃ n, ∃ x < n, Q s x) : s.Infinite := by grind

-- 3: fails
-- @[grind] lemma foo {s : Set ℕ} {n : ℕ} (h : ∃ x < n, Q s x) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} {n : ℕ} (h : ∃ x < n, Q s x) : s.Infinite := by grind

-- 4: works
-- @[grind] lemma foo {s : Set ℕ} (h : ∃ x, ∃ y, P s x y) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∃ x, ∃ y, P s x y) : s.Infinite := by grind

-- 5: works
-- @[grind] lemma foo {s : Set ℕ} (h : ∀ x, ∀ y, P s x y) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∀ x, ∀ y, P s x y) : s.Infinite := by grind

-- 6: fails
-- @[grind] lemma foo {s : Set ℕ} (h : ∀ x, ∃ y, P s x y) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∀ x, ∃ y, P s x y) : s.Infinite := by grind

-- 7: fails
-- @[grind] lemma foo {s : Set ℕ} (h : ∃ x, ∀ y, P s x y) : s.Infinite := sorry
-- lemma bar {s : Set ℕ} (h : ∃ x, ∀ y, P s x y) : s.Infinite := by grind

[Chris Henson]

I see, I misunderstood what failure you were focused on.

For 2+3, you are wanting the backwards reasoning pattern @[grind ←] on foo? The docs mention that "This may fail if not all of the arguments to the theorem appear in the conclusion". I think it fails for forward patterns for a similar reason.

I struggled with this for a while trying to use grind for cofinite quantification, where you inherently have an argument that is not indexable.