any example for lean4 parser

Stream: general

[kishou yusa]

Is there any example for lean4 parser? I read the document but example will be a better help

[Alex J. Best]

Can you be a bit more specific? Which part of the parser? What document did you already read, and what sort of example of input and output are you looking for. This is a very big topic

[kishou yusa]

I read the document from:https://leanprover-community.github.io/mathlib4_docs/Lean/Parser/Basic.html. I want to parse input which follow first order logic and transform and run duper on it.

[Arthur Paulino]

Others might think otherwise (with more paths than the ones I'm aware of), but my 2c is that this task is kinda hard because you have APIs that operate on different levels of abstraction.

If this duper you're talking about is a Lean tactic coded somewhere (maybe Mathlib?), it's an algorithm that runs at compile time when typechecking.

The only practical way I see for you to accomplish this task in this case is to write a Lean metaprogram that parses your input at compile time. By the way, IIRC, MetaM can perform IO operations like reading text from files. And from MetaM you'll have access to duper

The other approach is to manifest "duper" in the layer of abstraction of a regular Lean 4 program. Meaning, pretty much, implementing your own typechecker for the data you parse and then implementing duper for it

[Alexander Bentkamp]

Is your input in TPTP format (https://www.tptp.org/)? Duper includes a parser for TPTP. @Josh Clune would be able to tell you how to use it.

[Alexander Bentkamp]

Regarding the different levels of abstraction Arthur mentioned, I believe https://github.com/tydeu/lean4-partax solves this issue.

[Alexander Bentkamp]

BTW, duper is indeed a Lean tactic: https://github.com/leanprover-community/duper

[Josh Clune]

Alexander Bentkamp said:

Is your input in TPTP format (https://www.tptp.org/)? Duper includes a parser for TPTP. Josh Clune would be able to tell you how to use it.

Following up on this, if your input format is TPTP's first-order format (FOF), you can use either the tptp command (which takes an identifier and path and will attempt to transform an FOF file into a Lean goal) or the BEGIN_TPTP ... END_TPTP macro which will attempt to transform FOF syntax (written in the ...) into a Lean goal. Both are available if you have Duper as a dependency via import Duper.TPTP

import Duper
import Duper.TPTP

tptp test1 "path_to_fof_file"
  by duper [*]

BEGIN_TPTP test2
fof(h0, axiom, eats(A, cake)).
fof(h1, axiom, ~eats(B, cake)).
fof(goal, conjecture, A != B).
END_TPTP
  by duper [*]

[kishou yusa]

thanks for your help, do you think I can expanse on this and do a parser for CTL to prove CTL proposition on lean?

[Josh Clune]

Offhand, I don’t know enough about CTL to know whether it would be easier to try to directly build on the TPTP parser or just use it as inspiration for how a CTL parser might be built, but you’re welcome to do either.

[Alexander Bentkamp]

Either way, the TPTP parser is probably a good example to look at.
The syntax is declared here:
https://github.com/leanprover-community/duper/blob/main/Duper/TPTPParser/SyntaxDecl.lean
And the transformations of the new syntax into Lean terms is implemented here:
https://github.com/leanprover-community/duper/blob/main/Duper/TPTPParser/MacroDecl.lean

[Notification Bot]

Utensil Song has marked this topic as resolved.

[Notification Bot]

Utensil Song has marked this topic as unresolved.