printing lemma statements

Stream: new members

[Michael Beeson]

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?

[Kevin Lacker]

I am also curious whether this is possible

[Yury G. Kudryashov]

How exactly do you define "I have proved"?

[Yury G. Kudryashov]

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

[Kevin Lacker]

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:

[Michael Beeson]

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.

[Michael Beeson]

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

[Michael Beeson]

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.

[Michael Beeson]

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.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Alex J. Best]

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

[Kevin Lacker]

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

[Michael Beeson]

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.

[Michael Beeson]

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?

[Johan Commelin]

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