From d30a6fc71fe8f67d7a77cb6794d4cf38bc98ca9b Mon Sep 17 00:00:00 2001 From: dianne Date: Fri, 2 Aug 2019 13:40:41 -0700 Subject: [PATCH] add a readme! (rough draft) I'm planning on doing another pass over it and the comments, but it's a start! --- README.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..16b7ad8 --- /dev/null +++ b/README.md @@ -0,0 +1,18 @@ +About Minesweeper.Reasoning +=========================== + +Minesweeper.Reasoning is an Agda module providing a formal description of the game +[Minesweeper](https://en.wikipedia.org/wiki/Minesweeper_(video_game)) and proofs about it, inspired by +[ProofSweeper](https://github.com/A1kmm/proofsweeper/). In ProofSweeper, you play Minesweeper by formally proving in Idris that +cells are or aren't mines, using some provided axioms, rather than simply clicking to uncover them. +My goal with Minesweeper.Reasoning is to prove that those axioms are sound (if you use them to prove that a cell is or isn't +a mine, that will always be the case) and complete (if a cell is always or never a mine, you can prove it with those axioms). + +These proofs are found in `Minesweeper/Reasoning.agda`. The formalization of Minesweeper is split across the remaining modules; +of note, `Minesweeper/Rules.agda` and `Minesweeper/Moves.agda` contain the main definitions, along with some useful lemmas. + +Dependencies +============ + +Minesweeper.Reasoning was checked against [Agda v2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1) +and requires [agda-stdlib v1.1](https://github.com/agda/agda-stdlib/releases/tag/v1.1).