hitchhikers guide, but with examples?

Stream: new members

[Anders Larsson]

I'm reading the "The Hitchhiker’s Guide to Logical Verification". It's awesome, but are there any somewhat bigger examples to look at? Are there any small projects or that uses Lean that one can look at.

(I found a coulple, one related to Soong and a masters work by Sebastian Ullrich).

EDIT: I was thinking about program verification examples.

[Johan Commelin]

@Anders Larsson Are you looking for examples in CS or in maths direction?

[Anders Larsson]

Johan Commelin said:

Anders Larsson Are you looking for examples in CS or in maths direction?

I was thinking about program verification examples.

[Arthur Paulino]

@Anders Larsson I have this small example where I defined a DataFrame and one of its fields is a constraint of consistency.
That rule of consistency requires a proof that every row has the same length and types as defined in the dataframe scheme.

See how clean (and waaaaay less prone to bugs) addRow has become in comparison with this approach. Notice the struggle to map the situations where I'd make Lean panic.

[Arthur Paulino]

And in this example I defined a musical scale shape as a sequence of intervals, with some constraints. Then I provided proofs that allowed me to invert scale shapes and guarantee the consistency of the resulting scale shapes. So I'm feeling pretty confident about that inversion operation :smiley:

[Anders Larsson]

Nice with small but meaningful examples.

[Arthur Paulino]

You can find even more examples in Lean 4's Std.Data source code:
https://github.com/leanprover/lean4/tree/master/src/Std/Data

[Anders Larsson]

Arthur Paulino said:

You can find even more examples in Lean 4's Std.Data source code:
https://github.com/leanprover/lean4/tree/master/src/Std/Data

That's interesting too. I'm not goining to confuse my brain with Lean4 the coming days, but hopefully in the future.