Add verified Reversi with alpha-beta AI

[CharlesCNorton]

Summary

Formalizes Reversi (Othello) as a two-player game on an 8×8 board with standard placement and flipping rules, following the same patterns as TicTacToe.v and ConnectFour.v. The complete game tree is defined via well-founded recursion on a lexicographic measure (empty cells × pass count), proving finiteness. Execution uses depth-limited cotree search with alpha-beta pruning from AlphaBeta.v.

Game model

• Board: 64-cell list (row-major), index = row × 8 + col
• Moves: Place at (row, col) flipping opponent pieces in all 8 directions, or pass when no valid placement exists
• Win detection: Piece counting after two consecutive passes or full board
• Flipping: find_flips walks each direction accumulating opponents until a friendly bookend; all_flips aggregates across all 8 directions
• Decidable equality on all game types

Verified properties

Theorem	Statement
valid_moves	Every move in moves g satisfies valid_move
moves_complete	Every valid_move appears in moves g
apply_move_length	Board length invariant (= 64) preserved by legal moves
place_decreases_empty	Every placement strictly decreases empty cell count
all_flips_occupied	Every position returned by all_flips is occupied (not empty)
all_flips_in_bounds	Every flipped position is within board bounds
apply_flips_preserves_empty	Flipping occupied cells does not change empty count
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	get_result cannot simultaneously return both won_by black and won_by white
result_deterministic	get_result is a function (unique output)
reversi_eval_ab_correct	Alpha-beta pruning returns the same value as unpruned minimax
eval_ab_co_correct	Lazy cotree alpha-beta equals eager tree alpha-beta on materialized trees
eval_ab_co_minimax	Lazy cotree alpha-beta equals unpruned minimax
ai_subtree_reachable	Every node examined by the AI is reachable via valid game steps
full_board_no_moves	A full board produces no moves
double_pass_no_moves	Two consecutive passes end the game

Execution

• Depth-5 search via Cotrees.unfold_cotree + tree_of_cotree, rebuilt from current position each AI turn
• Lazy eval_ab_co operates directly on cotrees, avoiding full tree materialization
• AI scores children via eval_ab players_le_ge, picks optimal move
• Interactive terminal play loop with print_board, row/col input (0–7)
• OCaml extraction; make reversi runs the game

Library reuse

Component	Source
tree, unfold_tree, In_tree, root, children	Trees.v
unfold_cotree, tree_of_cotree, colist_of_list, cotree, colist	Cotrees.v
eval_ab, eval_val, players_le_ge, players_le_ge_strong, players_le_ge_adversarial	AlphaBeta.v
max, comparing	Eval.v
reachable, step	Relations.v
IO, SimpleIO, extraction setup	TicTacToe.v pattern

Test plan

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