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

[sakekasi]

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:

1. prove the current goal in its entirety
2. 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]

This is a bug. The reconstruction tactics should either fail or succeed, never leaving any subgoals behind. Perhaps this is due to some changes in more recent versions of Coq. CoqHammer was originally written in 2018, and I haven't actively worked on it since 2021, only maintaining.

As a workaround, you can try wrapping up the reconstruction tactics in some combination of solve (https://coq.inria.fr/doc/V8.19.0/refman/proof-engine/ltac.html#coq:tacn.solve) and unshelve. I already did that, but maybe something needs to change there.