Zulip Chat Archive

Stream: new members

Topic: printing lemma statements


view this post on Zulip Michael Beeson (Oct 16 2020 at 04:00):

I would like to have Lean print out the statements and names of all the lemmas and theorems I have proved.
How can I do that?

view this post on Zulip Kevin Lacker (Oct 16 2020 at 04:05):

I am also curious whether this is possible

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 04:06):

How exactly do you define "I have proved"?

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 04:07):

All lemmas in the current environment? All lemmas in the current file? Something else?

view this post on Zulip Kevin Lacker (Oct 16 2020 at 04:08):

or do you just want to know what they are, rather than having Lean itself do it, in which case you can do grep lemma your_code.lean :wink:

view this post on Zulip Michael Beeson (Oct 16 2020 at 04:30):

grep doesn't do it because some of the lemmas are on two or more lines. That only gives me the first line.
I mean all the lemmas in the current environment.

view this post on Zulip Michael Beeson (Oct 16 2020 at 04:31):

Today I proved duplicates of two lemmas I proved weeks ago, having forgotten that I already proved them. Yikes!

view this post on Zulip Michael Beeson (Oct 16 2020 at 04:33):

I have about 80 lemmas. Each one has a name in the Latex file, and a number that latex assigns it, and a name in the Lean file of the form "lemma43" that corresponds with the number in the pdf file that Latex makes. This is a clerical nightmare.

view this post on Zulip Michael Beeson (Oct 16 2020 at 04:34):

Since I refer to the pdf while formalizing the proof, that's why I made the Lean names correspond to the numbers in the pdf file.

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 04:37):

Note that the lemmas in the current environment include lots of lemmas from stdlib (and mathlib if you import it).

view this post on Zulip Yury G. Kudryashov (Oct 16 2020 at 04:37):

Do you want to have the list of lemmas from the current repository?

view this post on Zulip Alex J. Best (Oct 16 2020 at 04:39):

Heres a simple user command that prints name + statement of all decls in the file (not very well tested), this is in the file not the environment, you can remove the filter part if you want them all.

import tactic.basic
reserve notation `#file_decls`

-- examples
lemma bar (n : ) (h1 : 0 < n) : 0 < n := sorry
lemma baz (n : ) : 0 < n + 1 := sorry

open tactic
setup_tactic_parser
meta def file_decls : tactic (list (name × expr)) := do
  e  get_env,
  let l := e.filter (λ d, e.in_current_file d.to_name),
  return (l.map (λ d, d.to_name, d.type⟩))
@[user_command] meta def file_cmd (_ : parse $ tk "#file_decls") : lean.parser unit :=
trace file_decls.

#file_decls

view this post on Zulip Kevin Lacker (Oct 16 2020 at 04:46):

you can also use awk to do something like grep but across multiple lines: awk '/lemma/,/:=/' yourfile.lean

view this post on Zulip Michael Beeson (Oct 16 2020 at 05:58):

Kevin, that awk command prints out a zillion lines within the proofs where I have given an exact proof using :=
so it doesn't serve the desired purpose. Probably I can make it fancier and get only lines that begin with 'lemma' and subsequent lines up to := .Nice idea.

view this post on Zulip Michael Beeson (Oct 16 2020 at 05:59):

Has anyone thought about how one might fold up the tiniest inferences, leaving only the "important" lines,
and then scrape them off in a form that could be pasted into LaTeX?

view this post on Zulip Johan Commelin (Oct 16 2020 at 06:37):

@Michael Beeson if you speak Python, you might want to look at lean-formatter


Last updated: May 17 2021 at 21:12 UTC