## Stream: new members

### Topic: hitchhikers guide, but with examples?

#### Anders Larsson (Jan 12 2022 at 12:33):

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 (Jan 12 2022 at 12:39):

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

#### Anders Larsson (Jan 12 2022 at 12:53):

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 (Jan 12 2022 at 13:54):

@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 (Jan 12 2022 at 14:02):

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 (Jan 12 2022 at 15:13):

Nice with small but meaningful examples.

#### Arthur Paulino (Jan 12 2022 at 15:44):

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 (Jan 13 2022 at 08:16):

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.

Last updated: Dec 20 2023 at 11:08 UTC