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.
Scott Morrison (Oct 25 2019 at 01:21):
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
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 -/
def isEven(n : ℕ): Prop := ∃ k: ℕ, n = 2 * k
def double(n: ℕ): ℕ := 2 * n
lemma doubleIsEven: ∀ n: ℕ, isEven(double(n)) :=
def P := doubleIsEven(2:nat)
/- end -/
def P : isEven (double 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
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 ℕ (λ (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.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):
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
John Tristan (Oct 25 2019 at 02:29):
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