Proof storage in structures

Stream: general

[Valéry Croizier]

To maintain their invariant, some structures contain proofs in addition to "real" data. I wonder, does Lean store the actual proof at runtime? For a small structure like a rational number, the overhead must be huge.

[Scott Morrison]

No, everything in Prop is erased. That's more or less why Prop exists separately.

[Alex J. Best]

Lean doesn't store the proofs at runtime, they are used to typecheck the user's functions, but they are erased by the compiler by a step called erase_irrelevant, here is a small example of a type, which is a nat and a proof that it is small:

import tactic
set_option trace.compiler true --so we can see what the compiler does
structure smallnat :=
(n : ℕ)
(h : n < 10)

def sub : smallnat  → smallnat → smallnat := λ ⟨n1, h1⟩ ⟨n2, h2⟩, ⟨n1 - n2, by omega⟩
def sub' : nat  → nat → nat := λ n1 n2, n1 - n

First thing to note is that the generated bytecode (the last part of the output) is very similar for both functions e.g. for the smallnat version:

[compiler.optimize_bytecode]  sub 2
0: move 0
1: move 1
2: ginvoke nat.has_sub
3: apply
4: apply
5: ret

there are no proofs being referred to in this bytecode, in fact lean has optimized by realising our structure is basically just a nat, and gotten rid of the structure completely, but that happens after the proofs are erased. The version just for nats is almost the same:

[compiler.optimize_bytecode]  sub' 2
0: move 0
1: move 1
2: cfun nat.sub
3: ret

we can see the step where the proofs are stripped away here:

[compiler.elim_recursors]
>> sub
λ (_x ᾰ : smallnat),
  _x.cases_on
    (λ (n : ℕ) (h : n < [nat_value_macro]) (_x : smallnat),
       _x.cases_on (λ (n_1 : ℕ) (h_1 : n_1 < [nat_value_macro]), {n := n - n_1, h := _}))
    ᾰ
[compiler.erase_irrelevant]
>> sub
λ (_x ᾰ : smallnat),
  smallnat.cases_on _x
    (λ (n : ℕ) (h : ◾),
       smallnat.cases_on ᾰ (λ (n_1 : ℕ) (h : ◾), {n := has_sub.sub ◾ nat.has_sub n n_1, h := ◾}))