board validity is decidable

Minesweeper/Coords.agda

@@ -8,6 +8,7 @@ open import Data.Product.Relation.Pointwise.NonDependent using (≡?×≡?⇒≡
 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.Binary.PropositionalEquality
@@ -52,6 +53,10 @@ _≟_ : ∀ {bounds} → Decidable₂ (_≡_ {A = Coords bounds})
 _≟_ = ≡?×≡?⇒≡? _Fin≟_ _Fin≟_
 
 
+all? : ∀ {bounds p} {P : Coords bounds → Set p} → Decidable₁ P →
+  Dec (∀ coords → P coords)
+all? P? = Dec.map′ uncurry curry (Fin.all? (Fin.all? ∘ curry P?))
+
 ¬∀⟶∃¬ : ∀ bounds {p} (P : Coords bounds → Set p) → Decidable₁ P →
   ¬ (∀ coords → P coords) → (∃ λ coords → ¬ P coords)
 ¬∀⟶∃¬ bounds P P? ¬P with Fin.¬∀⟶∃¬ _ (λ x → ∀ y → P (x , y)) (Fin.all? ∘ curry P?) (¬P ∘ uncurry)

Minesweeper/Rules.agda

@@ -7,9 +7,10 @@ open import Data.Product
 open import Data.Sum
 open import Data.Nat as ℕ using (ℕ)
 open import Data.List hiding (lookup)
-open import Relation.Binary.PropositionalEquality
-open import Relation.Binary
 open import Relation.Nullary
+open import Relation.Unary  renaming (Decidable to Decidable₁; Irrelevant to Irrelevant₁)
+open import Relation.Binary renaming (Decidable to Decidable₂; Irrelevant to Irrelevant₂)
+open import Relation.Binary.PropositionalEquality
 
 open import Minesweeper.Coords
 open import Minesweeper.Board
@@ -41,7 +42,7 @@ _✓ : ∀ {bounds} → Board KnownTile bounds → Set
 _✓ {bounds} grid = ∀ coords → grid [ coords ]✓
 
 
-_⚐✓?_ : Decidable (_⚐✓_)
+_⚐✓?_ : Decidable₂ (_⚐✓_)
 mine⚐ ⚐✓? mine   = yes ⚐✓mine
 mine⚐ ⚐✓? safe _ = no λ { () }
 safe⚐ ⚐✓? mine   = no λ { () }
@@ -54,11 +55,11 @@ tileType (safe n) = inj₁ (⚐✓safe n)
 guessesDisjoint : ∀ {tile} → safe⚐ ⚐✓ tile → ¬ mine⚐ ⚐✓ tile
 guessesDisjoint () ⚐✓mine
 
-⚐✓-irrelevance : Irrelevant _⚐✓_
+⚐✓-irrelevance : Irrelevant₂ _⚐✓_
 ⚐✓-irrelevance ⚐✓mine     ⚐✓mine      = refl
 ⚐✓-irrelevance (⚐✓safe n) (⚐✓safe .n) = refl
 
-_≟⚐_ : Decidable (_≡_ {A = Guess})
+_≟⚐_ : Decidable₂ (_≡_ {A = Guess})
 mine⚐ ≟⚐ mine⚐ = yes refl
 mine⚐ ≟⚐ safe⚐ = no λ ()
 safe⚐ ≟⚐ mine⚐ = no λ ()
@@ -67,8 +68,8 @@ safe⚐ ≟⚐ safe⚐ = yes 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)
 
-_[_]✓? : ∀ {bounds} → Decidable (_[_]✓ {bounds})
-_[_]✓? {bounds} grid coords with lookup coords grid
+_[_]✓? : ∀ {bounds} → Decidable₂ (_[_]✓ {bounds})
+grid [ coords ]✓? with lookup coords grid
 ... | mine = yes tt
 ... | safe n with n ℕ.≟ length (Enumeration.list (neighboringMines grid coords))
 ...             | yes n≡len = yes (neighboringMines grid coords , n≡len)
@@ -80,6 +81,8 @@ _[_]✓? {bounds} grid coords with lookup coords grid
   length (Enumeration.list (neighboringMines grid coords)) ∎) }
   where open ≡-Reasoning
 
+_✓? : ∀ {bounds} → Decidable₁ (_✓ {bounds})
+grid ✓? = all? (grid [_]✓?)
 
 -- if a board is *not* valid, then there must be a specific safe tile on it whose label does not match the number of mines neighboring it
 identify-contradiction : ∀ {bounds} (grid : Board KnownTile bounds) →