a couple lemmas to beautify the soundness proof

Minesweeper/Moves.agda

@@ -1,10 +1,12 @@
 -- a hopefully-self-evident description of valid minesweeper moves
+-- and several lemmas about it
 
 module Minesweeper.Moves where
 
 open import Data.Empty
 open import Data.Product
 open import Data.Sum
+import      Data.List as List
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
 open import Data.Vec.Relation.Unary.Any as Any using (Any; any)
 import      Data.Vec.Relation.Unary.Any.Properties as AnyProp
@@ -24,6 +26,7 @@ open import Induction.WellFounded as WF
 open import Induction.Nat using (<-wellFounded)
 open import Function
 
+open import Minesweeper.Enumeration using (Enumeration)
 open import Minesweeper.Coords as Coords
 open import Minesweeper.Board
 open import Minesweeper.Rules
@@ -73,11 +76,24 @@ invert⚐ safe⚐ = mine⚐
 ¬-⚐✓-invert {safe⚐} {mine}   ¬guess⚐✓tile = ⚐✓mine
 ¬-⚐✓-invert {safe⚐} {safe n} ¬guess⚐✓tile = ⊥-elim (¬guess⚐✓tile (⚐✓safe n))
 
-
 unknown? : Decidable₁ (unknown ≡_)
 unknown? (known s) = no λ ()
 unknown? unknown   = yes refl
 
+-- if a tile is already known, it can only be filled that way.
+-- usually when we know a tile is known it's from a separate equality such as `known tile ≡ lookup coords grid`,
+-- so this is specialized to account for that case
+known-↝▣⇒≡ : ∀ {tile knowntile knowntile′} → tile ≡ known knowntile → tile ↝▣ knowntile′ → knowntile ≡ knowntile′
+known-↝▣⇒≡ refl (↝▣known _) = refl
+
+-- if a tile is specifically known to be safe with `n` adjacent mines on a consistent board `grid′`, we can go further:
+-- `grid′ ✓` gives us an Enumeration of that tile's neighboring mines with exactly `n` members.
+-- that is, on `grid′` it indeed does have `n` adjacent mines
+known-safe-✓ : ∀ {bounds} (coords : Coords bounds) grid grid′ {n} → lookup coords grid ≡ known (safe n) → grid ↝⊞ grid′ → grid′ ✓ →
+  Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid′) ] n ≡ List.length (Enumeration.list neighboringMines)
+known-safe-✓ coords grid grid′ coords↦safe grid↝⊞grid′ grid′✓ with grid′✓ coords
+...                                                              | grid′[coords]✓ rewrite sym (known-↝▣⇒≡ coords↦safe (grid↝⊞grid′ coords)) = grid′[coords]✓
+
 
 -- specificity: a partially filled board is more specific than another if it agrees on all known tiles
 -- and has strictly more tiles known. this is helpful in writing inductive proofs as it is well-founded:

Minesweeper/Reasoning.agda

@@ -100,9 +100,7 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord
 
 -- when the tile we're looking at is already known, it will stay the same in all ways of completing the board.
 -- so as long as our guess agrees with its current state, it's valid
-★⇒✓ grid coords (known★ tile guess coords↦tile guess⚐✓tile) grid′ grid↝⊞grid′ grid′✓ with grid↝⊞grid′ coords
-...                                                                                     | tile↝▣tile′   with lookup coords grid | lookup coords grid′
-★⇒✓ grid coords (known★ tile guess refl        guess⚐✓tile) grid′ grid↝⊞grid′ grid′✓    | ↝▣known .tile    | .(known tile)      | .tile = guess⚐✓tile
+★⇒✓ grid coords (known★ tile guess coords↦tile guess⚐✓tile) grid′ grid↝⊞grid′ grid′✓ = subst (guess ⚐✓_) (known-↝▣⇒≡ coords↦tile (grid↝⊞grid′ coords)) guess⚐✓tile
 
 -- for a proof by cases★ on the final board, only the case that applies to our actual final board `grid′` applies
 ★⇒✓ grid coords (cases★ testCoords guess cases) grid′ grid↝⊞grid′ grid′✓ = ★⇒✓ _ _ (cases (lookup testCoords grid′)) grid′ gridWithTest↝⊞grid′ grid′✓ where
@@ -137,28 +135,23 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord
   mineCountsConsistent                      (_ ∷ neighbors↝★guesses) | no ¬mine⚐✓tile | ⚐✓safe .n      | .(safe n)             | ⚐✓safe n = mineCountsConsistent neighbors↝★guesses
 
   testCoords-mineCount✓ : supposedMineCount ≡ List.length (Enumeration.list (neighboringMines grid′ testCoords))
-  testCoords-mineCount✓ with grid↝⊞grid′ testCoords | grid′✓ testCoords
-  ...                      | tile↝▣tile             | testCoords✓ rewrite testCoords-mineCount with lookup testCoords grid′
-  testCoords-mineCount✓    | ↝▣known _              | mines′ , supposedMineCount≡length-mines′ | _ =
+  testCoords-mineCount✓ with known-safe-✓ testCoords grid grid′ testCoords-mineCount grid↝⊞grid′ grid′✓
+  ... | mines′ , supposedMineCount≡length-mines′ =
     trans supposedMineCount≡length-mines′ (Enum.enumeration-length-uniform mines′ (neighboringMines grid′ testCoords))
 
 -- a tile being safe★ means it has an adjacent safe tile with as many adjacent mines as it can have, so by `Neighbors★-alreadyFull` it must be safe
 ★⇒✓ grid coords (safe★ neighborMineCount ((safeNeighbor , safeNeighbor-Adj) , safeNeighbor-safe) neighborMines neighborMines-length) grid′ grid↝⊞grid′ grid′✓
-  with grid↝⊞grid′ safeNeighbor | grid′✓ safeNeighbor
-...  | safe↝⊞safe               | safeNeighbor✓                               with lookup safeNeighbor grid | lookup safeNeighbor grid′
-★⇒✓ grid coords (safe★ neighborMineCount ((safeNeighbor , safeNeighbor-Adj) , refl) neighborMines neighborMines-length) grid′ grid↝⊞grid′ grid′✓
-     | ↝▣known .(safe _)        | mineEnumeration , neighborMineCount≡enumLength | .(known (safe _))        | .(safe _) =
+  with known-safe-✓ safeNeighbor grid grid′ (sym safeNeighbor-safe) grid↝⊞grid′ grid′✓
+... | mineEnumeration , neighborMineCount≡enumLength =
   Neighbors★-alreadyFull grid grid′ safeNeighbor (coords , Coords.Adjacent-sym coords safeNeighbor safeNeighbor-Adj) mine⚐ neighborMines mineEnumeration grid↝⊞grid′ grid′✓ enoughMines
   where
     enoughMines : List.length (Neighbors★.list neighborMines) ≡ List.length (Enumeration.list mineEnumeration)
     enoughMines = trans neighborMines-length neighborMineCount≡enumLength
 
 -- a tile being a mine★ means it has an adjacent safe tile with as many adjacent safe tiles as it can have, so by `Neighbors★-alreadyFull` it must be a mine
 ★⇒✓ grid coords (mine★ neighborMineCount ((safeNeighbor , safeNeighbor-Adj) , safeNeighbor-safe) neighborSafes neighborSafes-length) grid′ grid↝⊞grid′ grid′✓
-  with grid↝⊞grid′ safeNeighbor | grid′✓ safeNeighbor
-...  | safe↝⊞safe               | safeNeighbor✓                               with lookup safeNeighbor grid | lookup safeNeighbor grid′
-★⇒✓ grid coords (mine★ neighborMineCount ((safeNeighbor , safeNeighbor-Adj) , refl) neighborSafes neighborSafes-length) grid′ grid↝⊞grid′ grid′✓
-     | ↝▣known .(safe _)        | mineEnumeration , neighborMineCount≡enumLength | .(known (safe _))        | .(safe _) =
+  with known-safe-✓ safeNeighbor grid grid′ (sym safeNeighbor-safe) grid↝⊞grid′ grid′✓
+... | mineEnumeration , neighborMineCount≡enumLength =
   Neighbors★-alreadyFull grid grid′ safeNeighbor (coords , Coords.Adjacent-sym coords safeNeighbor safeNeighbor-Adj) safe⚐ neighborSafes safeEnumeration grid↝⊞grid′ grid′✓ enoughSafes
   where
     -- since the number of safe neighbors a tile has is defined by how many are left when you take away the mines,