add some more high-level comments

this also reorders the definitions in Reasoning.agda a bit for clarity
dianne · Apr 25, 2019 · d10cf3a · d10cf3a
1 parent d7c9d3f
commit d10cf3a
Show file tree

Hide file tree

Showing 5 changed files with 113 additions and 92 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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 ]✓