qauto breaks goal into multiple subgoals instead of solving or failing.

I'm trying to run an evaluation of how many proofs coqhammer can solve in the coq_wigderson project. To do this, I'm running the hammer tactic from coq-serapi, using coq 8.13. Running hammer on the lemma nbd_2_colorable_3 (in the file 'coloring.v' on line 232) succeeds with the reconstruction tactic qauto use: PositiveMap.gss, WP.F.not_find_in_iff, WP.F.not_mem_in_iff, WF.mem_find_b, WP.F..

However, instead of solving the goal it was run on, running this tactic takes me from this proof state:

---
(1/1)
forall (g : graph) (f : coloring) (p : colors),
coloring_complete p g f ->
three_coloring f p ->
forall (v : M.key) (ci : node),
M.find v f = Some ci ->
two_coloring (restrict_on_nbd f g v) (S.remove ci p) /\
coloring_complete (S.remove ci p) (neighborhood g v) (restrict_on_nbd f g v)

to this one

H3: forall (elt : Type) (m : M.t elt) (x y : M.key),
     x = y -> M.mem y (M.remove x m) = false
H2: forall (elt : Type) (m : M.t elt) (x : M.key),
     M.mem x m = (if M.find x m then true else false)
H: forall (A : Type) (i : PositiveMap.key) (x : A) (m : PositiveMap.t A),
    PositiveMap.find i (PositiveMap.add i x m) = Some x
g: graph
f: M.t node
p: colors
H6: three_coloring f p
v: M.key
ci: node
H7: M.find v f = Some ci
H0: forall (elt : Type) (m : M.t elt) (x : M.key),
     M.find x m = None -> M.In x m -> False
H8: forall (elt : Type) (m : M.t elt) (x : M.key),
     (M.In x m -> False) -> M.find x m = None
H1: forall (elt : Type) (m : M.t elt) (x : M.key),
     M.mem x m = false -> M.In x m -> False
H9: forall (elt : Type) (m : M.t elt) (x : M.key),
     (M.In x m -> False) -> M.mem x m = false
H10: forall (elt : Type) (m : M.t elt) (x y : M.key) (e : elt),
      M.In y m -> M.In y (M.add x e m)
H11: forall (elt : Type) (m : M.t elt) (x y : M.key) (e : elt),
      x = y -> M.In y (M.add x e m)
H4: forall (elt : Type) (m : M.t elt) (x y : M.key) (e : elt),
     M.In y (M.add x e m) -> x = y \/ M.In y m
H12: forall i : M.key, M.In i g -> M.In i f
H13: coloring_ok p g f
---
(1/3)
two_coloring (restrict_on_nbd f g v) (S.remove ci p)
---
(2/3)
M.In i (restrict_on_nbd f g v)
---
(3/3)
coloring_ok (S.remove ci p) (neighborhood g v) (restrict_on_nbd f g v)

I expected hammer and its reconstruction tactics to do one of 2 things:

prove the current goal in its entirety
give me an error

I'm a little surprised to find that the qauto tactic does neither of these things. Is this a bug in the tactic, or intended behavior?

Thanks for your help!

lukaszcz / coqhammer

qauto breaks goal into multiple subgoals instead of solving or failing. #183