From d10cf3a6da2673d652ca8dc8ee0aa04937d6a9af Mon Sep 17 00:00:00 2001 From: dianne Date: Thu, 25 Apr 2019 01:52:23 -0700 Subject: [PATCH] add some more high-level comments this also reorders the definitions in Reasoning.agda a bit for clarity --- Minesweeper/Board.agda | 3 + Minesweeper/Coords.agda | 2 + Minesweeper/Moves.agda | 16 +++- Minesweeper/Reasoning.agda | 170 +++++++++++++++++++------------------ Minesweeper/Rules.agda | 14 ++- 5 files changed, 113 insertions(+), 92 deletions(-) diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda index 2937ccd..7c725d5 100644 --- a/Minesweeper/Board.agda +++ b/Minesweeper/Board.agda @@ -18,6 +18,9 @@ open ≡-Reasoning open import Minesweeper.Enumeration as Enum using (Enumeration) open import Minesweeper.Coords hiding (_≟_) +-- Boards are 2D grids of tiles. they're parameterized over a type of tile, which we'll either instantiate with +-- `KnownTile` (when all tiles' identities are known) or `Tile` (when the board may have some unknown tiles). +-- for more about tiles, see Rules.agda and Moves.agda Board : Set → Bounds → Set Board A (w , h) = Vec (Vec A w) h diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda index 000e72c..4375c0d 100644 --- a/Minesweeper/Coords.agda +++ b/Minesweeper/Coords.agda @@ -17,9 +17,11 @@ open import Function open import Minesweeper.Enumeration as Enum using (Enumeration) +-- Bounds are board boundaries/dimensions Bounds : Set Bounds = ℕ × ℕ +-- Coords are coordinates on a board of a given size, used as a way to point to a specific tile. Coords : Bounds → Set Coords (w , h) = Fin w × Fin h diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index 0f4790e..a61a700 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -1,5 +1,7 @@ --- a hopefully-self-evident description of valid minesweeper moves --- and several lemmas about it +-- this module is dedicated to definitions and lemmas regarding partially known boards. importantly, we want to reason about when +-- an unknown tile will, when revealed, always be a mine or a safe tile. I refer to assigning guesses like that as "moves" and +-- call them "valid" when they will always hold, in reference to the actions of marking tiles as mines or revealing safe tiles +-- when playing minesweeper. module Minesweeper.Moves where @@ -31,11 +33,13 @@ open import Minesweeper.Coords as Coords open import Minesweeper.Board open import Minesweeper.Rules +-- Tile represents the tiles of a board that may have a mix of known and unknown tiles, like those in a game of minesweeper data Tile : Set where known : KnownTile → Tile unknown : Tile --- tile filling: an unknown tile can be filled with anything +-- tile filling: to relate filled and partial boards, we can fill in the tiles of a partial board to make a full board. +-- known tiles can only be "filled" with themselves, whereas unknown tiles can be filled with anything. data _↝▣_ : Tile → KnownTile → Set where ↝▣known : ∀ s → known s ↝▣ s ↝▣unknown : ∀ s → unknown ↝▣ s @@ -45,7 +49,11 @@ _↝⊞_ : ∀ {bounds} → Board Tile bounds → Board KnownTile bounds → Set _↝⊞_ = Pointwise _↝▣_ --- move validity: a guess as to a tile's identity on a board is valid when it holds in every rule-respecting way to fill the board's unfilled tiles +-- move validity: a guess as to a tile's identity on a board is valid when it holds in every rule-respecting way to fill the board's unfilled tiles. +-- here, "rule-respecting" means that we're only considering the filled boards where the numbers on the safe tiles match with the number of mines +-- adjacent to them. see Rules.agda for more details +-- in a game of minesweeper, a guess that a tile is safe or a mine being valid means that it definitely will be that. an invalid guess can still by +-- chance be right in a specific game you're playing, but there is some way of assigning the unknown tiles where you will be wrong. _[_]↝✓_ : ∀ {bounds} → Board Tile bounds → Coords bounds → Guess → Set grid [ coords ]↝✓ guess = ∀ grid′ → grid ↝⊞ grid′ → diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda index c97cf7e..bb7db5e 100644 --- a/Minesweeper/Reasoning.agda +++ b/Minesweeper/Reasoning.agda @@ -1,5 +1,6 @@ --- the goal of this module is to present inductive tools for reasoning about minesweeper, similar to the axioms ProofSweeper provides, --- and prove them sound and complete with respect to our formulation of minesweeper. +-- here, inspired by proofsweeper, we present inductive rules for describing valid minesweeper moves, and prove them +-- equivalent to the direct definition of move validity in Moves.agda. then, as a corollary, at the end of this module, +-- we prove that some principles closer to the rules used in proofsweeper also also sound. module Minesweeper.Reasoning where @@ -63,6 +64,7 @@ data _[_]↝★_ {bounds} grid coords where exfalso★ : ∀ guess → Contradiction grid → grid [ coords ]↝★ guess + -- let's do soundness first! -- roughly, this says that if you use the rules given by _[_]↝★_ to determine whether a tile is safe or a mine, -- it will indeed be that, for every possible way the unknown board tiles could be "filled in" @@ -105,8 +107,89 @@ data _[_]↝★_ {bounds} grid coords where +-- _[_]↝★_ is complete with respect to _[_]↝✓_ ! +-- roughly, this says that, given a partially filled board, and any tile on it that is either always safe or always a mine, +-- we can construct a proof that it always has that identity using only the rules given by _[_]↝★_ +✓⇒★ : ∀ {bounds} (grid : Board Tile bounds) coords guess → grid [ coords ]↝✓ guess → grid [ coords ]↝★ guess + +-- we proceed by induction on how "filled in" `grid` is. see the definition of _>_ in Minesweeper.Moves for more details +✓⇒★ {bounds} = >-rec _ ✓⇒★′ where + ✓⇒★′ : ∀ (grid : Board Tile bounds) → + (∀ filled → filled > grid → ∀ coords guess → filled [ coords ]↝✓ guess → filled [ coords ]↝★ guess) → + ∀ coords guess → grid [ coords ]↝✓ guess → grid [ coords ]↝★ guess + + -- through case analysis, we can exhaustively consider every possible choice until we've filled the entire board + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess with holey⊎filled grid + + -- if there's an unfilled tile left, we can apply the `cases★` rule to consider all possible ways of filling it + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₁ (unfilledCoords , unfilledCoords-unknown) = + cases★ unfilledCoords guess + λ tile → ✓⇒★-rec + (grid [ unfilledCoords ]≔ known tile) + (fill-> unfilledCoords grid tile unfilledCoords-unknown) + coords + guess + λ fullyFilled filled↝⊞fullyFilled fullyFilled✓ → coords↝✓guess + fullyFilled + (≥-↝⊞-trans (>⇒≥ (fill-> unfilledCoords grid tile unfilledCoords-unknown)) filled↝⊞fullyFilled) + fullyFilled✓ + + -- otherwise, `grid` is entirely filled. our assumption `coords↝✓guess` that `grid [ coords ]↝✓ guess` guarantees that + -- if there are no contradictions in `grid`, then we can find `guess` at `coords`. + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled with unwrap grid-filled ✓? + + -- in the case that `guess` can be found on `grid` at `coords`, we can use the `known★` rule + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | yes grid′✓ with coords↝✓guess (unwrap grid-filled) (↝⊞-unwrap grid-filled) grid′✓ + ... | guess⚐✓tile rewrite lookup∘unwrap grid-filled coords = + known★ (proj₁ (grid-filled coords)) guess (proj₂ (grid-filled coords)) guess⚐✓tile + + -- otherwise, there must be a contradiction somewhere on `grid`, so we can use the `exfalso★` rule + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | no ¬grid′✓ with identify-contradiction (unwrap grid-filled) ¬grid′✓ + ... | badCoords , ¬grid′[badCoords]✓ rewrite lookup∘unwrap grid-filled badCoords with grid-filled badCoords + + -- the contradiction can't be at a mine, since only safe tiles are considered when determining if a board is consistent + ... | mine , badCoords↦badTile = ⊥-elim (¬grid′[badCoords]✓ tt) + + -- at a safe tile reporting `n` neighboring mines, our assumption that there's a contradiction at that tile gives us that + -- there is *no* `Enumeration` of its neighboring mines with cardinality `n`. we can use this to build a `Contradiction` + -- in order to apply the `exfalso★` rule. + ... | safe n , badCoords↦badTile = + exfalso★ guess record + { coords = badCoords + ; supposedMineCount = n + ; coords-mineCount = badCoords↦badTile + ; neighborGuesses = neighborGuesses + ; neighborsKnown★ = λ i → + known★ + (proj₁ (neighbors-filled i)) + (neighborGuesses i) + (proj₂ (neighbors-filled i)) + (tileType-⚐✓ _) + ; disparity = n≢mineCount } + where + neighbors : Fin (Coords.neighborCount badCoords) → Coords bounds + neighbors = proj₁ ∘ (Inverse.to (Enumeration.lookup (Coords.neighbors badCoords)) ⟨$⟩_) + + neighbors-filled : ∀ i → ∃[ tile ] (lookup (neighbors i) grid ≡ known tile) + neighbors-filled = grid-filled ∘ neighbors + + neighborGuesses : Fin (Coords.neighborCount badCoords) → Guess + neighborGuesses = tileType ∘ proj₁ ∘ neighbors-filled + + mineCounts-agree : Enum.count (mine⚐ ≟⚐_) neighborGuesses ≡ cardinality (neighboringMines (unwrap grid-filled) badCoords) + mineCounts-agree = Enum.count-≡ _ _ _ _ (guesses-agree ∘ neighbors) where + guesses-agree : ∀ coords → mine⚐ ≡ tileType (proj₁ (grid-filled coords)) ⇔ mine⚐ ⚐✓ lookup coords (unwrap grid-filled) + guesses-agree coords rewrite lookup∘unwrap grid-filled coords with proj₁ (grid-filled coords) + ... | mine = equivalence (const ⚐✓mine) (const refl) + ... | safe _ = equivalence (λ ()) (λ ()) + + n≢mineCount : n ≢ Enum.count (mine⚐ ≟⚐_) neighborGuesses + n≢mineCount = ¬grid′[badCoords]✓ ∘ (neighboringMines (unwrap grid-filled) badCoords ,_) ∘ flip trans mineCounts-agree + + + -- now we'll also show that some familiar reasoning principles used in proofsweeper are sound --- (and thus as a corrollary of the completeness of `_[_]↝★_`, they can be expressed in terms of those rules). +-- (and thus as a corrollary of the completeness of `_[_]↝★_`, they can be expressed in terms of our inductive rules). -- specifically, we want to capture that if you have a known safe tile that already has as many adjacent safe -- tiles or mines as it can, then any other tile neighboring it must be of the other sort. for representing -- that conveniently, here's the following record: a given number of unique neighbors of a tile, all either @@ -209,84 +292,3 @@ otherNeighborIsMine grid neighborMineCount otherNeighbor ((safeCoords , safeCoor cardinality safeEnumeration + cardinality mineEnumeration ∸ cardinality mineEnumeration ≡⟨ m+n∸n≡m (cardinality safeEnumeration) (cardinality mineEnumeration) ⟩ cardinality safeEnumeration ∎ where open ≡-Reasoning - - - --- _[_]↝★_ is complete with respect to _[_]↝✓_ ! --- roughly, this says that, given a partially filled board, and any tile on it that is either always safe or always a mine, --- we can construct a proof that it always has that identity using only the rules given by _[_]↝★_ -✓⇒★ : ∀ {bounds} (grid : Board Tile bounds) coords guess → grid [ coords ]↝✓ guess → grid [ coords ]↝★ guess - --- we proceed by induction on how "filled in" `grid` is. see the definition of _>_ in Minesweeper.Moves for more details -✓⇒★ {bounds} = >-rec _ ✓⇒★′ where - ✓⇒★′ : ∀ (grid : Board Tile bounds) → - (∀ filled → filled > grid → ∀ coords guess → filled [ coords ]↝✓ guess → filled [ coords ]↝★ guess) → - ∀ coords guess → grid [ coords ]↝✓ guess → grid [ coords ]↝★ guess - - -- through case analysis, we can exhaustively consider every possible choice until we've filled the entire board - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess with holey⊎filled grid - - -- if there's an unfilled tile left, we can apply the `cases★` rule to consider all possible ways of filling it - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₁ (unfilledCoords , unfilledCoords-unknown) = - cases★ unfilledCoords guess - λ tile → ✓⇒★-rec - (grid [ unfilledCoords ]≔ known tile) - (fill-> unfilledCoords grid tile unfilledCoords-unknown) - coords - guess - λ fullyFilled filled↝⊞fullyFilled fullyFilled✓ → coords↝✓guess - fullyFilled - (≥-↝⊞-trans (>⇒≥ (fill-> unfilledCoords grid tile unfilledCoords-unknown)) filled↝⊞fullyFilled) - fullyFilled✓ - - -- otherwise, `grid` is entirely filled. our assumption `coords↝✓guess` that `grid [ coords ]↝✓ guess` guarantees that - -- if there are no contradictions in `grid`, then we can find `guess` at `coords`. - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled with unwrap grid-filled ✓? - - -- in the case that `guess` can be found on `grid` at `coords`, we can use the `known★` rule - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | yes grid′✓ with coords↝✓guess (unwrap grid-filled) (↝⊞-unwrap grid-filled) grid′✓ - ... | guess⚐✓tile rewrite lookup∘unwrap grid-filled coords = - known★ (proj₁ (grid-filled coords)) guess (proj₂ (grid-filled coords)) guess⚐✓tile - - -- otherwise, there must be a contradiction somewhere on `grid`, so we can use the `exfalso★` rule - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | no ¬grid′✓ with identify-contradiction (unwrap grid-filled) ¬grid′✓ - ... | badCoords , ¬grid′[badCoords]✓ rewrite lookup∘unwrap grid-filled badCoords with grid-filled badCoords - - -- the contradiction can't be at a mine, since only safe tiles are considered when determining if a board is consistent - ... | mine , badCoords↦badTile = ⊥-elim (¬grid′[badCoords]✓ tt) - - -- at a safe tile reporting `n` neighboring mines, our assumption that there's a contradiction at that tile gives us that - -- there is *no* `Enumeration` of its neighboring mines with cardinality `n`. we can use this to build a `Contradiction` - -- in order to apply the `exfalso★` rule. - ... | safe n , badCoords↦badTile = - exfalso★ guess record - { coords = badCoords - ; supposedMineCount = n - ; coords-mineCount = badCoords↦badTile - ; neighborGuesses = neighborGuesses - ; neighborsKnown★ = λ i → - known★ - (proj₁ (neighbors-filled i)) - (neighborGuesses i) - (proj₂ (neighbors-filled i)) - (tileType-⚐✓ _) - ; disparity = n≢mineCount } - where - neighbors : Fin (Coords.neighborCount badCoords) → Coords bounds - neighbors = proj₁ ∘ (Inverse.to (Enumeration.lookup (Coords.neighbors badCoords)) ⟨$⟩_) - - neighbors-filled : ∀ i → ∃[ tile ] (lookup (neighbors i) grid ≡ known tile) - neighbors-filled = grid-filled ∘ neighbors - - neighborGuesses : Fin (Coords.neighborCount badCoords) → Guess - neighborGuesses = tileType ∘ proj₁ ∘ neighbors-filled - - mineCounts-agree : Enum.count (mine⚐ ≟⚐_) neighborGuesses ≡ cardinality (neighboringMines (unwrap grid-filled) badCoords) - mineCounts-agree = Enum.count-≡ _ _ _ _ (guesses-agree ∘ neighbors) where - guesses-agree : ∀ coords → mine⚐ ≡ tileType (proj₁ (grid-filled coords)) ⇔ mine⚐ ⚐✓ lookup coords (unwrap grid-filled) - guesses-agree coords rewrite lookup∘unwrap grid-filled coords with proj₁ (grid-filled coords) - ... | mine = equivalence (const ⚐✓mine) (const refl) - ... | safe _ = equivalence (λ ()) (λ ()) - - n≢mineCount : n ≢ Enum.count (mine⚐ ≟⚐_) neighborGuesses - n≢mineCount = ¬grid′[badCoords]✓ ∘ (neighboringMines (unwrap grid-filled) badCoords ,_) ∘ flip trans mineCounts-agree diff --git a/Minesweeper/Rules.agda b/Minesweeper/Rules.agda index fe3812f..5751fca 100644 --- a/Minesweeper/Rules.agda +++ b/Minesweeper/Rules.agda @@ -1,4 +1,5 @@ --- the rules of filled minesweeper boards: do the numbers tell the truth? +-- here we describe the "rules" of minesweeper, +-- or what it means for the tiles of an entirely known board to be consistent with each other module Minesweeper.Rules where @@ -16,10 +17,15 @@ open import Minesweeper.Coords open import Minesweeper.Board open import Minesweeper.Enumeration as Enum using (Enumeration) +-- KnownTile represents the tiles of a completely filled board: +-- they're all either mines, or safe tiles labeled with how many mines there are adjacent to them data KnownTile : Set where mine : KnownTile safe : ℕ → KnownTile +-- Guess represents the type of a tile. the name is due to how they're used to reason about the identities of unknown tiles, +-- since a `safe⚐` guess could correspond to a safe tile `safe n` for any `n`. following the name, the "⚐" mnemonic is meant +-- to evoke placing flags over unknown tiles with mines in Windows minesweeper to mark them as such. data Guess : Set where mine⚐ : Guess safe⚐ : Guess @@ -30,14 +36,14 @@ data _⚐✓_ : Guess → KnownTile → Set where ⚐✓safe : ∀ n → safe⚐ ⚐✓ safe n --- a numbered tile is good if the number on it matches the number of mines adjacent to it. --- since all Enumerations of a type have the same length, it's sufficient to provide only one as evidence +-- consistency: `grid [ coords ]✓` means that if `grid` has a safe tile at `coords`, then the number on it agrees with the number of mines adjacent to it. +-- since only safe tiles are checked in this way, coordinates with mines are always regarded as valid, regardless of if they have adjacent inconsistent safe tiles. _[_]✓ : ∀ {bounds} → Board KnownTile bounds → Coords bounds → Set _[_]✓ {bounds} grid coords with lookup coords grid ... | mine = ⊤ ... | safe n = Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) ] n ≡ Enumeration.cardinality neighboringMines --- a board is good if all positions on it are good +-- a board `grid` is consistent (written `grid ✓`) if every tile on it is consistent with its neighbors _✓ : ∀ {bounds} → Board KnownTile bounds → Set _✓ {bounds} grid = ∀ coords → grid [ coords ]✓