more automation for induction?

Stream: new members

[Nada Amin]

Hi,

I am interested in automating proofs by induction in Lean. Here is an example of a development with rather tedious proofs:
https://github.com/namin/LeanSketcher/blob/main/StlcInd.lean

In contrast, the Dafny equivalent is much more digestible and scales well when adding new constructs to the model.

I know a little about grind now, and <;>, but I still wouldn't know how to make the proofs in the file above more regular and automated.

Any thoughts? Tricks?

Eventually, I'd like to metaprogram a sketching facility in Lean for to streamline such proofs.

Thanks, ~n