This repository contains functions and proofs about game trees in Rocq, implemented as rose trees. We provide two different flavors of game trees, inductive and coinductive game trees. Inductive game trees are finite by construction, but it is difficult to populate a tree from an initial value and a function that gives the next steps. We have to prove that the population (anamorphism or unfolding of a rose tree) terminates. Coinductive game trees can be infinite or finite. Populating a coinductive tree is easy since we do not have to prove termination, but we need bisimulation to reason about them.
In GameTrees.Trees.Unfold, we provide an unfold_tree function that populates an inductive tree in a provably terminating way, if you abide by certain restrictions about what the next function says the next steps will be. We prove that this function is sound and complete: a value is in the game tree if and only if there is a sequence of applications of next from the initial state that create that value.
In GameTrees.Cotrees.Unfold, we provide an unfold_cotree function that populates a possibly infinite tree. We prove that this function is also sound and complete.
To showcase our library, we provide an example: a tic-tac-toe game for which we unfold a proven-complete game tree and run minimax algorithm to implement an unbeatable AI.
You have to have the rocq-released registry of opam. You can obtain it by running opam repo add rocq-released https://rocq-prover.org/opam/released if you do not already have it.
To install the dependencies, run opam install . --deps-only. The project builds with Rocq 9.0.0 or higher.
To build the project use make. After that, you can optionally run the tic-tac-toe game with make run.
To install the project use opam install .. You do not need the make step from the build instructions for this.
We ❤️ contributions.
Have you had a good experience with this project? Why not share some love and contribute code, or just let us know about any issues you had with it?
We welcome issue reports here; be sure to choose the proper issue template for your issue, so that we can be sure you're providing the necessary information.
Before sending a Pull Request, please make sure you read our Contribution Guidelines.
Please read the LICENSE file.
This project has adopted a Code of Conduct. If you have any concerns about the Code, or behavior which you have experienced in the project, please contact us at [email protected].