Reading Inductive definition in Lean4

Stream: lean4

[Yasu Watanabe]

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]

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]

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]

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]

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]

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

[Yasu Watanabe]

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