Controlled reduction of proofs

Stream: lean4

[suhr]

For very basic proofs, term reduction is a viable technique for proof simplification. For example, it helped me to discover this little proof:

theorem not_one_le_zero: ¬1 ≤ 0 := by
  suffices any_zero: ∀k, 1 ≤ k → k = 0 → False from
    λh => any_zero 0 h rfl
  exact λk ok => ok.recOn
    (λ(h: 1 = 0) => succ_ne_zero 0 h)
    (λ{k} _ _ (ksz: k.succ = 0) => succ_ne_zero k ksz)

But larger proofs though it's disastrous because it tries to expand every definition.

It would be nice to have a guided version of #reduce that expands definitions only by request, yet automatically does β-reduction.

[Kyle Miller]

This could be a nice metaprogramming exercise. You could copy the definitions of #reduce, its elaborator, and the reduce function, look at how docs#Lean.Meta.whnfUntil works to see how to use docs#Lean.Meta.whnfHeadPred to reduce certain definitions, modify your reduce to use it, and modify your #reduce syntax to take a list of definitions to unfold. The function to use to turn Idents into resolved Names is docs#Lean.Elab.realizeGlobalConstNoOverloadWithInfo