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

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?)

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

Right, yes, I see.

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

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

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.

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

I will rephrase it.

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)

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

Let me find this...

@Karl Palmskog is this clearer?

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)

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?)

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.

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.

@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?

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)

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

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?

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

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.

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

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

What is naive_solver?

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

Last updated: Jun 23 2024 at 03:02 UTC