Stream: math-comp users

Topic: Automation tools


view this post on Zulip Patrick Nicodemus (Jan 12 2023 at 02:43):

I am relying on math-comp + SSReflect for a project and I am wondering if anybody has found any off-the-shelf automation tools that are at least modestly helpful when proving theorems.

There is a flood of research on machine learning and automation but I think that the logical structure of an SSReflect proof is different than a vanilla coq proof. Perhaps with a sufficiently abstract neural network operating only on tokens without any understanding of the proof structure this would not matter.

The creator of Coqhammer had a great idea by packaging some basic boolean reflection tactics into Coqhammer. However if you have data structures that have boolean valued fields you cannot just reduce the boolean with a prop because the data structure depends on it being a prop. For example if A is a subtype of B, say A = { b | P b } and you have a function f : A -> C and t : A, and you want to prove something about f(t). The term is not well-formed anymore if you try to change P b to a Boolean.

view this post on Zulip Karl Palmskog (Jan 12 2023 at 09:30):

if you want to do heavily automated reasoning (e.g., do everything modulo SMT / first-order logic), it's not really obvious why you would want to use SSReflect, which is best used for controlled, targeted reasoning in smaller increments. I think MathComp/SSR is best complemented by domain-specific automation, like mczify, Algebra Tactics, Hierarchy Builder. I'm sure deep learning could be helpful when doing SSR proofs, but maybe more for guidance than for writing complete scripts.

view this post on Zulip Enrico Tassi (Jan 12 2023 at 11:30):

Maybe also trakt can help

view this post on Zulip Karl Palmskog (Jan 12 2023 at 11:34):

I'd count Trakt as more of a "meta-automation" tool, i.e., people who want to develop domain-specific SSR/MathComp automation might want to build on Trakt. Using it directly for proof-writing productivity is probably above complexity threshold for regular proof engineers.

view this post on Zulip Karl Palmskog (Jan 12 2023 at 11:35):

(but happy to be "proved" wrong about that)

view this post on Zulip Alexander Gryzlov (Jan 12 2023 at 14:17):

Lemma overloading also works nicely as a form of automation in SSReflect.

view this post on Zulip Alexander Gryzlov (Jan 12 2023 at 14:20):

Though I must say writing the corresponding structures manually is not very straightforward, primarily due to the fact that there's no way of enforcing the directionality of information flow, i.e. "inputs" and "outputs" for the inference. Some form of higher-level graphical language a-la Haskell's arrows might be useful here.

view this post on Zulip Patrick Nicodemus (Jan 12 2023 at 15:12):

@Karl Palmskog It it is a good point.

Math-comp is a large library and it is central to the Coq ecosystem. Because of this I want to use it as a point of departure for some of my own projects, perhaps others will as well. Regardless of whether ssreflect and first order SMT ATPs complement each other well, you have to work heavily with Boolean reflection if you want to use the math-comp library.

view this post on Zulip Patrick Nicodemus (Jan 13 2023 at 03:10):

A bit tangential but I realized I don't have a good sense of what kinds of theorems can be proven by ATP's. I asked Coqhammer to prove
forall x : nat * nat, exists y : nat * nat, fst x = snd y /\ snd x = fst y and it failed. Should I stick to like, quantifier free FOL?
Can somebody describe roughly the kinds of theorems Coqhammer has a good shot of proving?

view this post on Zulip Bas Spitters (Jan 13 2023 at 08:04):

@Assia Mahboubi is probably the most informed here. See e.g. https://arxiv.org/abs/2204.02643

view this post on Zulip Bas Spitters (Jan 13 2023 at 08:10):

@Alexander Gryzlov Thanks. We have somewhat similar automation (with type classes) in math-classes.
The project seems somewhat old. I'd imagine there are more modern references for math-comp. Perhaps by @Enrico Tassi ?

view this post on Zulip Alexander Gryzlov (Jan 13 2023 at 12:14):

@Bas Spitters I think the latest academic reference is Ziliani's thesis, in practice I've recently used this idea to automate some heap lemmas in HTT: https://github.com/imdea-software/htt/blob/master/htt/heapauto.v#L376

view this post on Zulip Kazuhiko Sakaguchi (Jan 13 2023 at 12:30):

In my ITP'22 paper (about Algebra Tactics), I demonstrated how to use the approach of Lemma overloading (but without backtracking, which might not be very interesting) for implementing a goal preprocessor like zify. See Section 5.2. https://doi.org/10.4230/LIPIcs.ITP.2022.29

view this post on Zulip Karl Palmskog (Jan 13 2023 at 12:52):

isn't the automation hierarchy something like:

unification hints
|
canonical structures
/                  \
lemma overloading    structure inference w/ packed classes

view this post on Zulip Bas Spitters (Jan 13 2023 at 16:04):

Is there experience with itauto and math-comp?

view this post on Zulip Karl Palmskog (Jan 13 2023 at 16:13):

there is some limited support for boolean reflection in itauto, but not as yet applied to MathComp (https://gitlab.inria.fr/fbesson/itauto/-/blob/master/test-suite/refl_bool.v)


Last updated: Jul 23 2024 at 20:01 UTC