Zulip Chat Archive

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:

>> sub
λ (_x  : smallnat),
    (λ (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 := _}))
>> 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