Zulip Chat Archive

Stream: general

Topic: Writing proof terms to disk


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 25 2019 at 01:21):

@Keeley Hoek?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Oct 25 2019 at 01:46):

Maybe what you want is #reduce P?

view this post on Zulip 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)"

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip John Tristan (Oct 25 2019 at 02:03):

Interesting, thank you

view this post on Zulip 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.

view this post on Zulip Keeley Hoek (Oct 25 2019 at 02:25):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip John Tristan (Oct 25 2019 at 02:29):

Thanks a lot!

view this post on Zulip 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

view this post on Zulip 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