## Stream: Coq users

### Topic: Best practices for automation in mathematical proofs

#### Notification Bot (Jun 24 2023 at 20:24):

This topic was moved to #math-comp users > Best practices for automation in mathematical proofs by Karl Palmskog.

#### Patrick Nicodemus (Jun 24 2023 at 20:26):

I am interested in discussing best practice for automating mathematical proofs. As a concrete example, let us take the pigeonhole principle for maps f: { x : nat | x < n } -> { y : nat | x < m }, where we conclude that if m < n then there are x, y < n with x < y and f(x)=f(y). What would a "model proof" of this theorem look like? It has to deal with the difference between naturals and elements of the subset type {x : nat | x < n}, perhaps conversion between functions and function graphs represented as lists (so that we can use functional extensionality), possibly manipulating negation / contrapositives (f is not injective -> there are x, y with x < y and f(x) = f(y)). I have written some pages of code about ordinal arithmetic in this vein and I am very unhappy with how verbose it is, but I don't know how to proceed. I will try to post my work on github soon and request constructive feedback from the community.

I am not sure if boolean reflection style or vanilla coq are best for this. There are tradeoffs which have to be addressed. One could use
My experience has been that boolean reflection invites a proliferation of different forms for theorems, for example if b is boolean and I want to assert the negation of b, I could write `b=ff`, `b!=tt`, `(negb b) = tt`, `match b with tt => False | ff => True`, etc. This creates an explosion of the search space for automation because it has to navigate between the many forms that a proposition can take on; perhaps this happens with any approach though.
Also with booleans one can no longer easily define automation tools by induction on the syntactic form of the proposition to be proved. I don't know if that's a real problem.
Preference for SSReflect vs vanilla Coq is subjective but still a discussion worth having.
If it's possible to write better and cleaner automation in vanilla Coq without small scale reflection that improves user's quality of life then that might be better as a toy example, but probably we then have to have a discussion about how to manage complexity arising from sophisticated uses of dependent types and equality (to what extent is it a problem? are there other solutions than using SSR?)

#### Karl Palmskog (Jun 24 2023 at 20:27):

the problem is the following: if you state a problem in terms of `'I_n` and the like, most Coq users have no idea what this is about

#### Patrick Nicodemus (Jun 24 2023 at 20:28):

Right, yes, I see.

#### Karl Palmskog (Jun 24 2023 at 20:29):

the "other" solution for doing booleans is to remove them as much as possible and use a typeclass like Std++ `Decision`

#### Patrick Nicodemus (Jun 24 2023 at 20:29):

I don't have a commitment to math-comp representations of data. Whatever representation allows principles of good automation to be demonstrated clearly.

Karl Palmskog said:

the problem is the following: if you state a problem in terms of `'I_n` and the like, most Coq users have no idea what this is about

#### Patrick Nicodemus (Jun 24 2023 at 20:30):

You can use SProp to manage dependent type headaches but dealing with both Prop and SProp is the same issues as dealing with both Prop and bool.

#### Karl Palmskog (Jun 24 2023 at 20:30):

OK, then, if you can rephrase your code example(s) in terms of Stdlib, this would be a better fit for this stream

#### Patrick Nicodemus (Jun 24 2023 at 20:30):

I will rephrase it.

#### Paolo Giarrusso (Jun 24 2023 at 20:32):

A form of pigeonhole appears in software foundations as a (4-star) exercise, and it's been years, but I can't remember it looking like a matter for automation... It seemed just a surprisingly hard proof (OTOH, I was a Coq newbie)

#### Paolo Giarrusso (Jun 24 2023 at 20:33):

SProp remains experimental, and I'm not sure how necessary it is here

#### Paolo Giarrusso (Jun 24 2023 at 20:34):

Let me find this...

#### Patrick Nicodemus (Jun 24 2023 at 20:34):

@Karl Palmskog is this clearer?

#### Karl Palmskog (Jun 24 2023 at 20:36):

that's pretty good. May be helpful to also highlight Coq code (three backticks followed by `coq`, then newline, then code, then three backticks on newline)

#### Paolo Giarrusso (Jun 24 2023 at 20:48):

proliferation of different forms for theorems

yes, but that's a (nontrivial!) API design problem — pick a canonical form, use it in all statements, and when other forms arise add conversion lemmas.
If you're dealing with a set of rewrite rules (as is so common in math-comp/stdpp), there's a general technique that _can_ "canonicalize" the statements — https://en.wikipedia.org/wiki/Knuth–Bendix_completion_algorithm; but "use the canonical form in statements" covers many cases.

Also with booleans one can no longer easily define automation tools by induction on the syntactic form of the proposition to be proved.

When needed, one can define equivalent propositions, and relate them to the booleans with `reflect` — ssreflect has an extensive theory.

FWIW, I found https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#pigeonhole_principle, but that one is a significantly different version (and probably proof?)

#### Karl Palmskog (Jun 25 2023 at 20:30):

whenever the debate about booleans comes up, I usually link to this piece, which I think summarizes the "theory B" computer science view of booleans and their role in math and proving: https://existentialtype.wordpress.com/2011/03/15/boolean-blindness/

In Coq, the `Decision`typeclass in Std++ is how one can have have "bits with provenance". `reflect` lemmas are another largely orthogonal approach, which can facilitate easier computation inside proofs, if one cares about this.

#### Karl Palmskog (Jun 25 2023 at 20:33):

since I don't really care so much about whether proof scripts are mathematician readable, I usually prefer the style of working modulo a first-order solver, like METIS in the HOLs, and CoqHammer's sauto.

#### Patrick Nicodemus (Jun 26 2023 at 01:19):

@Karl Palmskog Yes, as far as I am concerned, I would be fine working modulo a first order solver, bring on the automation.
Regarding the booleans I understand the problem on an intuitive level but I am not fully convinced that it is a problem, would it be practical to automate reasoning with boolean-coded propositions as long as we had the theorems that justified this kind of reasoning? Like if I have to prove a goal of the form `a && b` where `&&` is Boolean conjunction I can write an Ltac script which looks for Boolean conjunction and splits accordingly. To what extent would this be practical?

#### Karl Palmskog (Jun 26 2023 at 08:33):

with the Std++ `Decision` approach, the idea is to (almost) never have any boolean operations in goals and proof context. For example, the `filter` function on lists doesn't take a boolean function with Std++. If you want to use boolean operations for domain reasons, I'd go with MathComp/`reflect` any day (but doesn't work well out-of-the-box with a FOL solver)

#### Paolo Giarrusso (Jun 26 2023 at 10:15):

do you have examples combining sauto with either stdpp or math-comp? I imagine it takes some setup, and I've never seen them do enough to be worth the trouble

#### Paolo Giarrusso (Jun 26 2023 at 10:17):

but doesn't work well out-of-the-box with a FOL solver

what's your experience with `From Hammer Require Import Reflect.` for that?

#### Karl Palmskog (Jun 26 2023 at 10:33):

last I looked at CoqHammer's support for reflection it didn't work beyond some trivial examples

#### Karl Palmskog (Jun 26 2023 at 10:34):

we did some experiments replacing all our uses of `firstorder` with `sauto` in a quite large project heavily using Std++. It went fairly well, but we didn't integrate it [the experimental `sauto` branch] yet.

#### Karl Palmskog (Jun 26 2023 at 10:36):

I'll try to summarize that stuff [trying various kinds of automation like Itauto, sauto in a typeclass-heavy Std++-based project] in an upcoming Coq Workshop presentation, slides will be public

#### Paolo Giarrusso (Jun 26 2023 at 10:46):

In principle, sauto should be able to replace naive_solver as well, but it seemed quite a bit slower

#### Patrick Nicodemus (Jun 27 2023 at 02:55):

What is naive_solver?

#### Karl Palmskog (Jun 27 2023 at 06:09):

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/tactics.v#L729

Last updated: Jun 23 2024 at 03:02 UTC