add a rule for case analysis

the previous rules for constructing proofs that minesweeper moves are valid
weren't strong enough to express all valid moves. for example, on the board
```
**
*6 1
**```
if the tiles marked with `*`s are mines, all of the tiles adjacent to the `1`
but not the `6` will be safe. however, before, this could not be proven, since
we do not know the exact positions of all the mines or safe tiles adjacent to
either the `6` or `1`, and that was necessary information to make any judgment.
the new rule captures the reasoning that the `1`'s neighbors not adjacent to the
`6` will always be safe, since they can be shown to be safe for any way of
picking which of the `6`'s unknown neighbors is the mine,

Minesweeper/Board.agda

@@ -1,10 +1,16 @@
 module Minesweeper.Board where
 
 open import Data.Vec as Vec using (Vec)
+import Data.Vec.Properties as VecProp
+open import Data.Fin using (_≟_)
 open import Data.Product
+open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡)
+open import Function
+open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
+open ≡-Reasoning
 
-open import Minesweeper.Coords
+open import Minesweeper.Coords hiding (_≟_)
 
 Board : Set → Bounds → Set
 Board A (w , h) = Vec (Vec A w) h
@@ -17,3 +23,26 @@ grid [ (x , y) ]≔ value = grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ va
 
 _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)
+
+
+lookup∘update : ∀ {A bounds} (coords : Coords bounds) (grid : Board A bounds) value →
+  lookup coords (grid [ coords ]≔ value) ≡ value
+lookup∘update (x , y) grid value = begin
+  lookup (x , y) (grid [ x , y ]≔ value)
+    ≡⟨⟩
+  Vec.lookup x (Vec.lookup y (grid Vec.[ y ]≔ (Vec.lookup y grid Vec.[ x ]≔ value)))
+    ≡⟨ cong (Vec.lookup x) (VecProp.lookup∘update y grid (Vec.lookup y grid Vec.[ x ]≔ value)) ⟩
+  Vec.lookup x (Vec.lookup y grid Vec.[ x ]≔ value)
+    ≡⟨ VecProp.lookup∘update x (Vec.lookup y grid) value ⟩
+  value ∎
+
+lookup∘update′ : ∀ {A bounds} {coords₁ coords₂ : Coords bounds} → coords₁ ≢ coords₂ → ∀ (grid : Board A bounds) value →
+  lookup coords₁ (grid [ coords₂ ]≔ value) ≡ lookup coords₁ grid
+lookup∘update′ {coords₁ = x₁ , y₁} {x₂ , y₂} coords₁≢coords₂ grid value with y₁ ≟ y₂
+... | no y₁≢y₂ = cong (Vec.lookup x₁) (VecProp.lookup∘update′ y₁≢y₂ grid (Vec.lookup y₂ grid Vec.[ x₂ ]≔ value))
+... | yes refl = begin
+  lookup (x₁ , y₁) (grid [ x₂ , y₁ ]≔ value)
+    ≡⟨ cong (Vec.lookup x₁) (VecProp.lookup∘update y₁ grid (Vec.lookup y₁ grid Vec.[ x₂ ]≔ value)) ⟩
+  Vec.lookup x₁ (Vec.lookup y₁ grid Vec.[ x₂ ]≔ value)
+    ≡⟨ VecProp.lookup∘update′ (coords₁≢coords₂ ∘ flip (curry ≡×≡⇒≡) refl) (Vec.lookup y₁ grid) value ⟩
+  Vec.lookup x₁ (Vec.lookup y₁ grid) ∎

Minesweeper/Coords.agda

@@ -1,10 +1,11 @@
 module Minesweeper.Coords where
 
-open import Data.Nat
+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.Fin hiding (_≟_)
+open import Data.Product.Relation.Pointwise.NonDependent using (≡?×≡?⇒≡?)
+open import Data.Fin renaming (_≟_ to _Fin≟_)
 open import Relation.Binary using (Decidable)
 open import Relation.Binary.PropositionalEquality
 
@@ -20,7 +21,7 @@ Adjacent : ∀ {bounds} (coords₁ coords₂ : Coords bounds) → Set
 Adjacent (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ≡ 1
 
 adjacent? : ∀ {bounds} → Decidable (Adjacent {bounds})
-adjacent? (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ≟ 1
+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
@@ -40,3 +41,7 @@ Adjacent-sym (x₁ , y₁) (x₂ , y₂) coords₁-coords₂-Adj = begin
 
 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})
+_≟_ = ≡?×≡?⇒≡? _Fin≟_ _Fin≟_

Minesweeper/Reasoning.agda

@@ -20,8 +20,8 @@ open import Function.Inverse as Inverse using (_↔_)
 
 open import Data.Fin using (Fin)
 open import Minesweeper.Enumeration as Enum using (Enumeration)
-open import Minesweeper.Coords
-open import Minesweeper.Board
+open import Minesweeper.Coords as Coords using (Coords ; Neighbor ; neighbors)
+open import Minesweeper.Board as Board using (Board ; _Neighboring_on_ ; lookup ; _[_]≔_)
 open import Minesweeper.Rules
 open import Minesweeper.Moves
 
@@ -45,6 +45,12 @@ 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
 
+  -- case analysis: in a filled board the tile at `testCoords` will either be safe or a mine, so if we can
+  -- prove that our `guess` holds for the tile at `coords` regardless of which of those it is, then it will always hold.
+  cases★ : ∀ testCoords guess →
+    (∀ tile → (grid [ testCoords ]≔ known tile) [ coords ]↝★ guess) →
+      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)
@@ -79,13 +85,24 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord
 ...                                                                                     | 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
 
+-- 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
+  -- proofs by case analysis include information gained from which case is being inspected in the `grid`.
+  -- in the relevant case, our updated `grid` still can complete to `grid′`:
+  gridWithTest↝⊞grid′ : (grid [ testCoords ]≔ known (lookup testCoords grid′)) ↝⊞ grid′
+  gridWithTest↝⊞grid′ coords′ with coords′ Coords.≟ testCoords
+  -- at the test coordinates, it updates to be the known tile at those coordinates on `grid′`, which is present on `grid′`
+  ... | yes refl rewrite Board.lookup∘update coords′ grid (known (lookup coords′ grid′)) = ↝▣known (lookup coords′ grid′)
+  -- and elsewhere it is the same as in `grid`, which is compatible with `grid′` by our assumption `grid↝⊞grid′` that `grid` and `grid′` are compatible
+  ... | no coords′≢testCoords rewrite Board.lookup∘update′ coords′≢testCoords grid (known (lookup testCoords grid′)) = grid↝⊞grid′ coords′
+
 -- 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 _) =
-  Neighbors★-alreadyFull grid grid′ safeNeighbor (coords , Adjacent-sym coords safeNeighbor safeNeighbor-Adj) mine⚐ neighborMines mineEnumeration grid↝⊞grid′ grid′✓ enoughMines
+  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
@@ -96,7 +113,7 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord
 ...  | 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 _) =
-  Neighbors★-alreadyFull grid grid′ safeNeighbor (coords , Adjacent-sym coords safeNeighbor safeNeighbor-Adj) safe⚐ neighborSafes safeEnumeration grid↝⊞grid′ grid′✓ enoughSafes
+  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,
     -- we need to do a bit of arithmetic--splitting all of safeNeighbor's neighbors into safe tiles and mines--to see that our list really has all of them