Stream: math-comp users

Topic: hammer


view this post on Zulip Bas Spitters (Jul 11 2022 at 13:43):

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?

view this post on Zulip Bas Spitters (Jul 12 2022 at 11:38):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:40):

@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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:40):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:42):

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.

view this post on Zulip Bas Spitters (Jul 12 2022 at 11:47):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:48):

you can do boolean reflection also in itauto: https://gitlab.inria.fr/fbesson/itauto/-/blob/master/test-suite/refl_bool.v

view this post on Zulip Bas Spitters (Jul 12 2022 at 11:51):

Quick question about itauto. I see it is implemented in ml. Is it trusted or proof producing?

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:51):

I was experimenting with porting this insertion sort tutorial from coqhammer to itauto as an example, but didn't make it go through yet.

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:52):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 11:55):

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.

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:02):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:03):

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.

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:09):

We might use a script that tries to replace calls to intuition with something simpler.

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:09):

It would be good if a linter/IDE started to make such suggestions

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:10):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:11):

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.

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:19):

Would any of these tactics work for mc finite sets?

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:20):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:22):

or directly write mc_set_solver to use itauto in several calls with the right leaf tactics

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:23):

For reference:
https://plv.mpi-sws.org/coqdoc/stdpp/stdpp.sets.html

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:25):

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.

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:25):

@Paolo Giarrusso will know ;-)

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:27):

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)

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:29):

set_solver definitely needs _some_ first-order reasoning — so wiring it with sauto might make sense

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:30):

I tried it super-briefly and at least the basics do work out

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:33):

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_solveror whatever). Asking for a friend who might do benchmarking at some point.

view this post on Zulip Bas Spitters (Jul 12 2022 at 12:33):

@Paolo Giarrusso great. If you have something more definitive, please let us know.

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:35):

@Karl Palmskog it'd make sense and I expect Robbert would agree

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:37):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:40):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:41):

in contrast, itauto can likely be used without anyone changing much of their practices, just some small syntax adaptations.

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:43):

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

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:45):

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.

view this post on Zulip Paolo Giarrusso (Jul 12 2022 at 12:49):

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

view this post on Zulip Karl Palmskog (Jul 12 2022 at 12:59):

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.

view this post on Zulip Łukasz Czajka (Jul 12 2022 at 20:53):

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".

view this post on Zulip Karl Palmskog (Jul 12 2022 at 21:02):

thanks, I'll try that one too, but one interesting challenge with the linked sort.v was the switch between Prop predicate and bool

view this post on Zulip Łukasz Czajka (Jul 12 2022 at 21:05):

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.

view this post on Zulip Karl Palmskog (Jul 12 2022 at 21:07):

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

view this post on Zulip Ben Siraphob (Jul 13 2022 at 01:53):

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

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 10:31):

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?

view this post on Zulip Karl Palmskog (Jul 13 2022 at 11:24):

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

view this post on Zulip Karl Palmskog (Jul 13 2022 at 11:35):

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.

view this post on Zulip Karl Palmskog (Jul 13 2022 at 11:36):

I guess one can make a MathComp-idiomatic version and see how sauto/itauto works out then

view this post on Zulip Théo Zimmermann (Jul 13 2022 at 11:46):

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!

view this post on Zulip Łukasz Czajka (Jul 13 2022 at 18:40):

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.

view this post on Zulip Łukasz Czajka (Jul 13 2022 at 18:43):

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.

view this post on Zulip Łukasz Czajka (Jul 13 2022 at 18:46):

And more than just first-order reasoning, most importantly case reasoning on inductive predicates.

view this post on Zulip Karl Palmskog (Jul 13 2022 at 19:36):

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.

view this post on Zulip Karl Palmskog (Jul 13 2022 at 19:39):

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)

view this post on Zulip Karl Palmskog (Jul 31 2022 at 20:48):

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.

view this post on Zulip Karl Palmskog (Jul 31 2022 at 20:55):

(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, ...)

view this post on Zulip Alex Loiko (Aug 06 2022 at 13:25):

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.

view this post on Zulip Pierre Roux (Aug 06 2022 at 16:15):

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

view this post on Zulip Patrick Nicodemus (Sep 06 2022 at 22:37):

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?

view this post on Zulip Kazuhiko Sakaguchi (Sep 06 2022 at 23:23):

@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

view this post on Zulip Patrick Nicodemus (Sep 07 2022 at 01:24):

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.

view this post on Zulip Patrick Nicodemus (Sep 07 2022 at 02:35):

I installed the github version now, not through opam but I have the same problem. I can't pass the tests

view this post on Zulip Patrick Nicodemus (Sep 07 2022 at 02:42):

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.

view this post on Zulip Patrick Nicodemus (Sep 07 2022 at 04:24):

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