"Qed." takes a long time

I am writing a chess program in Coq and encountered a strange problem. The “Qed.” command after one of my proofs seemed not to terminate. The proof itself is ok (all green in CoqIDE).

I simplified the code to isolate the problem and found that the time it takes for the “Qed.” to finish depends on the size of the chess board. If the board is 4x4, it takes a few seconds. If the board is 5x5, it takes 16 minutes. How long it would take for the actual code with an 8x8 board I couldn’t begin to imagine. I used Coq version 8.15.2.

If anyone wants to take a look at the code, here are the two versions for a 4x4 and a 5x5 board:

The entry for the Qed command in the manual cautions that “one may have to wait a while when the proof is large”, but my proof is rather simple.

Any hints as to what causes this behavior and what I might do to solve the problem would be greatly appreciated.

It has trouble rechecking the first unfold find_king in * (which is doing find_kind in H)
Indeed if you do

Lemma find_king_correct : forall pp c king_rank king_file,
  In (Loc king_rank king_file) (find_king pp c) <->
  (location_valid (Loc king_rank king_file)) /\
  (get_square_by_index pp king_rank king_file =
  Occupied c King).
Proof.
  intros pp c king_rank king_file. split.
  - unfold find_king;intro H. apply find_piece_correct in H. HdAnd. split; auto.
    apply valid_squares_suf in H. auto.
  - intro H;unfold find_king. HdAnd. apply valid_squares_nec in H.
    apply find_piece_correct. split; auto.
Qed.

(intro H after the unfold in the first bullet) then it is fast, but if you do


Lemma find_king_correct : forall pp c king_rank king_file,
  In (Loc king_rank king_file) (find_king pp c) <->
  (location_valid (Loc king_rank king_file)) /\
  (get_square_by_index pp king_rank king_file =
  Occupied c King).
Proof.
  intros pp c king_rank king_file. split.
  - intro H;unfold find_king in H. apply find_piece_correct in H. HdAnd. split; auto.
    apply valid_squares_suf in H. auto.
  - intro H;unfold find_king. HdAnd. apply valid_squares_nec in H.
    apply find_piece_correct. split; auto.
Qed.

(intro H before unfold in the first bullet) then it is slow.
This is because unfold inserts a trace of the goal change in the produced term, but there is no trace when unfolding in an hypothesis.

Specifically it needs to do


Check
  fun (pp : PiecePlacements) (c : Color)
    (king_rank king_file : nat)
    (H : @In SquareLocation (Loc king_rank king_file)
             (find_king pp c))
  =>
    (H : (@In SquareLocation (Loc king_rank king_file)
              (find_piece pp c King valid_locations))).

which is slow. It compares find_king ... and find_piece ... valid_locations, and decides to unfold find_piece (and then valid_locations) first. This is a mistake as the size of the unfolded find_piece ... valid_locations is about 2^(n^2): find_piece looks like

Fixpoint find_piece ... locations := match locations with 
| [] -> []
| elt :: rest -> if cond then elt :: find_piece ... rest else find_piece ... rest
end

and we are not unfolding the cond (they are on variables so unfolding it won’t pick a side).

So these ways make this work:

  • delay the intro until after the unfold: the unfold trace makes Qed check the conversion in the opposite order so it unfolds find_king first and finds out that it’s convertible quickly
  • put Strategy expand [find_king]. which makes conversion always unfold find_king first
  • put Strategy opaque [valid_locations]. (which is where the n^2 part appears) so that valid_locations is unfolded last
  • define valid_locations using combinators, eg Definition valid_locations := concat (map (fun l => map (fun r => Loc l r) (seq 0 5)) (seq 0 5)). (for the 5x5 case), this allows unfolding to be less eager

Thank you very much. Even the original 8x8 case works instantly when I unfold first and introduce the hypothesis afterward.

I am not quite sure I understand the cause completely. I guess I need to be wary of unfolding in hypotheses. Couldn’t Coq keep track of unfolds in hypotheses in the same way it does for unfolds in the goal?

The way it keeps track of unfolds in the goal is by doing refine (_ : OLD GOAL), you can see eg if you do
unfold find_king (without having introd) then Show Proof says

(fun (pp : PiecePlacements) (c : Color) (king_rank king_file : nat) =>
 conj
   (?Goal0
    :
    In (Loc king_rank king_file) (find_king pp c) ->
    location_valid (Loc king_rank king_file) /\
    get_square_by_index pp king_rank king_file = Occupied c King) ?Goal)

then if you intro H Show Proof says

(fun (pp : PiecePlacements) (c : Color) (king_rank king_file : nat) =>
 conj
   ((fun H : In (Loc king_rank king_file) (find_piece pp c King valid_locations) => ?Goal0)
    :
    In (Loc king_rank king_file) (find_king pp c) ->
    location_valid (Loc king_rank king_file) /\
    get_square_by_index pp king_rank king_file = Occupied c King) ?Goal)

The fun H has the unfolded type.

I guess @SkySkimmer 's answer means Coq cannot do that in exactly the same way; but (EDIT) it seems unfold foo in H could be implemented as revert H; unfold foo at <occurrences in H>; intro H, aka
refine (((fun H : new_type) => _) : OLD GOAL) H. Is there some blocker to that? The usual backward compatibility questions don’t seem huge here…