parsing theorems from lean4 files

Stream: lean4

[John Mercer]

Related note, it would be very helpful for anyone doing code analysis to enforce -- theorem_end and --lemma_end like comment tags at the end of theorems and lemmas respectively to facilitate parsing lean4 files. This was the most appropriate thread I could find to add this comment, so please redirect if there is better place.

[Scott Morrison]

I don't think it's a good idea to try to parse lean4 files with anything other than lean4... We're never going to expect people to write comments like this.

[Yury G. Kudryashov]

Moreover, we can use macroses to generate similar theorems.

[Yury G. Kudryashov]

And we have attributes that generate theorems and definitions.

[John Mercer]

Scott Morrison said:

I don't think it's a good idea to try to parse lean4 files with anything other than lean4... We're never going to expect people to write comments like this.

Hi Scott, can you please elaborate? Is there some functionality in lean4 I'm not seeing to, e.g., list all theorems and lemmas?
[theorem name], [conjecture], [proof body (i.e. everything after :=)]

[Yaël Dillies]

Have a look at docs4#Lean.Environment and around.

[Henrik Böving]

John Mercer said:

Scott Morrison said:

I don't think it's a good idea to try to parse lean4 files with anything other than lean4... We're never going to expect people to write comments like this.

Hi Scott, can you please elaborate? Is there some functionality in lean4 I'm not seeing to, e.g., list all theorems and lemmas?
[theorem name], [conjecture], [proof body (i.e. everything after :=)]

Lean can be infinitely customized via meta programming, you can introduce arbitrary syntax with arbitrary meaning (including auto generating theorems) so processing lean with something that is not a fully fledged lean compiler is bound to fail.

[Notification Bot]

7 messages were moved here from #lean4 > rfc: theorem names by Eric Wieser.

[Jireh Loreaux]

John, a classic example of where you would find theorems that are auto-generated and don't show up explicitly in the source (which is why you need to parse Lean with Lean), would be any theorem in mathlib marked with the to_additive or simps attributes. Now, maybe you don't want to include these theorems, but for instance, there is no explicit code which gives the foundational result: "the quotient of a Banach space by a subspace is complete" (note: unless the subspace is closed the quotient is only seminormed) because here we are taking an additive group quotient, for which docs4#QuotientAddGroup.completeSpace applies, but this declaration is autogenerated from docs4#QuotientGroup.completeSpace using to_additive (see source).

[Yury G. Kudryashov]

See also Data.UInt

[Max Nowak 🐉]

It’s not too difficult to list all theorems in a given file from a lean metaprogram. You can get the Environment object, and then iterate through all constants filtering them to only theorems, done.

[Max Nowak 🐉]

Filtering for only a specific import file is only a little bit more involved, I did that for one of my projects. If you can’t figure it out yourself I can go dig that code up.

[John Mercer]

Thanks everyone for the great feedback and help! Will do another iteration of investigation and testing (based on info above) and will get back to you.