I am relying on mathcomp + SSReflect for a project and I am wondering if anybody has found any offtheshelf 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 wellformed anymore if you try to change P b to a Boolean.
if you want to do heavily automated reasoning (e.g., do everything modulo SMT / firstorder 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 domainspecific 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.
Maybe also trakt can help
I'd count Trakt as more of a "metaautomation" tool, i.e., people who want to develop domainspecific SSR/MathComp automation might want to build on Trakt. Using it directly for proofwriting productivity is probably above complexity threshold for regular proof engineers.
(but happy to be "proved" wrong about that)
Lemma overloading also works nicely as a form of automation in SSReflect.
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 higherlevel graphical language ala Haskell's arrows might be useful here.
@Karl Palmskog It it is a good point.
Mathcomp 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 mathcomp library.
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?
@Assia Mahboubi is probably the most informed here. See e.g. https://arxiv.org/abs/2204.02643
@Alexander Gryzlov Thanks. We have somewhat similar automation (with type classes) in mathclasses.
The project seems somewhat old. I'd imagine there are more modern references for mathcomp. Perhaps by @Enrico Tassi ?
@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/imdeasoftware/htt/blob/master/htt/heapauto.v#L376
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
isn't the automation hierarchy something like:
unification hints

canonical structures
/ \
lemma overloading structure inference w/ packed classes
Is there experience with itauto and mathcomp?
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/testsuite/refl_bool.v)
Last updated: Jul 23 2024 at 20:01 UTC