Has anyone used hammers successfully with math-comp? I couldn't find this quickly.
https://coqhammer.github.io/
https://coq-tactician.github.io/
or perhaps smtcoq?
@Karl Palmskog suggest that mczify is useful here:
https://coq.discourse.group/t/machine-learning-and-hammers-for-coq/303/21
Has there been any further progress?
@Bas Spitters with MathComp, I would nowadays probably recommend using a leaner solution for automation like Itauto. See discussion between Frédéric and Assia here for what might be missing: https://gitlab.inria.fr/fbesson/itauto/-/issues/28
as you may have seen, we plan to add itauto to the Fall 2022 release of the Platform: https://github.com/coq/platform/issues/265
there are some very interesting synergies between: itauto, mczify, algebra-tactics, Trakt, general MathComp stuff. But probably needs tuning by experts to be usable by ordinary MathComp users.
Thanks. This https://coqhammer.github.io/#boolean-reflection suggests that there has been some progress.
There is also a stale branch https://github.com/lukaszcz/coqhammer/tree/mathcomp
you can do boolean reflection also in itauto: https://gitlab.inria.fr/fbesson/itauto/-/blob/master/test-suite/refl_bool.v
Quick question about itauto. I see it is implemented in ml. Is it trusted or proof producing?
I was experimenting with porting this insertion sort tutorial from coqhammer to itauto as an example, but didn't make it go through yet.
I see [itauto] is implemented in ml. Is it trusted or proof producing?
it's not trusted, it's essentially an efficient SAT solver implemented in Gallina with some ML on top to get reflection
one might think of CoqHammer's sauto as Coq's Vampire-like FOL solver, while itauto is an Z3-like SAT/SMT solver. FOL solvers and SAT/SMT have different strengths. I think sauto is good for a workflow where you buy 100% into FOL automation, like METIS in Isabelle and HOL4. itauto is a more unintrusive addition when you want to keep proofs mostly manual.
in contrast to intuition
, which claims to be a propositional solver but actually does first-order stuff, itauto
is more disciplined: https://gitlab.inria.fr/fbesson/itauto/-/issues/25
in my view, firstorder
and intuition
are basically obsoleted by sauto
and itauto
at this point. Unless you're using Stdpp, regular intuition.
is actually dangerous, since it expands to intuition auto with *.
. This is a long-standing problem that can't easily be fixed without breaking a large part of Coq's CI.
We might use a script that tries to replace calls to intuition with something simpler.
It would be good if a linter/IDE started to make such suggestions
in an industry project, we recently replaced intuition
with itauto
, but we were already using Stdpp, so I expect more trouble for ordinary projects: https://github.com/runtimeverification/vlsm/commit/981386edcc7dd92fecbe42c1956c662e9b47fec8
we have this boilerplate on top of every file Local Tactic Notation "itauto" := itauto auto.
, but this has been added into itauto itself for 8.16, so itauto.
can be used directly in place of intuition.
for 8.16 and later.
Would any of these tactics work for mc finite sets?
how I would get automation for MC finsets is probably to create an analogue for the set_solver
tactic from Stdpp, then run itauto mc_set_solver
or directly write mc_set_solver
to use itauto
in several calls with the right leaf tactics
For reference:
https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.sets.html
right, I guess one should even check how itauto (and sauto) might synergize with Stdpp.
Since firstorder already fails or loops on very small goals generated by set_solver, we use the naive_solver tactic as a substitute.
@Paolo Giarrusso will know ;-)
I've not gotten a lot of looping with itauto, just failures. But it likely solves much less than firstorder (without the right leaf tactics)
set_solver
definitely needs _some_ first-order reasoning — so wiring it with sauto
might make sense
I tried it super-briefly and at least the basics do work out
wouldn't it make sense to parameterize set_solver
on the general solver? (And then have the regular set_solver
invocation set it to naive_solver
or whatever). Asking for a friend who might do benchmarking at some point.
@Paolo Giarrusso great. If you have something more definitive, please let us know.
@Karl Palmskog it'd make sense and I expect Robbert would agree
@Bas Spitters I haven't pursued that further because I didn't see immediate advantages from sauto
— I didn't do this:
I think sauto is good for a workflow where you buy 100% into FOL automation, like METIS in Isabelle and HOL4.
and sauto
isn't useful if you only ever call set_solver
on small MC-style lemmas (like done in stdpp)
@Paolo Giarrusso I think sauto
can be useful in the small as well, as shown in the tutorial I talked about above. But if you have a quite large project and want to use sauto
to its fullest, I think almost every proof engineer will have to learn a bunch of sauto
options and quirks, like how unfolding works.
in contrast, itauto
can likely be used without anyone changing much of their practices, just some small syntax adaptations.
the challenge with itauto
might instead be how to combine it with "just enough" FOL reasoning at the leaves. But already, the combination of lia
and congruence
at the leaves (smt
tactic) is impressive, and the whole thing is modular so a bunch of SMT theories could be added like so: https://gitlab.inria.fr/fbesson/itauto/-/blob/master/theories/NOlia.v#L30
I have basically no sauto
experience; I only mean that, given how I use set_solver
, naive_solver
is never the bottleneck. I could almost replace naive_solver
by timeout 0.2 naive_solver
.
mostly because if naive_solver
takes longer, it almost never succeeds. How long do you let sauto
run before interrupting it? I suspect I'd have to be more patient with it
I think the general rule of thumb is to never run it more than a few seconds. But the only FOL solver I've used seriously is METIS in HOL4. And there, it's unusual to require more than 5-10 seconds for a goal - longer than that is very likely to be divergence.
Karl Palmskog said:
I was experimenting with porting this insertion sort tutorial from coqhammer to itauto as an example, but didn't make it go through yet.
I'd like to point out the existence of a small library of sorting algorithms formalised with sauto: https://github.com/lukaszcz/sortalgs. In particular, the insertion sort formalisation from the library (https://github.com/lukaszcz/sortalgs/blob/master/isort.v) seems simpler than what the quoted link describes as "simple".
thanks, I'll try that one too, but one interesting challenge with the linked sort.v
was the switch between Prop
predicate and bool
(although I guess sorted.v
in sortalgs has something similar)
I don't think anyone is actively working on this now. By adding appropriate rewrite hints to the brefl
database (mentioned in https://coqhammer.github.io/#boolean-reflection) one could probably go pretty far in improving sauto support for mathcomp. But I'm not a mathcomp user, so I can't say and don't have time to figure out what these hints should exactly be.
yeah, I think we need some good MathComp challenge problems/files to get an apples-to-apples comparison of sauto and others. These days, I think one could even do automation-specific preprocessing via Trakt
Turns out the proof of sort_perm
was a bit more convoluted than it needed to be and CoqHammer (through the hammer
tactic) was able to produce the intermediate sorted list before applying transitivity of permutations. I updated the gist https://gist.github.com/siraben/3fedfc2c5a242136a9bc6725064e9b7d
Karl Palmskog said:
in my view,
firstorder
andintuition
are basically obsoleted bysauto
anditauto
at this point. Unless you're using Stdpp, regularintuition.
is actually dangerous, since it expands tointuition auto with *.
. This is a long-standing problem that can't easily be fixed without breaking a large part of Coq's CI.
What about adding a note to the reference manual recommending these replacements?
@Théo Zimmermann if you think a PR for this would be welcome, I can make one (probably next week). However, we will have to ping in those who actually know the implementation of firstorder
and/or intuition
(e.g., PMP) to make sure it's technically accurate and a fair assessment of the situation.
here is a version of Ben's sort.v
with Stdpp and itauto: https://gist.github.com/palmskog/e9514b34306e8882542eac7e3d193f5a
One proof (sorted_insert
) got longer, but otherwise on par with sauto.
I guess one can make a MathComp-idiomatic version and see how sauto/itauto works out then
Karl Palmskog said:
Théo Zimmermann if you think a PR for this would be welcome, I can make one (probably next week). However, we will have to ping in those who actually know the implementation of
firstorder
and/orintuition
(e.g., PMP) to make sure it's technically accurate and a fair assessment of the situation.
Sounds like a good plan!
Karl Palmskog said:
Théo Zimmermann if you think a PR for this would be welcome, I can make one (probably next week). However, we will have to ping in those who actually know the implementation of
firstorder
and/orintuition
(e.g., PMP) to make sure it's technically accurate and a fair assessment of the situation.
I'd say it's not entirely accurate. While the procedure behind sauto is theoretically complete for first-order intuitionistic logic, the implementation isn't. It sacrifices completeness to work well for the kinds of problems which typically appear in Coq developments (they usually are not purely "first-order", require some unfolding, equality reasoning, reasoning about inductive types, etc). If you run the tactics on purely first-order problems, "firstorder" wins unequivocally. But it turns out truly pure first-order reasoning is not that useful in typical Coq practice.
A more accurate description of sauto would be: a supercharged version of eauto which can also do some first-order reasoning typical for Coq developments.
And more than just first-order reasoning, most importantly case reasoning on inductive predicates.
thanks for summarizing the caveats. Given the "legacy" state of firstorder
, which is only semi-maintained (I remember PMP calling the implementation very difficult to work with), I still think it's worth mentioning sauto in the Coq manual/refman, though.
for example, I don't think Metis is complete for the first-order fragment of HOL, but it's heavily used in HOL4 and Isabelle (and probably also HOL Light, but I never tried)
I saw this not-so-subtle snipe on the topic of automation and hammers [my emphasis]:
One of the reasons I prefer higher-order logic to dependent type theories — apart from simple semantics, equality that works and no need to put everything in the kernel — is that dependent types seem to make automation much more difficult. Groups with access to institutional support and steady, ample resources still don’t seem to have duplicated what had been built at Cambridge on a single £250K grant. And please don’t say “dependent type checking makes other automation unnecessary”. Yes, I keep hearing this.
(my conclusion: there needs to be better marketing of all Coq's recent automation, including sauto/CoqHammer, itauto, Elpi/Trakt, Equations, lia/lra/zify/MC+zify, ...)
Slightly oftopic: does someone have a working setup of automation for mathcomp that you can recommend? CoqHammer/sauto worked somewhat for the examples in the "Mathematical Components" book. When I tried to use it in a real project with lots of imports, the provers never finish and often run out of memory. sauto
needs to be given which lemmas to use, which I guess can be solved by building a hint database, but I never did that. The only automation I ended up using was Ltac ssrnat_lia := rewrite /leq /subn /subn_rec /addn /addn_rec /muln /muln_rec; lia.
which I'd like to improve upon.
For lia
, you should use https://github.com/math-comp/mczify then From mathcomp Require Import zify
(and not Require Import Lia
or Require Import Psatz
), then lia
works fine with MathComp.
Similarly, for ring/field, you have https://github.com/math-comp/algebra-tactics
Alex Loiko said:
Slightly oftopic: does someone have a working setup of automation for mathcomp that you can recommend? CoqHammer/sauto worked somewhat for the examples in the "Mathematical Components" book. When I tried to use it in a real project with lots of imports, the provers never finish and often run out of memory.
sauto
needs to be given which lemmas to use, which I guess can be solved by building a hint database, but I never did that. The only automation I ended up using wasLtac ssrnat_lia := rewrite /leq /subn /subn_rec /addn /addn_rec /muln /muln_rec; lia.
which I'd like to improve upon.
Bumping this question as I'm curious too.
Also besides practical tools I'd like to know what literature there is out there the general idea of having automated theorem provers make use of small scale reflection efficiently, i.e teaching a computer to swap between representations based on convenience.
Would that just be subsumed under general rewriting theory?
@Patrick Nicodemus This is probably not what you are looking for, but Algebra Tactics (mentioned above) somehow uses small scale reflection in reification. IMO, the idea is generic enough to make use of other reflexive tactics, e.g., (Braibant and Pous, 2012), in the presence of MathComp-style overloaded operators. https://doi.org/10.4230/LIPIcs.ITP.2022.29
I am having trouble getting coq-hammer to find the ATP's I installed. I added all of them to the path and changed the file names as it says on the website so that running "vampire" in the shell calls vampire and so on. I installed coq-hammer using opam. I checked the opam config env and it seems to have the file paths I want.
I installed the github version now, not through opam but I have the same problem. I can't pass the tests
I upgraded to the latest version of proof-general, too. The problem still persists on the command line so it's not an emacs thing.
Alright, I figured it out. Coqhammer finds the libraries by calling Ocaml's "Sys.command" so I had to make sure that whatever shell ocaml invokes to make that happen has those commands available. Shells other than the login shell don't play nice with aliases and I also think the tilde shorthand for the home directory breaks things.
I added all the paths to /etc/environment and I think that worked.
Last updated: Mar 29 2024 at 07:01 UTC