Blog post: ProofData for organizing intermediate definitions

Stream: general

[pandaman]

Hi! I blogged about a pattern I used for organizing definitions and their properties so that I could reuse proofs about the intermediate data that appeared when verifying my lean-regex library. I hope this kind of articles will help software verification with ITPs more approachable.

The TLDR is to create type classes to hold the input to the regex compliation function so that we can state the intermediate steps using the type class fields and reason about them. I also found some annoyances when applying the technique, so any advice are welcome. Thanks!

Article link: https://zenn.dev/pandaman64/articles/lean-proof-data-en