getEqnsFor? non-recursive function

Stream: lean4

[Marcus Rossel]

Is there a way to get nicer equational lemmas for non-recursive functions than what is currently returned by docs4#Lean.Meta.getEqnsFor?? For example:

import Lean

def Bool.toNat : Bool → Nat
  | false => 0
  | true => 1

#eval Lean.Meta.getEqnsFor? ``Bool.toNat (nonRec := true)
#check Bool.toNat._eq_1
/-
Bool.toNat._eq_1 (x✝ : Bool) :
  Bool.toNat x✝ =
    match x✝ with
    | false => 0
    | true => 1
-/

When I was hoping it would return two equations:

Bool.toNat._eq_1 false = 0
Bool.toNat._eq_2 true = 1

Works great for recursive functions

Interestingly, it works great for recursive functions:

import Lean

def fact : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * fact n

#eval Lean.Meta.getEqnsFor? ``fact
#check fact._eq_1 -- fact._eq_1 : fact 0 = 1
#check fact._eq_2 -- fact._eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n

Though not for non-trivial ones:

def Bool.toZero (b : Bool) : Nat :=
  match _h : b with
  | false => 0
  | true  => toZero false
termination_by toZero b => b.toNat
decreasing_by simp_wf; simp_arith [Bool.toNat]; simp [*]

#eval Lean.Meta.getEqnsFor? ``Bool.toZero
#check Bool.toZero._eq_1
/-
Bool.toZero._eq_1 (b : Bool) :
  Bool.toZero b =
    match _h : b with
    | false => 0
    | true => Bool.toZero false
-/

Sidenote on doc-gen4

It would also be nice to have this for doc-gen4, as currently the output for non-recursive definitions can be suboptimal (cf. docs4#Bool.toLBool).

[Marcus Rossel]

Pinging this, as I haven't found a solution yet.

[Joachim Breitner]

It's on the roadmap. We want

• equation lemmas and induction principles for all functions, not just recursive ones
• use the same case-splittint heuristic for all of them

[Marcus Rossel]

(deleted)

[Eric Wieser]

Perhaps lean#2042 should be re-opened, which was intended to track this?