## Stream: general

### Topic: Proof storage in structures

#### Valéry Croizier (Jun 01 2021 at 20:11):

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 (Jun 01 2021 at 21:07):

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

#### Alex J. Best (Jun 01 2021 at 21:09):

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 := ◾}))


Last updated: Dec 20 2023 at 11:08 UTC