Pretty printing equations

Stream: lean4

[Henrik Böving]

Hi. I'm currently working on listing the equations of definitions for doc-gen4, my very naive approach to this was :

#eval show MetaM _ from do
  let name := `Array.insertionSort.swapLoop
  let foo := (←getEqnsFor? name).mapM (λ eqs => eqs.mapM (mkConstWithFreshMVarLevels · >>= inferType))

And this approach does seem to work quite nicely but once it arrives at Array.insertionSort.swapLoop defined over here: https://leanprover-community.github.io/mathlib4_docs/Init/Data/Array/InsertionSort.html#Array.insertionSort.swapLoop it complains about the following:

uncaught exception: tactic 'generalize' failed, result is not type correct
  ∀ (x : ℕ) (x_1 : x = x),
    Array.insertionSort.swapLoop lt a x h =
      match x, x_1 with
      | 0, he => a
      | Nat.succ j', he =>
        let_fun h' := (_ : j' < Array.size a);
        if lt (Array.get a { val := x, isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
          Array.insertionSort.swapLoop lt (Array.swap a { val := x, isLt := h } { val := j', isLt := h' }) j'
            (_ : j' < Array.size (Array.swap a { val := x, isLt := h } { val := j', isLt := h' }))
        else a
α : Type u_1
lt : α → α → Bool
a : Array α
j : ℕ
h : j < Array.size a
⊢ Array.insertionSort.swapLoop lt a j h =
    match j, (_ : j = j) with
    | 0, he => a
    | Nat.succ j', he =>
      let_fun h' := (_ : j' < Array.size a);
      if lt (Array.get a { val := j, isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
        Array.insertionSort.swapLoop lt (Array.swap a { val := j, isLt := h } { val := j', isLt := h' }) j'
          (_ : j' < Array.size (Array.swap a { val := j, isLt := h } { val := j', isLt := h' }))
      else a

And I looked at the code and am entirely confused by this error message because neither in the code for swap loop nor in the entire insertion sort file can I ever see the generalize tactic getting mentioned. Can someone enlighten me on what's going on?

[Gabriel Ebner]

The error is not from the definition of Array.insertionSort.swapLoop, it's from the code that generates the equational lemmas.

[Gabriel Ebner]

In contrast to Lean 3, equational lemmas are not automatically created when you add a definition but only when they are first used.

[Gabriel Ebner]

Does attribute [simp] Array.insertionSort.swapLoop also fail with this error?

[Gabriel Ebner]

You can report that as an issue on the lean 4 bugtracker.

[Henrik Böving]

Yup it doesnt like that either with the same error.

[Henrik Böving]

Aight

[Henrik Böving]

https://github.com/leanprover/lean4/issues/986

[Henrik Böving]

Got another one with todays nightly! xd

#eval show MetaM _ from do
  let name := `Lean.Elab.Term.resolveLocalName.loop
  let foo := (←getEqnsFor? name).mapM (λ eqs => eqs.mapM (mkConstWithFreshMVarLevels · >>= inferType))

@Gabriel Ebner shall I open another issue? Should I blacklist this and continue trying to generate so I can catch all that dont work right now?

[Gabriel Ebner]

I would turn it into a warning for now (and have the docs say that the equations could not be generated for that definition). Then we'll have a better idea of how many errors there are.

[Gabriel Ebner]

It might also be better to make one issue with all failing declarations. Generating equation lemmas for definitions in Lean.* is not high priority though since nobody is going to use them with simp.

[Henrik Böving]

Yeah that was my idea with the blacklisting and trying again, I'm seeing another thing I'm a bit confused after doing this though.... I'm getting a maximum number of heartbeats reached at 100000 despite setting it to a much much higher value here https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Load.lean#L49. did I missunderstand how exactly heartbeats work?

[Gabriel Ebner]

I'm not sure what your model of heartbeats was. The number you given is for the whole documentation generation, I would try to set it per-file or per-declaration.

There are also several places which set a lower limit, that's what you're probably seeing.

[Henrik Böving]

image.png progress :octopus:, I'll post a list of functions that fail to compute their equational lemmata to the issue tracker tomorrow.

[Henrik Böving]

image.png also ehhh...kiiiinda works for bigger stuff but Idk if we want that xd

[Henrik Böving]

https://github.com/leanprover/lean4/issues/998 This is all I could find with reasonably high heartbeat per declaration values, it might be possible that there are hidden some more behind timeouts right now but either way these error expressions are already pretty wild.

[Henrik Böving]

Also now where I'm done with the equation implementation I'm noticing many functions dont even have equation lemmata at all? For example:

#eval show MetaM _ from do
  getEqnsFor? `id

Simply returns none, is this expected? Do functions that are defined without case distinction just not get an equation lemma (which would basically be the definition anyways) at all? And if that is the case, should I just print the definition without binders if I get back a none from getEqnsFor?or is there some other case I have to be aware of?

[Leonardo de Moura]

Yes, it is expected. Lean only creates equations for definitions where structural or well-founded recursion was used.

And if that is the case, should I just print the definition without binders if I get back a none from getEqnsFor?

Yes. For example, if getEnqnsFor? for foo returns none, then simp [foo] just uses the actual definition.

or is there some other case I have to be aware of?

partial definitions should be treated as opaque constants.