lukaszcz / coqhammer Goto Github PK

Very cool project!

I was just testing it out with some examples from the Software Foundations book. One example I tried it seemed Z3 found a proof, but the reconstruction failed. From https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab199 I tried the theorem ev_plus_plus. It failed on its own, but after `intros. apply (ev_ev__ev (n+n) (m+p))."

It gets into the state

2 subgoals
n, m, p : nat
H : ev (n + m)
H0 : ev (n + p)
______________________________________(1/2)
ev (n + n + (m + p))
______________________________________(2/2)
ev (n + n)

From which hammer says that Z3 succeeded but the proof failed to reconstruct:

Running provers (using 8 threads)...
Z3 succeeded
 - dependencies: H, LF.Logic.plus_comm3_take2, Coq.Arith.Plus.plus_assoc_reverse, ev_sum, H0
 - definitions: 
Trying tactic Reconstr.reasy...
Trying tactic Reconstr.rsimple...
Trying tactic Reconstr.rcrush...
Trying tactic Reconstr.rblast...
Trying tactic Reconstr.rscrush...
Trying tactic Reconstr.ryelles4...
Trying tactic Reconstr.rexhaustive1...
Trying tactic Reconstr.rreconstr4...
Trying tactic Reconstr.rrauto4...
Trying tactic Reconstr.ryreconstr...
Trying tactic Reconstr.ryelles6...
Trying tactic Reconstr.rreconstr6...
Error: Hammer failed to solve the goal.

For the record I solved the remainder with only rewriting and applying H, H0, PeanoNat.Nat.add_shuffle1, ev_sum, double_plus, and ev_double. So it looks very close to the dependencies used by Z3.

I am curious if there is some way I can debug this failure, or tweak something to make it succeed. I tried Set Hammer ReconstrLimit 20. but it still failed. I also tried disabling Z3 in hammer, but the other ATPs failed.

Coq version: 8.12.2
Hammer version: 1.3

So far the sauto/hauto/qauto tactics family has been amazing for my Coq development. However, it does not work quite well when we have lemmas with implicit arguments and a bunch of implicit type class constraints. This problem becomes more unfortunate when I am also using the stdpp library (https://gitlab.mpi-sws.org/iris/stdpp), which contains a lot of such lemmas. One example of such lemmas is insert_mono from stdpp.fin_maps.

Let's say we have a lemma lem whose type is like forall {A}, .... We can use this lemma with eauto (eauto using lem), but we can not use it directly with sauto. Running sauto use: lem gives me errors about not being able to infer the implicit parameter A. (the use tactic behaves the same)

In this simple case, we can just prepend the lemma with @, so sauto use: @lem works. However, if this lemma also has a lot of type class constraints, sauto use @lem (or hauto, etc) may either fail or run forever. I suspect it is because the amount of assumptions sauto needs to discharge is huge. For example, pose proof @insert_mono (or use @insert_mono) produces the following hypothesis. (I apologize for the out-of-context example, but my point is some lemmas have a lot of typeclass assumptions)

  H : ∀ (K : Type) (M : Type → Type) (H : FMap M) (H0 : 
                                                    ∀ A : Type, 
                                                      Lookup K A (M A)) 
         (H1 : ∀ A : Type, Empty (M A)) (H2 : ∀ A : Type, PartialAlter K A (M A)) 
         (H3 : OMap M) (H4 : Merge M) (H5 : ∀ A : Type, FinMapToList K A (M A)) 
         (EqDecision0 : EqDecision K),
         FinMap K M
         → ∀ (A : Type) (m1 m2 : M A) (i : K) (x : A),
             m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2

My current workaround is to run epose proof lem first. For example, epose proof insert_mono produces the following hypothesis instead.

  H : ∀ (m1 m2 : amap ?A) (i : atom) (x : ?A), m1 ⊆ m2 → <[i:=x]> m1 ⊆ <[i:=x]> m2

As you can tell, Coq has already resolved all the type class constraints. If I run sauto now, it is more likely to solve the goal than sauto use: @lem.

It would be great if sauto family also accepts lemmas with implicit arguments like eauto does, and let Coq figure out what the type class instances are. I reckon this should be a fairly simple fix, because sauto apparently works well if I epose proof the lemmas first.

Thanks for your hardwork!

Recent versions of OCaml (> 4.07) have deprecated the module Pervasives in favor of Stdlib. This means that CoqHammer currently shows deprecation warnings like the following when compiled with, e.g., OCaml 4.09.0:

File "src/coq_transl.ml", line 1141, characters 30-48:
1141 |   Hhlib.sort_uniq (fun x y -> Pervasives.compare (fst x) (fst y)) axs
                                     ^^^^^^^^^^^^^^^^^^
Alert deprecated: module Stdlib.Pervasives
Use Stdlib instead.

If you need to stay compatible with OCaml < 4.07, you can use the
stdlib-shims library: https://github.com/ocaml/stdlib-shims

Since Coq users are in my experience slow to migrate to new OCaml compilers, making stdlib-shims a dependency may be the best solution. However, note that these deprecations are not urgent to address as of right now.

Because of the different cost model and slightly different heuristics there will probably always be some problems which can be quickly solved by the old tactic set but not the sauto-based new ones.

https://github.com/lukaszcz/coqhammer/blob/v1.1.1-coq8.10/src/hammer_lib.ml#L335

Dear Coq Hammer team,

over night the SHA code of many coq hammer git tarballs used by opam packages changed. I tested:

https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.13.tar.gz
https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.14.tar.gz
https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz

All 3 packages have as of today a different hash code than given in opam. Since this breaks Coq Platform I will fix the opam package, but I would ask you to avoid changing tags after the facts without prior notice and without adjusting the opam packages pretty much at the same time.

Best regards,

Michael

It will be helpful if the tactic generated by hammer can first remove unused assumptions. In my simple example, (a) takes 0.046s while (b) takes 5.888s.

(a)
clear -H13.
Time hauto use: Z.add_0_r unfold: sval_refine.
(b)
Time hauto use: Z.add_0_r unfold: sval_refine.

It's worth mentioning that I added clear -H13 at the beginning because otherwise hammer would time out. But that doesn't matter for the main point.

When I try to use opam to install CoqHammer 1.3 for Coq 8.12 on macOS I get the following (after typing "opam install coq-hammer").

The following actions will be performed:

• install conf-clang 1 [required by coq-hammer]
• install coq-hammer-tactics 1.3+8.12 [required by coq-hammer]
• install coq-hammer 1.3+8.12
  ===== 3 to install =====
  Do you want to continue? [Y/n] y

<><> Gathering sources ><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The sources of the following couldn't be obtained, aborting:
- coq-hammer.1.3+8.12: Bad checksum
- coq-hammer-tactics.1.3+8.12: Bad checksum

The issue is not limited to my configuration: I got a report about the same problem from another user.

@palmskog could you look into this?

I run "dune build" and get the following error:

  coqdep theories/Plugin/Hammer.v.d

*** Warning: in file Hammer.v, library Hammer.Tactics.Tactics is required and has not been found in the loadpath!
File "./theories/Plugin/Hammer.v", line 1, characters 27-42:
Error: Unable to locate library Tactics.Tactics with prefix Hammer.

I notice that uncommenting the line

;(theories Hammer.Tactics)

in the file theories/Plugin/dune solves the problem. But I don't know what the purpose of commenting the line out was and whether it won't affect something else.

@palmskog I made the 1.3.1 release for Coq 8.10, 8.11, 8.12 and 8.13. Could you create the right opam packages and make sure they end up in the right remote repository? BTW, if you're no longer up to maintaining the opam packages and/or travis CI for CoqHammer, let me know and I'll learn to do this myself (at some point).

Dear CoqHammer developer,

I am trying to build CoqHammer from the source in Mac. After building it, I used CoqHammer in CoqIde. But I meet the following problem.

The Coq code are a part of the Software Foundation's Hoare Logic section. I found if I didn't use From Hammer Require Import Hammer. nothing went wrong. But after loading the hammer plugin, the problem occurred.

I am not sure is it an error or just due to my computer's reason.

Sincerely,
Zhang Liao

Dear devs,

in Coq we are considering requiring plugins in the CI to use the same set of compiler flags for warnings than the main Coq tree (c.f. coq/coq#9605 ), in particular, this means that the plugins should now compile warning-free, except for deprecation notices.

Note that some of the raised warnings are really fatal, [like missing match cases].

Please, try to fix OCaml warnings present in your codebase, thanks!

CoqHammer dependency prediction fails when calling "hammer" from CoqIDE on MacOS. Curiously, it works with ProofGeneral and from the command line. Configuration of CoqIDE may be a problem: look into this later.

I was following the video tutorial but got this issue:

→  hammer_switch                          ocaml-base-compiler.4.12.0  hammer_switch
(meta_learning) brandomiranda~/sketching-learning-coq ❯ opam install coq-hammer-tactics 
[ERROR] No package named coq-hammer-tactics found.

How do I install CoqHammer?

The Coq team released Coq 8.15.0 on January 13, 2022.
The corresponding Coq Platform release 2022.02 should be released before February 28, 2022.
It can be delayed in case of difficulties until April 11, 2022, but this should be an exception.

This issue is to inform you that to our (possibly a few days old) best knoweldege the latest released version of your project (1.3.2+8.14) does not work with Coq 8.15.0.
We tried to remove version restrictions in opam files and possibly make or configure files, but this did not suffice.

Please note that in Coq Platform CI (unlike Coq CI) we test only released / tagged versions. Coq CI appears to test this project, but has some special handling for your project which makes it difficult to retrieve the commit it tests for your project.

Could you please create a tag and opam package, or communicate us any existing tag that works with Coq branch v8.15, preferably before February 14, 2022?
In case we might have to delay the Coq Platform release cause of issues with your project, we would prefer to be informed about the situation as early as possible.

In case the tag and opam package are available before January 25, 2022, it will be included in an early Coq Platform beta release of the for Coq 8.15.0.

The working branch of Coq Platform, which already supports Coq version 8.15.0, can be found here https://github.com/coq/platform/tree/main.

Please don't close this issue, even after creating the new tag and/or opam package.
We will close the issue after updating Coq Platform.
This is a measure of 'double book keeping' in order to avoid that we ship the wrong version.

In any case, Coq Platform won't be released before this issue is closed!

Thanks!

P.S.: this issue has been created automatically based on CI status.

CC: coq/platform#193

I'm trying to build from source, but make fails because it doesn't handle hammer.mlg.

[jayce@tracer coqhammer]$ make
coq_makefile -f _CoqProject -o Makefile.coq
Unknown option src/hammer.mlg
[...]
make: *** [Makefile:8: Makefile.coq] Error 1

I'm using the latest versions of everything. Is there a workaround?

Dear designer of coqhammer,

I make some changes to the coq source code and then want to use coqhammer in my changed coq. I have got the directory Hammer which contains necessary files for coqhammer in the opam directory.
Then I add the directory Hammer in coq's source. What should I do so that I can use tactic from coqhammer in my coq version?

coq_makefile -f _CoqProject -o Makefile.coq            
make -f Makefile.coq                                 
make[1]: Entering directory '/home/user/.opam/ocaml-base-compiler/.opam-switch/build/coq-hammer.1.1+8.9'
COQDEP VFILES                                                                
CAMLDEP src/provers.mli                                 
CAMLDEP src/features.mli                                  
CAMLDEP src/coq_transl.mli                             
CAMLDEP src/tptp_out.mli                             
CAMLDEP src/coq_convert.mli
CAMLDEP src/hashing.mli                                                      
CAMLDEP src/coq_typing.mli                              
CAMLDEP src/defhash.mli                                 
COQDEP src/hammer_plugin.mllib           
CAMLDEP src/partac.ml         
CAMLDEP src/provers.ml                                  
CAMLDEP src/features.ml                            
File "src/provers.ml", line 193, characters 143-145:
Warning 14: illegal backslash escape in string.       
CAMLDEP src/parallel.ml          
CAMLDEP src/opt.ml        
CAMLDEP src/coq_transl.ml                             
CAMLDEP src/tptp_out.ml          
CAMLDEP src/coq_convert.ml
CAMLDEP src/hashing.ml                  
CAMLDEP src/coq_typing.ml                    
CAMLDEP src/defhash.ml    
CAMLDEP src/coqterms.ml                                                
CAMLDEP src/coq_transl_opts.ml                       
CAMLDEP src/timeout.ml                                                       
CAMLDEP src/msg.ml    
CAMLDEP src/hh_term.ml
CAMLDEP src/hhlib.ml       
CAMLDEP src/hammer_errors.ml                            
CAMLDEP -pp src/hammer.ml4                      
COQC theories/Reconstr.v                        
CAMLOPT -c  src/hammer_errors.ml                                                                           
CAMLOPT -c  src/hhlib.ml               
CAMLOPT -c  src/hh_term.ml
CAMLOPT -c  src/msg.ml
CAMLOPT -c  src/timeout.ml
CAMLOPT -c  src/coq_transl_opts.ml
CAMLC -c src/hhlib.ml
CAMLC -c src/coq_transl_opts.ml
CAMLC -c src/hh_term.ml
CAMLOPT -c  src/opt.ml
CAMLOPT -c  src/parallel.ml
CAMLC -c src/features.mli
CAMLC -c src/provers.mli
CAMLOPT -c  src/partac.ml
CAMLOPT -c  src/coqterms.ml
CAMLC -c src/coqterms.ml
CAMLOPT -c  src/features.ml
CAMLC -c src/defhash.mli
File "src/features.ml", line 48, characters 28-249:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Id ""
CAMLC -c src/coq_typing.mli
CAMLC -c src/hashing.mli
CAMLC -c src/coq_convert.mli
CAMLC -c src/tptp_out.mli
CAMLC -c src/coq_transl.mli
CAMLOPT -c  src/defhash.ml
CAMLOPT -c  src/hashing.ml
CAMLOPT -c  src/coq_convert.ml
CAMLOPT -c  src/tptp_out.ml
CAMLOPT -c  src/coq_typing.ml
File "src/coq_typing.ml", line 117, characters 16-61:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(_,
(SortProp|SortSet|SortType|Var _|Const _|App (_, _)|Case (_, _, _, _, _)|
Cast (_, _)|Fix (_, _, _, _, _)|Equal (_, _)), _, _)
CAMLOPT -c  src/coq_transl.ml
File "src/coq_transl.ml", line 500, characters 16-628:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(_,
(SortProp|SortSet|SortType|Var _|Const _|App (_, _)|Case (_, _, _, _, _)|
Cast (_, _)|Fix (_, _, _, _, _)|Equal (_, _)), _, _)
File "src/coq_transl.ml", line 455, characters 8-3062:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(_,
(SortProp|SortSet|SortType|Var _|Const _|App (_, _)|Case (_, _, _, _, _)|
Cast (_, _)|Fix (_, _, _, _, _)|Equal (_, _)), _, _)
File "src/coq_transl.ml", line 1032, characters 2-886:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
(_,
(SortProp|SortSet|SortType|Var _|Const _|App (_, _)|Case (_, _, _, _, _)|
Cast (_, _)|Fix (_, _, _, _, _)|Equal (_, _)), _, _)
File "src/coq_transl.ml", line 111, characters 0-62:
Warning 34: unused type axioms_monad.
CAMLOPT -c  src/provers.ml
File "src/provers.ml", line 193, characters 143-145:
Warning 14: illegal backslash escape in string.
CAMLOPT -pp -c  src/hammer.ml4
File "src/hammer.ml4", line 256, characters 34-72:
Warning 3: deprecated: ArgArg
Use version in [Locus]
File "src/hammer.ml4", line 265, characters 30-56:
Warning 3: deprecated: ArgVar
Use version in [Locus]
CAMLOPT -a -o src/hammer_plugin.cmxa
CAMLOPT -shared -o src/hammer_plugin.cmxs
COQC theories/Hammer.v
g++ -std=c++11 -DCOQ_MODE -O2 -Wall src/predict/main.cpp -o predict
gcc -O2 -Wall src/htimeout/htimeout.c -o htimeout
src/predict/main.cpp:2:10: fatal error: memory: No such file or directory
 #include <memory>
          ^~~~~~~~
compilation terminated.
make[2]: *** [Makefile.coq.local:4: predict] Error 1
make[2]: *** Waiting for unfinished jobs....
make[1]: *** [Makefile.coq:328: all] Error 2
make[1]: Leaving directory '/home/user/.opam/ocaml-base-compiler/.opam-switch/build/coq-hammer.1.1+8.9'
make: *** [Makefile:2: all] Error 2

I don't see anything wrong with my libstdc++ and haven't had this problem with the previous 8.9.

As described in this blogpost, builds of CoqHammer that use make parallelism (e.g., make -j3) sometimes fail, and in a nondeterministic ("flaky") way. Failed builds give the message: Error: Corrupted compiled interface. It may be due to some kind of race condition in compilation of OCaml files.

The best way to fix this problem is likely to switch from coq_makefile to dune (which has more robust support for parallel builds). However, since CoqHammer builds so quickly, I suggest, as a workaround, that we simply turn off parallelism in all OPAM packages until the project is fully ported to dune.

Dear Coq-Hammer Team,

@palmskog requested here: (coq/platform#10) to include your development into the Coq Platform, which is the standard user facing distribution of Coq.

Coq Platform has a "full" and "extended" level. Inclusion in the "full" level requires an explicit statement by the maintainers, that they agree to the charter of the Coq Platform and intend to publish compatible releases for each release of Coq in a reasonable time frame. For the "extended" level the rules are more relaxed. For developments in the "full" level, users should be able to rely on that the package is maintained, so that they can base their own development on it without a large risk that they have to factor it out again later cause of maintenance issues.

Can you please comment in the Coq Platform issue mentioned above if you do want your package included in the Coq Platform in agreement to the Coq Platform charter, and if so which level you would prefer?

Best regards,

Michael

We have been using CoqHammer extensively to translate proofs at the "specification level" from Isabelle/HOL to Coq (see project and CoqPL materials). I think this worked really well, echoing Paulson's experience going from HOL Light to Isabelle/HOL, and is an application area that should be highlighted.

However, once we were done hammering, it appeared unnecessary to still have the whole CoqHammer plugin as a requirement for the project, when all we really needed were a few of the CoqHammer standalone tactics. Isabelle doesn't have this problem, since all hammer "replacement tactics", such as metis, are built-in.

Would it make sense to have separate packages (and thus build scripts) for CoqHammer's tactics and the CoqHammer plugin? Would a PR to implement this be welcome?

The "hammer" tactic should display the minimum (user) name for each dependency, not the fully qualified name.

Thanks to our earlier compatibility efforts, release 1.1 appears to work fine with the newly released Coq 8.9.0.

However, the version name (1.1+8.8) and version string (CoqHammer 1.1 for Coq 8.8 and Coq 8.9beta) may be misleading. So, should I modify the existing OPAM package for 8.9 compatibility, or do you want to make a new release (and have a new OPAM package)?

The default rewriting tactic (rewrite/autorewrite) will refuse to rewrite under binders/arrows. See the manual. Unfortunately, that means that sauto will also not do those rewriting if they are in the rew:db: hint set.

Example:

Parameter A B : Prop. 
Parameter ab : A <-> B.
Hint Rewrite ab : ab.

Lemma test : (forall x : nat, A) -> B.
  sauto db:ab. (* fails *)

  setoid_rewrite ab.
  sauto (* succeeds *)
Qed.

The workaround is to define a custom autorewrite with ab with

Ltac ab_simp :=
  progress (repeat (rewrite_strat topdown hints ab); 
  repeat match goal with 
  | H : _ |- _ => rewrite_strat topdown hints ab in H
  end).

Then sauto simp+:ab_simp proves the test lemma.

This is kind of exactly what was done for boolean reflection, but it would be nice if the default sauto rewriting was already as powerful as this. It is possible that this change may break existing proofs with some not-well designed rewriting systems. Therefore, adding it as an extra option like setoid_rew:on might be worthwhile.

I'm looking for a tool which can find counterexamples to Coq conjectures which do not hold.

For example, if I do

Lemma bad1: forall n, n + n + n = 2 * n.
Proof.
  hammer.

I just get back

Error: Hammer failed: ATPs failed to find a proof

Instead, I'd like to get something like

Counterexample found: 
n := 1

Is there an option for that? If not, would it be hard to implement? If I understand correctly, if Z3 answers sat, all you'd have to do would be to call (get-model) and either display the raw output, or, as a plus, translate it back to Coq syntax.

I think this would be a very useful feature!

Coq OPAM archive maintainers recently noticed that the CoqHammer website (http://cl-informatik.uibk.ac.at/cek/coqhammer/) went down, possibly due to some reorganization at the hosting university.

This has left several files with early versions of CoqHammer unavailable. Even if the website comes back up eventually, would it be possible to host these files on GitHub for preservation purposes? For example, future research may do some comparison of hammers across versions.

Some examples of (former URLs of) unavailable files:
http://cl-informatik.uibk.ac.at/cek/coqhammer/coqhammer-1.0.3-coq8.6.tar.gz
http://cl-informatik.uibk.ac.at/cek/coqhammer/coqhammer-1.0.6-coq8.6.tar.gz
http://cl-informatik.uibk.ac.at/cek/coqhammer/coqhammer-0.9-coq8.5.tar.gz
http://cl-informatik.uibk.ac.at/cek/coqhammer/atp-experiments.tgz

Here is an example of what a "historical" release can look like on GitHub: https://github.com/math-comp/math-comp/releases/tag/archive - basically, the idea is to use GitHub's feature to associate a release with a manually uploaded file.

On Mac OS X dependency prediction gives more dependencies than asked for, which seems to substantially decrease CoqHammer success rate. This can be reproduced using the "predict" tactic.

Since the master branch now tracks the development version of Coq, will there be a specific branch for Coq 8.9 (which is already diverging from the development Coq)? Or is coq8.8 still the branch to use for 8.9-related pull requests?

I run "dune runtest" (after installing CoqHammer with "dune install") and get:

    coqc alias tests/plugin/runtest (exit 1)

(cd _build/default/tests/plugin && /Users/rkw886/.opam/default/bin/coqc plugin_test.v)
CoqHammer (dev) for Coq 8.12
Found 9907 accessible Coq objects.
(...)
Error: System error: "./plugin_test.vos: Permission denied"

    coqc alias tests/tactics/runtest (exit 1)

(cd _build/default/tests/tactics && /Users/rkw886/.opam/default/bin/coqc tactics_test.v)
Error: System error: "./tactics_test.vos: Permission denied"

I fixed issue #45 but now I don't know how to fix Travis CI. @palmskog could you help?

Sorry to trouble you. Sometimes I think the tactic predict returns too many premises which costs too much time. Is it possible to do some change to the code to limit the number of the premises returned? It seems can not be changed by some constants in the tactics like predict 500. If it is possible, which file should I change?

Thanks for merging the changes for separate tactics and plugin packages - this will be a big improvement for the projects I'm using CoqHammer in. On that note, do you think it's worth applying these changes to the coq8.9 branch also? If so, I can do a PR for that, but then I think there should be a new release based on that branch as well.

In "sauto" (sauto.ml) the head of a hypothesis (and of the goal) should be determined modulo weak head reduction. Use Reductionops.whd_all_stack or something like this.

Coq version: 8.12
Operating System: Ubuntu 20.04
interface: CoqIde (8.12?)
the problem occurs for any lemmas.
Code example:
Lemma not_True : (~ True) = False.
Proof.
hammer.
Qed.
which generates the following error:
CoqHammer bug: please report: Not_found
I am working in classical logic with proof irrelevance (Coq.Logic.Classical_Prop and Coq.Logic.PropExtensionality libraries)
Does anyone has an idea of what is wrong?
Thanks in advance.

Branch coq8.11 at de94498.
it's because of 2f05090. Is it needed?

Welcome to Coq 8.11.0 (April 2020)

Coq < From Coq Require Import Extraction.
[Loading ML file extraction_plugin.cmxs ... done]

Coq < From Hammer Require Import Hammer Reconstr.
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file r_syntax_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]
[Loading ML file hammer_lib.cmxs ... done]
[Loading ML file hammer_tactics.cmxs ... failed]
Toplevel input, characters 0-43:
> From Hammer Require Import Hammer Reconstr.
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: while loading
/Users/lelf/.opam/coq811/lib/coq/user-contrib/Hammer/Tactics/hammer_tactics.cmxs:
execution of module initializers in the shared library failed: "Anomaly: generic argument already declared: mlname."

Hi,

I assume this is something that should not happen: The hammer tactic reports that CVC4 found a solution for a goal which is provably false (and where nothing in the context allows deriving False). Then, hammer fails to reconstruct the proof, as it obviously should.

I'm sorry that this example is a bit long; I removed the parts of my proof that it didn't need, and this is what is left. I included the proofs of the lemmas to demonstrate that there is nothing inconsistent there. I added comments and Compute statements at the end demonstrating that the goal after the "exists" statement should be unprovable.

(Furthermore, and I assume this is a different issue, if I execute everything in CoqIde straight to the end, including the "hammer." statement, coqproofworker.opt segfaults (no OOM). So what I do in coqtop to demonstrate this is to execute up to the point just before the "hammer." statement, wait until everything before that has been evaluated, and then proceed to the hammer statement.)

I'm using coq 8.13.2 with coq-hammer 1.3.2+8.13 from opam.

Require Import Arith.
Require Import Psatz.
Require Import FunInd.
Require Import Recdef.
Require Import ssreflect ssrfun ssrbool.
Require Import Unicode.Utf8.
Require Import Coq.Program.Basics.

From Hammer Require Import Tactics Hammer Reflect.

Set Hammer GSMode 5.
Set Hammer ATPLimit 20.
Set Hammer ReconstrLimit 5.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition log3_iter_internal_round tup :=
    match tup with
    | (log_up_counter, up_counter, dist_next) =>
            match dist_next with
            | O => ((S log_up_counter), (S up_counter), (2 * up_counter + 1))
            | S dist_next' => (log_up_counter, (S up_counter), dist_next')
            end
    end.

Definition log3_iter (down_counter log_up_counter up_counter dist_next : nat) :=
    match iter (nat*nat*nat) down_counter log3_iter_internal_round (log_up_counter, up_counter, dist_next) with
    | (val, _, _) => val
    end.

Fixpoint log3_iter_alternative down_counter log_up_counter up_counter dist_next :=
    match down_counter with
    | O => log_up_counter
    | S down_counter' => match dist_next with
                            | O => log3_iter_alternative down_counter' (S log_up_counter) (S up_counter) (2 * up_counter + 1)
                            | S dist_next' => log3_iter_alternative down_counter' log_up_counter (S up_counter) dist_next'
                            end
    end.

Definition log3_nat (n : nat) : nat := log3_iter (Nat.pred n) 0 1 1.

Lemma iter_round : ∀ (A : Type) (n : nat) (f : A -> A) (x0 : A), iter A (S n) f x0 = f (iter A n f x0).
Proof.
    auto.
Qed.

Lemma iter_plus : ∀ {A : Set} (n1 n2 n3 : nat) (x0 : A) (f : A -> A),
    n1 = n2 + n3 -> iter A n1 f x0 = iter A n2 f (iter A n3 f x0).
Proof.
    induction n1. sauto lq: on. sauto q: on.
Qed.

Lemma log3_iter_alternative_equal : ∀ down_counter log_up_counter up_counter dist_next,
    log3_iter_alternative down_counter log_up_counter up_counter dist_next =
    log3_iter down_counter log_up_counter up_counter dist_next.
Proof.
    intro.
    set (fst3 (tup : (nat*nat*nat)) := let '(p, _, _) := tup in p).
    assert (∀ (tup: (nat*nat*nat)), (let '(p, _, _) := tup in p) = fst3 tup) as Fst3. auto.

    set (fiter dc logup up dn := fst3 (iter (nat * nat * nat) dc log3_iter_internal_round (logup, up, dn))).
    unfold log3_iter.

    induction down_counter. sfirstorder.
    intros.

    assert (∀ down_counter log_up_counter up_counter dist_next,
            fst3 (iter (nat * nat * nat) down_counter log3_iter_internal_round (log_up_counter, up_counter, dist_next)) =
            fiter down_counter log_up_counter up_counter dist_next) as Fiter. auto.
    rewrite -> Fst3, -> Fiter.
    simpl. destruct dist_next.
    -   (* dist_next = 0 *)
        unfold log3_iter_alternative.
        rewrite -> IHdown_counter. repeat rewrite -> Fst3. unfold fiter. f_equal.
        rewrite (iter_plus (A:=nat*nat*nat) (n2:=down_counter) (n3:=1) (log_up_counter, up_counter, 0)). lia. auto.
    -   (* dist_next > 0 *)
        unfold log3_iter_alternative.
        rewrite -> IHdown_counter. repeat rewrite -> Fst3. unfold fiter. f_equal.
        rewrite (iter_plus (A:=nat*nat*nat) (n2:=down_counter) (n3:=1) (log_up_counter, up_counter, S dist_next)). lia. auto.
Qed.

Lemma log3_iter_alternative_spec : ∀ down_counter log_up_counter up_counter dist_next,
    3^(S log_up_counter) = dist_next + up_counter + 1 →
    dist_next < 2*3^log_up_counter →
    let s := log3_iter_alternative down_counter log_up_counter up_counter dist_next in
    3^s <= down_counter + up_counter < 3^(S s).
Proof.
    assert (∀ z, (3^z + (3^z + 3^z)) = 3*3^z); try lia.
    induction down_counter.
    -   do 3 intro. intros EQ LT. simpl.
        rewrite <- plus_n_O, -> H, <- Nat.pow_succ_r'.
        split; try lia.
        assert (up_counter = 3^(S log_up_counter) - dist_next - 1); try lia.
        rewrite -> H0, -> Nat.pow_succ_r'. lia.
    -   do 3 intro. intros EQ LT.
        destruct dist_next.
        +   rewrite -> plus_Sn_m, -> plus_n_Sm.
            apply IHdown_counter; try lia. simpl.
            repeat rewrite <- plus_n_O.
            rewrite -> H, <- Nat.pow_succ_r', -> EQ.
            lia.
        +   rewrite -> plus_Sn_m, -> plus_n_Sm.
            apply IHdown_counter.
            all: lia.
Qed.

Lemma log3_iter_spec : ∀ down_counter log_up_counter up_counter dist_next,
    3^(S log_up_counter) = dist_next + up_counter + 1 →
    dist_next < 2*3^log_up_counter →
    let s := log3_iter down_counter log_up_counter up_counter dist_next in
    3^s <= down_counter + up_counter < 3^(S s).
Proof.
    intros. subst s.
    rewrite <- log3_iter_alternative_equal. apply log3_iter_alternative_spec; auto.
Qed.

Lemma log3_nat_spec : ∀ n, 0<n → 3^(log3_nat n) <= n < 3^S (log3_nat n).
Proof.
    intros.
    set (s := log3_nat n).
    replace n with (Nat.pred n + 1); try lia.
    apply log3_iter_spec; auto.
Qed.

Lemma log3_nat_mono_weak : ∀ n, log3_nat n <= log3_nat (S n).
Proof.
    intros. unfold log3_nat, log3_iter. destruct n. auto. simpl Nat.pred.
    rewrite (iter_plus (A:=(nat*nat*nat)) (n1:=S n) (n2:=1) (n3:=n) (0, 1, 1)). lia.
    sauto q: on.
Qed.

Lemma log3_nat_mono : ∀ n m, n <= m -> log3_nat n <= log3_nat m.
Proof.
    intros.
    replace m with ((m-n)+n); try lia.
    induction (m-n). auto.
    hauto use: Nat.lt_succ_r, Nat.add_succ_l, Nat.le_lt_trans, Nat.add_comm, log3_nat_mono_weak.
Qed.

Lemma log3_nat_0 : ∀ n, n < 3 <-> log3_nat n = 0.
Proof.
    intros.
    split.
    -   sauto lq: on.
    -   intros Log0. do 3 (destruct n; auto).
        assert (2 < S (S (S n))). lia. apply log3_nat_mono in H.
        replace (log3_nat 3) with 1 in H; compute; lia.
Qed.

Lemma log3_nat_mul3 : ∀ a, 2 < a -> log3_nat (3*a) = S (log3_nat a).
Proof.
    intros a Gt2. do 3 (destruct a; try lia). clear Gt2.
    set (n := S (S (S a))).
    assert (0 < n) as Gt0; try lia.
    pose proof (log3_nat_spec Gt0) as [Spec1_1 Spec1_2].
    clear Gt0. assert (0 < 3*n) as Gt0. lia.
    pose proof (log3_nat_spec Gt0) as [Spec2_1 Spec2_2].
    clear Gt0.

    pose proof (log3_nat_0 (3*n)) as log3_3_pos.

    replace (log3_nat (3*n)) with (S (Nat.pred (log3_nat (3*n)))) in Spec2_1; try lia.

    rewrite -> Nat.pow_succ_r', <- Nat.mul_le_mono_pos_l in Spec2_1; auto.
    rewrite -> Nat.pow_succ_r', <- Nat.mul_lt_mono_pos_l in Spec2_2; auto.

    assert (3^log3_nat n < 3^log3_nat (3*n)) as Lt1. lia.
    assert (3^Nat.pred (log3_nat (3*n)) < 3^S (log3_nat n)) as Lt2. lia.

    rewrite <- Nat.pow_lt_mono_r_iff in Lt1, Lt2; auto; lia.
Qed.

Lemma log3_nat_pow3 : ∀ a, log3_nat (3^a) = a.
Proof.
    intros. induction a. compute. auto.
    destruct a. auto.
    rewrite -> Nat.pow_succ_r', log3_nat_mul3; auto.
    hauto use: Nat.le_gt_cases, log3_nat_0 unfold: lt.
Qed.

Lemma log3_nat_succ_same_within_pow3 : ∀ a, 0 < a ->
    log3_nat (S a) = log3_nat a <-> ∀ p, 3^p ≠ (S a).
Proof.
    intros a Gt0. destruct a. lia.
    pose proof (log3_nat_spec Gt0) as [Spec1_1 Spec1_2]. clear Gt0.
    assert (0 < S (S a)) as Gt0; try lia. pose proof (log3_nat_spec Gt0) as [Spec2_1 Spec2_2]. clear Gt0.
    split.
    -   intros Eq p.
        hcrush use: Nat.lt_neq, Eq, log3_nat_pow3, Nat.succ_lt_mono unfold: lt.
    -   intros Neq.
        unfold log3_nat, log3_iter. simpl Nat.pred. rewrite iter_round.
        case_eq (iter (nat * nat * nat) a log3_iter_internal_round (0, 1, 1)). intros [log_up_counter up_counter] dist_next Iter.
        case_eq dist_next; auto.
        intro Dist_next. rewrite Dist_next in Iter.
        unfold log3_nat, log3_iter in Spec1_1, Spec1_2, Spec2_1, Spec2_2.
        simpl Nat.pred in Spec1_1, Spec1_2, Spec2_1, Spec2_2.
        rewrite Iter in Spec1_1, Spec1_2.
        rewrite -> iter_round, -> Iter in Spec2_1, Spec2_2.
        simpl in Spec2_1, Spec2_2, Spec1_2, Spec2_2.
        replace (3 ^ log_up_counter + (3 ^ log_up_counter + (3 ^ log_up_counter + 0))) with (3*3^log_up_counter) in
            Spec2_1, Spec2_2, Spec1_2; try lia.
        replace (3 * 3 ^ log_up_counter + (3 * 3 ^ log_up_counter + (3 * 3 ^ log_up_counter + 0)))
                with ((3*(3*3^(log_up_counter)))) in Spec2_2; try lia.
        rewrite <- Nat.pow_succ_r' in Spec1_2, Spec2_1, Spec2_2. rewrite <- Nat.pow_succ_r' in Spec2_2.
                assert (S (S a) = 3^(S log_up_counter)). lia. hauto lq: on.
Qed.

Lemma log3_nat_eq_succ_is_pow3 : ∀ a, log3_nat (S a) = S (log3_nat a) -> ∃ b, S a = 3^b.
Proof.
    intros a Eq.

    (* The goal is, I believe, true until this exists instantiates b with something that makes it false: *)
    exists (S (log3_nat a)).

    (* Now, the goal of S a = 3^S (log3_nat a) is false: For example, with a=0,
            S 0 = 3^S (log3_nat 0) <-> 1 = 3^1 <-> 1 = 3. *)
    Compute (S 0 = 3^S (log3_nat 0)).

    (* The only assumption in the context is Eq : log3_nat (S a) = S (log3_nat a), which is not contradictory; eg.
       log3_nat (S 2) = S (log3_nat 2). *)
    Compute (log3_nat (S 2) = S (log3_nat 2)).

    (* Furthermore, there are no axioms in this file, and all lemmas have been duly proved, so there should be nothing in the
       context to derive False.

       Nevertheless, hammer purports to find a solution using CVC4, which it then fails to reconstruct. *)

    hammer.

Here's what hammer outputs:

Extracting features...
Running provers (5 threads)...
CVC4 (knn-256) succeeded
Minimizing dependencies...
- dependencies: Arith.PeanoNat.Nat.lt_succ_diag_r, Arith.PeanoNat.Nat.pow_0_r, Eq, Arith.PeanoNat.Nat.neq_0_lt_0,
                Bug.log3_nat_pow3, Bug.log3_nat_succ_same_within_pow3, Arith.PeanoNat.Nat.lt_neq
- inversions: Init.Datatypes.nat
Reconstructing the proof...
Trying reconstruction batch 1...
Trying reconstruction batch 2...
Trying reconstruction batch 3...
Trying reconstruction batch 4...
Trying reconstruction batch 5...
Trying reconstruction batch 6...
Trying reconstruction batch 7...
Hammer failed: proof reconstruction failed.

It should be possible to use the auto/eauto hint databases with sauto.

Coq devs just created the v8.11 branch which will eventually lead to Coq 8.11.0. To allow me to adjust OPAM and CI for this Coq branch, there needs to be a coq8.11 branch.

Hi,

I'm trying to run Hammer on the examples from the intro video, and I get the following error:

From Hammer Require Import Hammer.
Hammer_version. (* CoqHammer 1.3 for Coq 8.12 *)
Require Import PeanoNat.
Theorem n_or_Sn_Odd : forall (n : nat), Nat.Odd n \/ Nat.Odd (n + 1).
  Fail predict 1.
  Fail hammer.

(Incidentally, although hammer fails, Fail hammer also fails).

Fail predict 1:

Extracting features...

The command has indeed failed with message:
Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predict7b5c13fea /tmp/predict7b5c13dep /tmp/predict7b5c13seq -n 1 -p knn 2>/dev/null < /tmp/predict7b5c13conj > /tmp/coqhammer_outknn1b99e30

Fail hammer:

Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 128 -p nbayes 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outnbayes1280bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 1024 -p knn 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outknn10240bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 64 -p knn 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outknn640bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 256 -p knn 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outknn2560bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 64 -p nbayes 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outnbayes640bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 256 -p nbayes 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outnbayes2560bd166
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 64 -p nbayes 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outnbayes64cc5633
Error: Hammer error: Dependency prediction failed.
Prediction command: predict /tmp/predicta1a369fea /tmp/predicta1a369dep /tmp/predicta1a369seq -n 128 -p nbayes 2>/dev/null < /tmp/predicta1a369conj > /tmp/coqhammer_outnbayes128cc5633
The command has indeed failed with message:
Hammer failed: ATPs failed to find a proof.
You may try increasing the ATP time limit with 'Set Hammer ATPLimit N' (default: 20s).

I've certainly been able to run the examples before. Could this be a local issue? How could I debug this?

$ coqc --version
The Coq Proof Assistant, version 8.12.1 (February 2021)
compiled on Feb 17 2021 22:36:26 with OCaml 4.11.1
$ z3 --version
Z3 version 4.8.10 - 64 bit
$ cvc4 --version
This is CVC4 version 1.9-prerelease [git master 098cee0e (with modifications)]
compiled with GCC version 10.2.0
on Oct 22 2020 16:09:36

Thanks in advance.

Would be great with a proper GitHub release with support for CVC4 that can be included in Coq's OPAM. I can also confirm that current master works with the newly released Coq 8.8.2.

Hi @lukaszcz , would you be interested in adding coqhammer to Coq's CI?

See https://github.com/coq/coq/blob/master/dev/ci/README.md#information-for-external-library--plugin-authors

Let us know if you have any question.

Since Coq 8.11.0 is now out, any chance of a release (with a GitHub tarball) of CoqHammer that is compatible with that version? As before, I can take care of submitting an OPAM package for the Coq OPAM archive.

Require Import Hammer.Tactics.Tactics.
Require Import Hammer.Plugin.Hammer.

Section Test.

Variable P R : nat -> Prop.
Variable Q : nat -> nat -> Prop.

Axiom R_implies_P : forall x,
  R x ->
  P x.

Axiom P_Q_trans : forall x y,
  P x ->
  Q x y ->
  P y.

Lemma foo : R 0 -> Q 0 1 -> P 1.
Proof.
  intros.
  eapply P_Q_trans; only 2 : apply H0.
  Fail hammer.
(*The command has indeed failed with message:
  CoqHammer bug: please report: "Anomaly: grounding a non evar-free term" *)
Abort.

End Test.

The proof procedure introduces evars, but then unifies them before calling hammer. So I think the goal is evar-free by that time. Hopefully hammer can support this kind of goals.

I believe the coq8.10 branch is ready for a release that officially supports the recently-released Coq 8.10.0. While the Coq OPAM package is currently stuck as a pull request, I can submit new CoqHammer OPAM packages for a new release as soon as the Coq package is out.

When the hammer tactic in CoqHammer 1.2 for Coq 8.11 fails, it also reports an anomaly, as follows:

Error: Hammer failed: ATPs failed to find a proof
Error: Anomaly "Uncaught exception Failure("Hammer failed")." Please report at http://coq.inria.fr/bugs/.

This can be misleading to the user, since the "problem" is not in Coq and should not be reported as a bug. According to the Coq developers, the recommended way of handling exceptions (instead of leaving them uncaught) is to use CErrors.user_err.

Hi, the opam command to install the coq hammer is currently down

$ opam install coq-hammer

#=== ERROR while fetching sources for coq-hammer-tactics.1.3.2+8.15 ===========#
OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

#=== ERROR while fetching sources for coq-hammer.1.3.2+8.15 ===================#
OpamSolution.Fetch_fail("https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz (Bad checksum, expected sha512=0277150c2fd570400693ee1a3e4b2f253fbf7cc4b9997a803bb5e0e3e633352eb8cca2f3e8b1c47e49b9994b73c6f744f31e9e81eac665d1bf7ed4054ef39512)")

I visited the page https://github.com/lukaszcz/coqhammer/archive/v1.3.2-coq8.15.tar.gz and it returns an error:

the given path has multiple possibilities: #<Git::Ref:0x00007f6457d24f98>, #<Git::Ref:0x00007f6457cefa28>

I guess it's the reason why the opam failed, and it looks like some wrong configuration in the git repo.

Any chance for a branch (copy of current master) for Coq 8.10? Since Coq's v8.10 and master are starting to diverge a lot, it makes sense to split. I can do a pull request with CI and OPAM changes in the 8.10 branch.

I ran into several issues with Coq's builtin firstorder tactic, so I was very excited when I saw the documentation of coqhammer's sauto tactic: A general proof search tactic that allows me to specify which lemmas to use, which inductives to split on, which constructors to use, etc seems to be exactly the tool I was looking for.

So I tried it out on the following example (extracted to be standalone from a compiler correctness proof I'm working on):

From Hammer Require Import Hammer.
From Hammer Require Import Tactics.

Axiom K: Type.
Axiom V: Type.
Axiom map: Type.
Axiom get: map -> K -> option V.
(* in putmany m1 m2, keys of m2 override those of m1 *)
Axiom putmany: map -> map -> map.
(* `split m m1 m2` means that m can be split into two disjoint maps m1 and m2 *)
Axiom split : map -> map -> map -> Prop.

Axiom split_spec: forall (M A B: map),
    split M A B <-> forall k,
      (exists v, get M k = Some v /\
                 ((get A k = Some v /\ get B k = None) \/
                  (get B k = Some v /\ get A k = None))) \/
      (get M k = None /\ get A k = None /\ get B k = None).

Axiom putmany_spec: forall (m1 m2: map) k,
    (exists v, get (putmany m1 m2) k = Some v /\
               (get m2 k = Some v \/ (get m2 k = None /\ get m1 k = Some v))) \/
    (get (putmany m1 m2) k = None /\ get m2 k = None /\ get m1 k = None).

Goal forall m mKeep mGive frame m2 mL mStack,
    split m mKeep mGive ->
    split m2 m mL ->
    split mL mStack frame ->
    split m2 (putmany mKeep mL) mGive.
Proof.
  intros *. intros A1 A2 A3.
  pose proof (proj1 (split_spec _ _ _) A1) as B1.
  pose proof (proj1 (split_spec _ _ _) A2) as B2.
  pose proof (proj1 (split_spec _ _ _) A3) as B3.
  apply (proj2 (split_spec _ _ _)).
  clear A1 A2 A3.

  pose proof (putmany_spec mKeep mL) as B4.

  sauto inv: - ctrs: - cases: - ecases: off.

However, this sauto invocation does not return within 30s.

So I thought that maybe I'm not using the options correctly, and that the hammer plugin would tell me the right options to use, so I installed vampire and ran hammer:

Extracting features...
Running provers (8 threads)...
cvc4: No such file or directory
Error: Error running cvc4.
cvc4: No such file or directory
Error: Error running cvc4.
Error: Error running eprover.
Vampire (nbayes-64) succeeded
- dependencies: B4, B2, hammer_tests.putmany_spec, B1
Reconstructing the proof...
Trying reconstruction batch 1...
Trying reconstruction batch 2...
Trying reconstruction batch 3...
Trying reconstruction batch 4...
Trying reconstruction batch 5...
Trying reconstruction batch 6...
Trying reconstruction batch 7...

Error:
Hammer failed: proof reconstruction failed.
You may try increasing the reconstruction time limit with 'Set Hammer ReconstrLimit N' (default: 5s).
Other options are to disable the ATP which found this proof (Unset Hammer CVC4/Vampire/Eprover/Z3), or try to prove the goal manually using the displayed dependencies. Note that if the proof found by the ATP is inherently classical, it can never be reconstructed with CoqHammer's intuitionistic proof search procedure. As a last resort, you may also try enabling legacy reconstruction tactics with 'From Hammer Require Reconstr'.

... but the way it invoked proof reconstruction failed as well (after ~20s or so).

On the other hand, the following script solves the goal quite quickly, which makes me think that this goal is "not so hard":

  intro k.
  specialize (B1 k).
  specialize (B2 k).
  specialize (B3 k).
  specialize (B4 k).
  Time firstorder congruence. (* 0.61 secs *)
Qed.

• Is there a way to make sauto succeed on this goal?
• Do you have a recommended way of debugging proof reconstruction failures?

Coqhammer version: Latest commit (28200f8) on the coq8.11 branch
Coq version: 8.11.0

Coq version: Tested on 8.10, 8.11, possibly applicable to more
CoqHammer version: 1.3, not an issue on 1.2.1 (from Opam)
Operating System: Ubuntu 18.04.4
Interface: Coqtop, CoqIDE

@HazardousPeach and I use CoqHammer as part of our Coq theorem prover. We noticed after upgrading to hammer 1.3 we run into parsing errors.

Example:
Coq < From Hammer Require Import Hammer.
Coq < Lemma nat_eq (p q: nat): {p = q} + {p <> q}.
Toplevel input, characters 16-18:

Lemma nat_eq (p q: nat): {p = q} + {p <> q}.
_______________^^
Error:
Syntax error: ':=' or ':' or [Prim.name] expected after [Prim.name] (in [constr:closed_binder]).

This issue seems to only be present in 1.3. The bug It also appears to be magically tied to having the characters q and : appear sequentially without a space separating them. The lemma definition parses successfully if there's a space between the two characters. It also parses if hammer is not imported.

While compiling the CoqHammer master branch with Coq master with coq_makefile, I noticed the following warning:

CAMLOPT -c -for-pack Hammer_plugin src/plugin/g_hammer.ml
findlib: [WARNING] Interface partac.cmi occurs in several directories: ~/.opam/4.11.1.coqdev/lib/coq/stm, src/plugin
CAMLOPT -pack -o src/plugin/hammer_plugin.cmx
findlib: [WARNING] Interface partac.cmi occurs in several directories: ~/.opam/4.11.1.coqdev/lib/coq/stm, src/plugin
CAMLOPT -a -o src/plugin/hammer_plugin.cmxa
findlib: [WARNING] Interface partac.cmi occurs in several directories: ~/.opam/4.11.1.coqdev/lib/coq/stm, src/plugin
CAMLOPT -shared -o src/plugin/hammer_plugin.cmxs
findlib: [WARNING] Interface partac.cmi occurs in several directories: ~/.opam/4.11.1.coqdev/lib/coq/stm, src/plugin

The underlying cause is that Coq's master branch introduced a file stm/partac.ml, while CoqHammer already has src/plugin/partac.ml. The coq_makefile build seems to resolve the conflict properly, but when I tried to build with Dune, I get failures like this:

File "./theories/Plugin/Hammer.v", line 2, characters 0-34:
Error:
Dynlink error: The module `Partac' is already loaded (either by the main program or a previously-dynlinked library)

So coq_makefile is probably only getting lucky, and there may be more problems due to this clash in the future.

One solution is to rename the CoqHammer partac.ml file to something else - maybe hammer_partac.ml?

This is just to flag up that the v8.12 branch of Coq was recently created. If a corresponding branch (coq8.12) is created here, I can submit a pull request with the usual CI and OPAM changes.

On the topic of CI, I recommend switching the repo to use travis.com rather than travis.org. This will allow getting the clickable green checkmark symbol on commits on GitHub. For me, to convert a repo was as simple as going to the travis.com repo link, logging in via GitHub, and pressing a button.