Writing proof terms to disk

Stream: general

[John Tristan]

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.

[Scott Morrison]

@Keeley Hoek?

[Bryan Gin-ge Chen]

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]

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]

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]

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]

Maybe what you want is #reduce P?

[John Tristan]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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]

Interesting, thank you

[Keeley Hoek]

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]

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

[Keeley Hoek]

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]

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

[John Tristan]

Thanks a lot!

[Keeley Hoek]

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]

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