Stream: Coq users

Topic: Best practices for automation in mathematical proofs


view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jun 24 2023 at 20:28):

Right, yes, I see.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jun 24 2023 at 20:30):

I will rephrase it.

view this post on Zulip 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)

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 20:33):

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

view this post on Zulip Paolo Giarrusso (Jun 24 2023 at 20:34):

Let me find this...

view this post on Zulip Patrick Nicodemus (Jun 24 2023 at 20:34):

@Karl Palmskog is this clearer?

view this post on Zulip 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)

view this post on Zulip 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?)

view this post on Zulip 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 Decisiontypeclass 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (Jun 27 2023 at 02:55):

What is naive_solver?

view this post on Zulip 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