make the definition of Neighboring more generic

this requires moving a few things around but it greatly simplifies further
developments

Minesweeper/Board.agda

@@ -15,5 +15,5 @@ lookup (x , y) grid = Vec.lookup x (Vec.lookup y grid)
 _[_]≔_ : ∀ {A bounds} → Board A bounds → Coords bounds → A → Board A bounds
 grid [ (x , y) ]≔ value = grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ value)
 
-_Neighboring_on_ : ∀ {A bounds} → A → Coords bounds → Board A bounds → Set
-tile Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] tile ≡ lookup (proj₁ neighbor) grid
+_Neighboring_on_ : ∀ {A bounds} → (A → Set) → Coords bounds → Board A bounds → Set
+P Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] P (lookup (proj₁ neighbor) grid)

Minesweeper/Moves.agda

@@ -10,10 +10,6 @@ data Tile : Set where
   known   : KnownTile → Tile
   unknown : Tile
 
-data Guess : Set where
-  mine⚐ : Guess
-  safe⚐ : Guess
-
 -- tile filling: an unknown tile can be filled with anything
 data _↝▣_ : Tile → KnownTile → Set where
   ↝▣known   : ∀ s → known s ↝▣ s
@@ -23,17 +19,13 @@ data _↝▣_ : Tile → KnownTile → Set where
 _↝⊞_ : ∀ {bounds} → Board Tile bounds → Board KnownTile bounds → Set
 holey ↝⊞ filled = ∀ coords → lookup coords holey ↝▣ lookup coords filled
 
--- guessing: is a guess of a tile's type valid for that tile?
-data _↝⚐_ : Guess → KnownTile → Set where
-  ↝⚐mine : mine⚐ ↝⚐ mine
-  ↝⚐safe : ∀ n → safe⚐ ↝⚐ safe n
 
 -- 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
 _[_]↝✓_ : ∀ {bounds} → Board Tile bounds → Coords bounds → Guess → Set
 grid [ coords ]↝✓ guess = ∀ grid′ →
   grid ↝⊞ grid′ →
   grid′ ✓ →
-    guess ↝⚐ lookup coords grid′
+    guess ⚐✓ lookup coords grid′
 
 -- solvable boards: a board is solvable when there is a rule-respecting way to fill its unfilled tiles
 record Solvable {bounds} (unsolved : Board Tile bounds) : Set where
@@ -45,5 +37,5 @@ record Solvable {bounds} (unsolved : Board Tile bounds) : Set where
 -- "play" a valid move on a solvable board, giving evidence that it holds in the provided solution
 play : ∀ {bounds grid} (coords : Coords bounds) {guess} →
   grid [ coords ]↝✓ guess → (solved : Solvable grid) →
-    guess ↝⚐ lookup coords (Solvable.solution solved)
+    guess ⚐✓ lookup coords (Solvable.solution solved)
 play coords move solved = move (Solvable.solution solved) (Solvable.relevance solved) (Solvable.validity solved)

Minesweeper/Reasoning.agda

@@ -36,18 +36,18 @@ Many_neighboring★_on_excluding_ guess neighbor grid exclude = Neighbors★ gri
 
 data _[_]↝★_ {bounds} grid coords where
   -- known tiles already have a proven identity
-  known★ : ∀ tile guess → lookup coords grid ≡ known tile → guess ↝⚐ tile → grid [ coords ]↝★ guess
+  known★ : ∀ tile guess → lookup coords grid ≡ known tile → guess ⚐✓ tile → grid [ coords ]↝★ guess
 
   -- a tile is safe if an adjacent safe tile already has as many adjacent mines as it can
   safe★ : ∀ neighborMineCount
-    (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid)
+    (safeNeighbor : (known (safe neighborMineCount) ≡_) Neighboring coords on grid)
     (neighborMines : Many mine⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) →
     List.length (Neighbors★.list neighborMines) ≡ neighborMineCount →
       grid [ coords ]↝★ safe⚐
 
   -- a tile is a mine if an adjacent safe tile already has as many adjacent safe tiles as it can
   mine★ : ∀ neighborMineCount
-    (safeNeighbor : known (safe neighborMineCount) Neighboring coords on grid)
+    (safeNeighbor : (known (safe neighborMineCount) ≡_) Neighboring coords on grid)
     (neighborSafes : Many safe⚐ neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords) →
     List.length (Neighbors★.list neighborSafes) + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeNeighbor)))) →
       grid [ coords ]↝★ mine⚐

Minesweeper/Rules.agda

@@ -7,8 +7,7 @@ open import Data.Product
 open import Data.Nat as ℕ using (ℕ)
 open import Data.List hiding (lookup)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Binary using () renaming (Decidable to Decidable₂)
-open import Relation.Unary  using () renaming (Decidable to Decidable₁)
+open import Relation.Binary
 open import Relation.Nullary
 
 open import Minesweeper.Coords
@@ -19,26 +18,42 @@ data KnownTile : Set where
   mine : KnownTile
   safe : ℕ → KnownTile
 
+data Guess : Set where
+  mine⚐ : Guess
+  safe⚐ : Guess
+
+-- guessing: is a guess of a tile's type valid for that tile?
+data _⚐✓_ : Guess → KnownTile → Set where
+  ⚐✓mine : mine⚐ ⚐✓ mine
+  ⚐✓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
 _[_]✓ : ∀ {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 ≡ length (Enumeration.list neighboringMines)
+... | safe n = Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) ] n ≡ length (Enumeration.list neighboringMines)
 
 -- a board is good if all positions on it are good
 _✓ : ∀ {bounds} → Board KnownTile bounds → Set
 _✓ {bounds} grid = ∀ coords → grid [ coords ]✓
 
 
-mine? : Decidable₁ (_≡_ mine)
-mine? mine     = yes refl
-mine? (safe _) = no  λ { () }
+_⚐✓?_ : Decidable (_⚐✓_)
+mine⚐ ⚐✓? mine   = yes ⚐✓mine
+mine⚐ ⚐✓? safe _ = no λ { () }
+safe⚐ ⚐✓? mine   = no λ { () }
+safe⚐ ⚐✓? safe n = yes (⚐✓safe n)
+
+⚐✓-irrelevance : Irrelevant _⚐✓_
+⚐✓-irrelevance ⚐✓mine     ⚐✓mine      = refl
+⚐✓-irrelevance (⚐✓safe n) (⚐✓safe .n) = refl
 
-neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords bounds) → Enumeration (mine Neighboring coords on grid)
-neighboringMines grid coords = Enum.filter ≡-irrelevance (λ { (neighbor , _) → mine? (lookup neighbor grid) }) (neighbors coords)
+neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords bounds) → Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid)
+neighboringMines grid coords = Enum.filter ⚐✓-irrelevance (λ { (neighbor , _) → mine⚐ ⚐✓? (lookup neighbor grid) }) (neighbors coords)
 
-_[_]✓? : ∀ {bounds} → Decidable₂ (_[_]✓ {bounds})
+_[_]✓? : ∀ {bounds} → Decidable (_[_]✓ {bounds})
 _[_]✓? {bounds} grid coords with lookup coords grid
 ... | mine = yes tt
 ... | safe n with n ℕ.≟ length (Enumeration.list (neighboringMines grid coords))