## Stream: general

### Topic: Writing proof terms to disk

#### John Tristan (Oct 25 2019 at 01:17):

Is there a command I could use to write a proof term to disk? Something like #print, but where I could specify a file where to write the term.

@Keeley Hoek?

#### Bryan Gin-ge Chen (Oct 25 2019 at 01:31):

I take it putting #print some_term at the end of some_file.lean and running lean some_file.lean > output_file from the command line won't do for some reason?

#### Bryan Gin-ge Chen (Oct 25 2019 at 01:34):

I have zero experience with programming in Lean, but I bet someone could rig something together following this function from leanpkg:

import system.io

def write_file (fn : string) (cnts : string) (mode := io.mode.write) : io unit := do
h ← io.mk_file_handle fn io.mode.write,
io.fs.write h cnts.to_char_buffer,
io.fs.close h


#### John Tristan (Oct 25 2019 at 01:35):

It does work actually, thanks for the idea. In general, I might need to write different proof terms to different files so I don't know if this trick will always do it.

#### John Tristan (Oct 25 2019 at 01:42):

Following up on this is there a way to control the amount of inlining? Let me clarify with an example.
Consider the following snippet:

/- start -/
open nat

def isEven(n : ℕ): Prop := ∃ k: ℕ, n = 2 * k

def double(n: ℕ): ℕ := 2 * n

lemma doubleIsEven: ∀ n: ℕ, isEven(double(n)) :=
begin
intros,
unfold double,
unfold isEven,
existsi n,
trivial,
end

def P := doubleIsEven(2:nat)

#print P
/- end -/

It prints:
def P : isEven (double 2) :=
doubleIsEven 2

But ideally, what I want is to print the term of doubleIsEven applied to 2 and beta reduced.
Is it something that I could do? Does it even make sense?

#### Bryan Gin-ge Chen (Oct 25 2019 at 01:46):

Maybe what you want is #reduce P?

#### John Tristan (Oct 25 2019 at 01:47):

I actually gave it a try and I end up with the message "Exists.intro 2 (eq.refl 4)"

#### Bryan Gin-ge Chen (Oct 25 2019 at 01:50):

Yeah, I'm not sure how to get it to display the result with notation...

#### Bryan Gin-ge Chen (Oct 25 2019 at 01:54):

If you put set_option pp.implicit true in the line before you get to see the implicit arguments to Exists.intro:

@Exists.intro ℕ (λ (k : ℕ), 4 = nat.mul 2 k) 2 (@eq.refl ℕ 4)


#### John Tristan (Oct 25 2019 at 02:03):

Interesting, thank you

#### Keeley Hoek (Oct 25 2019 at 02:24):

In community lean there are functions io.serialize and io.deserialize which write proof terms (actually, any expr) in lean's binary serial format to and from disk.

#### Keeley Hoek (Oct 25 2019 at 02:25):

That is, https://github.com/leanprover-community/lean lean 3.5.0c

#### Keeley Hoek (Oct 25 2019 at 02:26):

For big exprs you don't want to use anything else if you need to load them back in, because io buffer stuff in lean has abysmal performance

#### Keeley Hoek (Oct 25 2019 at 02:27):

But the original point of adding that was so big tactics like omega and (maybe vampire?, hopefully, eventually rewrite_search) could save their boring autogenerated proof of an easy fact, without having to recompute every time the library was compiled

Thanks a lot!

#### Keeley Hoek (Oct 25 2019 at 02:31):

No problem, no idea but just in case you're completely new to metaprogramming in lean you'll probably want to look at environment.get in core to obtain the expr underlying any declaration you ask for

#### John Tristan (Oct 25 2019 at 02:41):

I am indeed completely to metaprogramming in lean, and very new to lean itself, so thanks for the tip!

Last updated: May 16 2021 at 05:21 UTC