Grind is impressive

Stream: lean4

[Sorrachai Yingchareonthawornchai]

I'm not sure if this is the right thread to post on. But I want to mention that grind is quite impressive. For example, I use this to prove Pascal's triangle bound in one line.

import Mathlib.Tactic
set_option autoImplicit false

@[grind] def factorial : ℕ → ℕ
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

notation:10000 n "!" => factorial n

@[grind] lemma fact (n :ℕ) : 1 ≤ n ! := by
  induction' n with n ih <;> all_goals grind [factorial]

def P : ℕ → ℕ → ℕ
  | _, 0 => 1
  | 0, _ + 1 => 1
  | a + 1, b + 1 => P (a + 1) b + P a (b + 1)
termination_by a b => a + b

#check P.induct
#check P.induct_unfolding

#eval [P 0 0]
#eval [P 0 1,P 1 0]
#eval [P 2 0,P 1 1, P 2 0]
#eval [P 3 0,P 2 1, P 1 2, P 0 3]
#eval [P 4 0,P 3 1, P 2 2, P 1 3, P 0 4]

-- without grind
lemma P_le_fact ( a b : ℕ ): P a b ≤ (a+b)! := by
  fun_induction P <;> all_goals (try simp_all only [add_zero, fact])
  · rename_i a b ih1 ih2
    calc
      P (a + 1) b + P a (b + 1) ≤ (a + 1 + b) ! + (a + (b + 1)) ! := by rel [ih1, ih2]
        _ ≤ (a + b) * (a + b + 1) ! + (a + 1 + b) ! + (a + (b + 1)) !  := by omega
        _ = ((a + b + 1) + 1) * (a + b + 1)! := by ring_nf
        _ = ((a + b + 1) + 1)! := by bound
        _ = (a + 1 + (b + 1))! := by ring_nf

-- With grind, you can solve the goal in one line.
lemma P_le_fact' ( a b : ℕ ): P a b ≤ (a+b)! := by
  fun_induction P <;> all_goals grind

[(deleted)]

This is its intended use. And in large developments we should use grind often to keep proofs maintainable

[(deleted)]

With grind Lean is light years ahead

[Sorrachai Yingchareonthawornchai]

Is there a way to obtain the proof term from it?

[Kenny Lau]

@Sorrachai Yingchareonthawornchai #print P_le_fact'

[Sorrachai Yingchareonthawornchai]

Thanks. The output proof term is not human-readable...

[Kenny Lau]

well, that is to be expected of powerful tactics

[Yaël Dillies]

Soon there will be a way to print grind proofs as a sequence of calls to grind modules