rewrite Enumeration

now, instead of defining Enumeration--a collection of all unique elements of a
type--as a list of all of its elements (unique up to propositional equality),
it is a bijection between a finite set and its elements (up to a provided
equivalence). mostly, I think this makes things nicer! it allows for expressing
more things in terms of standard library functions, and simplifies a few
others, but some did need extra work to transfer over, and overall it was a big
rewrite. I want this to look as presentable as I can make it, though, so I think
it's worth it.

Minesweeper/Board.agda

@@ -9,10 +9,13 @@ open import Data.Product
 open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡)
 open import Function
 open import Relation.Nullary
-open import Relation.Binary
+open import Relation.Unary  using  (Decidable)
+open import Relation.Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality
+import Relation.Binary.Construct.On as On
 open ≡-Reasoning
 
+open import Minesweeper.Enumeration as Enum using (Enumeration)
 open import Minesweeper.Coords hiding (_≟_)
 
 Board : Set → Bounds → Set
@@ -24,8 +27,18 @@ 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 = Vec.updateAt y (Vec._[ x ]≔ value) 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)
+-- `P Neighboring coords on grid` are the adjacent tiles to `coords` that satisfy the predicate `P`:
+-- a `Neighbor coords` paired with a proof that its coordinates, when looked up on `grid`, satisfy `P`.
+-- we don't compare the proofs for equality, so we define their setoid equality as equality on the Neighbors
+_Neighboring_on_ : ∀ {p A bounds} → (A → Set p) → Coords bounds → Board A bounds → Setoid _ _
+P Neighboring coords on grid = On.setoid
+  {B = Σ[ neighbor ∈ Setoid.Carrier (Neighbor coords) ] P (lookup (proj₁ neighbor) grid)}
+  (Neighbor coords)
+  proj₁
+
+-- in order to get the neighbors of some coords satisfying P, we can filter all of its neighbors to just the ones satisfying P
+filterNeighbors : ∀ {p A bounds} {P : A → Set p} (P? : Decidable P) (grid : Board A bounds) (coords : Coords bounds) → Enumeration (P Neighboring coords on grid)
+filterNeighbors {P = P} P? grid coords = Enum.filter (P? ∘ flip lookup grid ∘ proj₁) (subst (P ∘ flip lookup grid) ∘ ≡×≡⇒≡) (neighbors coords)
 
 
 Pointwise : ∀ {ℓ A B} (_∼_ : REL A B ℓ) {bounds} → REL (Board A bounds) (Board B bounds) _

Minesweeper/Coords.agda

@@ -4,15 +4,15 @@ open import Data.Nat renaming (_≟_ to _ℕ≟_)
 open import Data.Integer using (∣_∣; _⊖_)
 open import Data.Integer.Properties using (∣m⊖n∣≡∣n⊖m∣)
 open import Data.Product
-open import Data.Product.Relation.Pointwise.NonDependent using (≡?×≡?⇒≡?)
+open import Data.Product.Relation.Pointwise.NonDependent using (×-setoid; ≡×≡⇒≡; ≡?×≡?⇒≡?)
 open import Data.Fin renaming (_≟_ to _Fin≟_)
 import      Data.Fin.Properties as Fin
 open import Relation.Nullary
 import      Relation.Nullary.Decidable as Dec
-open import Relation.Unary  using () renaming (Decidable to Decidable₁)
-open import Relation.Binary using () renaming (Decidable to Decidable₂)
+open import Relation.Unary  using ()       renaming (Decidable to Decidable₁)
+open import Relation.Binary using (Setoid) renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality
-open import Relation.Binary.PropositionalEquality.WithK
+import      Relation.Binary.Construct.On as On
 open import Function
 
 open import Minesweeper.Enumeration as Enum using (Enumeration)
@@ -29,11 +29,16 @@ Adjacent (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣
 adjacent? : ∀ {bounds} → Decidable₂ (Adjacent {bounds})
 adjacent? (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ℕ≟ 1
 
-Neighbor : ∀ {bounds} (coords : Coords bounds) → Set
-Neighbor coords = Σ[ neighbor ∈ _ ] Adjacent coords neighbor
+-- a Neighbor to `coords` is an adjacent tile: another coordinate pair and a proof that it's adjacent to `coords`.
+-- we don't compare the proofs for equality, so we define their setoid equality as equality on the coordinates
+Neighbor : ∀ {bounds} (coords : Coords bounds) → Setoid _ _
+Neighbor {w , h} coords = On.setoid {B = ∃ (Adjacent coords)} (×-setoid (Fin.setoid w) (Fin.setoid h)) proj₁
 
 neighbors : ∀ {bounds} (coords : Coords bounds) → Enumeration (Neighbor coords)
-neighbors {w , h} coords = Enum.filter ≡-irrelevant (adjacent? coords) (Enum.allFin w Enum.⊗ Enum.allFin h)
+neighbors {w , h} coords = Enum.filter (adjacent? coords) (subst (Adjacent coords) ∘ ≡×≡⇒≡) (Enum.allFin w Enum.⊗ Enum.allFin h)
+
+neighborCount : ∀ {bounds} (coords : Coords bounds) → ℕ
+neighborCount = Enumeration.cardinality ∘ neighbors
 
 
 Adjacent-sym : ∀ {bounds} (coords₁ coords₂ : Coords bounds) → Adjacent coords₁ coords₂ → Adjacent coords₂ coords₁
@@ -45,8 +50,6 @@ Adjacent-sym (x₁ , y₁) (x₂ , y₂) coords₁-coords₂-Adj = begin
   1 ∎
   where open ≡-Reasoning
 
-neighbor-sym : ∀ {bounds} {coords : Coords bounds} (neighbor : Neighbor coords) → Neighbor (proj₁ neighbor)
-neighbor-sym {coords = coords} (neighbor , adjacency) = coords , Adjacent-sym coords neighbor adjacency
 
 
 _≟_ : ∀ {bounds} → Decidable₂ (_≡_ {A = Coords bounds})