Zulip Chat Archive

Stream: lean4

Topic: Reading Inductive definition in Lean4


Yasu Watanabe (Mar 19 2022 at 01:07):

I've been reading Theorem Proving in Lean4 for several weeks, I feel I can generate Java and Python's data structures of my work from Lean4 Inductive type. I know there exists such tool but I I use Lean4, it would be finally possible to define, detect or prove some kind of consistency of data definition. To try this,
any clue or hints to reading Inductive type from Lean4 are appreciated.

Chris B (Mar 19 2022 at 07:31):

Can you elaborate a little bit on what exactly you'd like to accomplish? It sounds like you have an inductive type in Lean 4, and you want to export it to another language (java/python). When you say consistency, is the goal to prove that the extraction/translation is faithful?

Yasu Watanabe (Mar 19 2022 at 08:26):

Chris B said:

Can you elaborate a little bit on what exactly you'd like to accomplish? It sounds like you have an inductive type in Lean 4, and you want to export it to another language (java/python). When you say consistency, is the goal to prove that the extraction/translation is faithful?

I just imagine some possiblity of Lean4 usage and I do not consider very deeply. But I explain what I thought.

I have custom tool that can generate Java nad python data type, whose data format is proto
https://github.com/protocolbuffers/protobuf.
Currently, it just generate data type.
If we define the data type in Lean4, I thought I could specify the restriction or relation between data.

What I hope to try finally is a mixture of functional domain modeling
https://fsharpforfunandprofit.com/ddd/, proof and code generation.

As compared to F#, Lean4 or dependent type can describe more detailed specificationof data or domain.
I think it is possible to prove some propert of domain model, that makes domain model more robust.

If we prove some properties about domain model, the generated data type can be more robust than just using proto.

This is a long story but I'd like to try to implement to generating ex Java class from Lean4 data type.

Mario Carneiro (Mar 19 2022 at 08:46):

You can do lean code generation just the same as java / python code generation. But if you want the lean type to be richer with invariants and so on then this will have to be represented in the input somehow, and I don't think protobuf has anything in particular for this

Chris B (Mar 19 2022 at 08:56):

You can add the proofy stuff to the Lean code post-hoc if you're sure the types you're reasoning about are accurate representations of the ones used in the language you're targeting.

Chris B (Mar 19 2022 at 09:09):

Looking at some of the derive handlers might be helpful if generating source code from Lean declarations is a goal.

Yasu Watanabe (Mar 19 2022 at 11:29):

Mario Carneiro Chris B
Thank you for the information. I'll investigate deriving feature.


Last updated: Dec 20 2023 at 11:08 UTC