Why does an internal term produced by Lean's equation compiler have holes in it?

Question

Section 4.7 of the Lean reference manual (version 3.3) gives an example of a division function defined by well-founded recursion. I used the #print command to inspect the internal term that the equation compiler generates, and I found that it has two holes in it. The code below shows the original function, and an internal term that corresponds to it that was produced by the print command (using Lean version 3.48.0).

def wfdiv : ℕ → ℕ → ℕ
| x y :=
  if h : 0 < y ∧ y ≤ x then
    have x - y < x,
    from nat.sub_lt (lt_of_lt_of_le h.left h.right) h.left,
    wfdiv (x - y) y + 1
 else
   0

#eval wfdiv 25 6
-- result: 4

-- set_option pp.generalized_field_notation false
-- #print wfdiv
-- #print wfdiv._main
-- #print wfdiv._main._pack


def «printed wfdiv._main._pack» : Π (_x : Σ' (ᾰ : ℕ), ℕ), (λ (_x : Σ' (ᾰ : ℕ), ℕ), ℕ) _x :=
λ (_x : Σ' (ᾰ : ℕ), ℕ),
  well_founded.fix has_well_founded.wf
    (λ (_x : Σ' (ᾰ : ℕ), ℕ),
       psigma.cases_on _x
         (λ (fst snd : ℕ),
            id_rhs ((Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ) → ℕ)
              (λ (_F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ),
                 dite (0 < snd ∧ snd ≤ fst)
                   (λ (h : 0 < snd ∧ snd ≤ fst),
                      have this : fst - snd < fst, from _,
                      _F ⟨fst - snd, snd⟩ _ + 1)
                   (λ (h : ¬(0 < snd ∧ snd ≤ fst)), 0))))
    _x

def «printed wfdiv._main» : ℕ → ℕ → ℕ
:= λ (ᾰ ᾰ_1 : ℕ), «printed wfdiv._main._pack» ⟨ᾰ, ᾰ_1⟩

#eval «printed wfdiv._main» 25 6
-- result: 4

Note that the second #eval shows that «printed wfdiv._main» is still computationally effective even though it has holes in it.

The first hole is in the line have this : fst - snd < fst, from _,, and the Lean emacs mode describes it with

30:57: don't know how to synthesize placeholder
context:
_x _x : Σ' (ᾰ : ℕ), ℕ,
fst snd : ℕ,
_F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ,
h : 0 < snd ∧ snd ≤ fst
⊢ fst - snd < fst

The second hole is in the line _F ⟨fst - snd, snd⟩ _ + 1), and the Lean emacs mode describes it with

31:43: don't know how to synthesize placeholder
context:
_x _x : Σ' (ᾰ : ℕ), ℕ,
fst snd : ℕ,
_F : Π (_y : Σ' (ᾰ : ℕ), ℕ), has_well_founded.r _y ⟨fst, snd⟩ → ℕ,
h : 0 < snd ∧ snd ≤ fst,
this : fst - snd < fst
⊢ has_well_founded.r ⟨fst - snd, snd⟩ ⟨fst, snd⟩

The < and has_well_founded.r terms both have type Prop when applied to two arguments. Is it correct to say that the equation compiler is omitting these essentially due to "proof irrelevance" (described in section 3.7 of the manual)? In other words, the equation compiler knows that these propositions are true, and also knows that they aren't needed for the actual computation, and so therefore in the code it just leaves them as hypothesized. Is that roughly correct?

Assuming that I'm understanding the situation correctly, then I have one more question about this: would the performance of the code be negatively impacted if those holes were filled in? In other words, is the compiler leaving those terms as holes simply because they are computationally irrelevant and so there's no reason to bother filling them in? or is it leaving them as holes because doing so actually improves performance?

Answer 1

You can see the proofs by putting

set_options pp.proofs true

before the #print. (pp.all true also works but with much harder to read output.)

The default of the pretty printer is to have pp.proofs false. I think the docs (found in #help options) are a bit outdated:

pp.proofs (Bool) (pretty printer) if set to false, the type will be displayed instead of the value for every proof appearing as an argument to a function (default: true)

It seems to be doing what the Lean 4 docs say:

"(pretty printer) if set to false, replace proofs appearing as an argument to a function with a placeholder"

Also, if you want to test this, it only replaces proofs with _ if the proof is more than one token:

def foo (h : true) : nat := 0
def bar : nat := foo trivial
#print bar  -- def bar : nat := foo trivial
def bar2 : nat := foo (id trivial)
#print bar2  -- def bar2 : nat := foo _

So I think it is just pretty printing.

---

As for proof erasure, I believe Lean erases proofs in the VM and compiled code, and yes I believe it provides a speed advantage, since one doesn't have to evaluate the proof. So when your run your function (or my bar example) with #eval, it first converts it to VM code without proof or type data.

However, this isn't directly related to what you are seeing. Lean does store the proofs for inspection by #print (and other reasons like external checking of .olean files). It just doesn't always show the proof apparently.