Add verified Connect Four with alpha-beta AI

[CharlesCNorton]

Summary

Formalizes Connect Four as a two-player game over a 7×6 board with gravity, following the same patterns as TicTacToe.v. The complete game tree (~4.5 trillion nodes) is defined via well-founded recursion on empty slots, proving finiteness. Execution uses depth-limited cotree search with alpha-beta pruning from AlphaBeta.v.

Game model

• Board: 7 columns as list player (bottom-to-top), gravity = append
• Win detection: 69 lines of four (24 horizontal + 21 vertical + 12 diagonal-up + 12 diagonal-down)
• Moves: filter over columns with height < 6; game halts on win/draw
• Decidable equality on all game types

Verified properties

Theorem	Statement
all_lines_sound	Every entry in all_lines is geometrically valid
all_lines_complete	Every in-bounds line of four appears in all_lines
all_lines_NoDup	No duplicate entries
has_won_correct	has_won b p = true iff ∃ a valid winning line with all four cells occupied by p
valid_moves	Every move in moves g satisfies valid_move
moves_complete	Every valid_move appears in moves g
valid_board_apply_move	Column height invariant (≤ 6) preserved by legal moves
complete_tree_sound	Every node in the game tree is reachable from the initial position
complete_tree_complete	Every reachable position appears in the game tree
at_most_one_winner	On any reachable board, it is impossible for both players to have four in a row simultaneously
c4_eval_ab_correct	Alpha-beta pruning returns the same value as unpruned minimax (eval_ab_correct instantiation)
ai_subtree_reachable	Every node examined by the AI is reachable via valid game steps

Execution

• Depth-7 search via Cotrees.unfold_cotree + tree_of_cotree, rebuilt from current position each AI turn
• AI scores children via eval_ab players_le_ge, picks optimal move
• Interactive terminal play loop with print_board, read_line, column input (1–7)
• OCaml extraction; make c4 runs the game

Library reuse

Component	Source
tree, unfold_tree, In_tree, root, children	Trees.v
unfold_cotree, tree_of_cotree, colist_of_list	Cotrees.v
eval_ab, players_le_ge	AlphaBeta.v
max, comparing	Eval.v
IO, SimpleIO, extraction setup	TicTacToe.v pattern

Test plan

• make compiles all files including ConnectFour.v (Rocq 9.0)
• No existing files modified (one Makefile convenience target added)
• Extraction produces connectfour.ml; make c4 runs the interactive game