Zulip Chat Archive

Adam and I just brainstormed about how to compile evidence that we actually verified what we claimed we did. I first suggested to split all the definitions that are relevant for the statement into a separate directory structure. But that quickly becomes messy. Then Adam suggested to have a directory examples/ where we prove that certain gadgets are equal to what you expect them to be, by rfl. I really like this idea.

Adam is currently preparing examples/pBanach.lean. The nice benefit is that we can also easily show that mathlib got things right, e.g. by having examples/real.lean that shows (thanks @Alex J. Best and @Yaël Dillies) that the reals form a conditionally complete linearly ordered field.
Similarly, we can have examples/measures.lean and examples/Ext.lean.

Filippo A. E. Nuccio (Jul 18 2022 at 15:24):

Very nice! But what kind of "examples" would you like for p-Banach, for instance? The proof of a "known" theorem in that theory that we can formalize using the current definition?

Adam Topaz (Jul 18 2022 at 15:26):

Here is a start on the examples file for p-Banach:
https://github.com/leanprover-community/lean-liquid/pull/95

Filippo A. E. Nuccio (Jul 18 2022 at 15:27):

Ah, I see.

Filippo A. E. Nuccio (Jul 18 2022 at 15:27):

Sure, it makes sense.

Johan Commelin (Jul 18 2022 at 18:26):

I left some comments

Adam Topaz (Jul 18 2022 at 19:02):

Johan Commelin said:

I left some comments

Which are now accounted for!

Johan Commelin (Jul 18 2022 at 19:18):

Thanks!

Johan Commelin (Jul 18 2022 at 19:18):

Minor nitpick about formatting: in expressions like ∥ v + w ∥ ≤ ∥ v ∥ + ∥ w ∥ I tend to find that there are too many spaces. What do you think of ∥v + w∥ ≤ ∥v∥ + ∥w∥?