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`

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`

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.

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/or`intuition`

(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/or`intuition`

(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 was`Ltac 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: Jan 29 2023 at 19:02 UTC