Required definitions

Stream: general

[Yaël Dillies]

@George Shakan and I just finished proving the Plünnecke-Ruzsa inequality in #15440 and we were wondering how to convince the world that we indeed proved Plünnecke-Ruzsa. One idea we came up with was to list the definitions that our statement depends on. Is it possible to write a small program that lists all definitions that a given lemma depends on? It's obviously going to be a lot of junk, but I can then curate the list.

[Johan Commelin]

Have you seen the approach we've been implementing in LTE?

[Johan Commelin]

We identify the objects occuring in the statement and write a ~100 line file that shows these objects behave as expected.
We take care to make those files polished and readable.

[Johan Commelin]

See https://github.com/leanprover-community/lean-liquid/tree/master/src/examples

[Yaël Dillies]

Yeah but #15440 is only 300 lines long :rofl:

[Johan Commelin]

I don't see why that changes anything about the strategy.

[Yaël Dillies]

It's possibly a bit too much effort, but mostly I do not even know what definitions I should do that for.

[Johan Commelin]

Only the ones that occur in the statement.

[Johan Commelin]

But the statement looked quite readable to me.

[Yaël Dillies]

Maybe I can just add a bunch of #eval to check explicit cases?

[Mauricio Collares]

A rough interpretation of Freiman's theorem is that the only "interesting" examples for small doubling are subsets of (generalized) arithmetic progressions. Perhaps taking B to be an arithmetic progression is already good enough for demonstration purposes? You can compute (m • B - n • B).card and (B + B).card to sanity-check the definitions.

[Antoine Chambert-Loir]

Yaël Dillies said:

George Shakan and I just finished proving the Plünnecke-Ruzsa inequality in #15440 and we were wondering how to convince the world that we indeed proved Plünnecke-Ruzsa. One idea we came up with was to list the definitions that our statement depends on. Is it possible to write a small program that lists all definitions that a given lemma depends on? It's obviously going to be a lot of junk, but I can then curate the list.

I would love seeing clean mathematical statements in the docstring, as well as references to the mathematical litterature where the results were first proved, and, if this is relevent, references to the proofs that you used..

[Riccardo Brasca]

https://github.com/leanprover-community/leancrawler/

Can surely produce the list you want