split specialized mine/safe rules out

they're not needed for the rules to be complete, so I've separated out the proofs that they're sound into their own definitions. I haven't paid too much attention to making it look nice, since I'm rewriting those parts anyway, but this change needed to come first.
dianne · Feb 14, 2019 · 4251b10 · 4251b10
1 parent 588a21f
commit 4251b10
Showing 1 changed file with 77 additions and 80 deletions.
diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda
@@ -27,22 +27,9 @@ open import Minesweeper.Board as Board using (Board ; _Neighboring_on_ ; lookup
 open import Minesweeper.Rules
 open import Minesweeper.Moves
 
--- our inductive family for minesweeper proofs! based on ProofSweeper but using our own machinery
--- and not intended for hand-writing at all
+-- our inductive family for minesweeper proofs!
 data _[_]↝★_ {bounds} (grid : Board Tile bounds) (coords : Coords bounds) : Guess → Set
 record Contradiction {bounds} (grid : Board Tile bounds) : Set
-record Neighbors★ {bounds} (grid : Board Tile bounds) (neighbor : Coords bounds) (exclude : Coords bounds) (guess : Guess) : Set
-Many_neighboring★_on_excluding_ : ∀ {bounds} → Guess → Coords bounds → Board Tile bounds → Coords bounds → Set
-
-record Neighbors★ {bounds} grid neighbor exclude guess where
-  inductive
-  field
-    list : List (Neighbor neighbor)
-    unique : ∀ {elem} (ix₁ ix₂ : elem ∈ list) → ix₁ ≡ ix₂
-    guess-valid★ : All (λ elem → grid [ proj₁ elem ]↝★ guess) list
-    exclusion : All (λ elem → exclude ≢ proj₁ elem) list
-
-Many_neighboring★_on_excluding_ guess neighbor grid exclude = Neighbors★ grid neighbor exclude guess
 
 -- noticing contradictions lets us narrow our resoning by dismissing impossible board states.
 -- here we define a contradiction as the existence of a known safe tile whose neighbors we can identify
@@ -70,34 +57,12 @@ data _[_]↝★_ {bounds} grid coords where
   -- ex falso quodlibet: a board with a contradiction in it has no way of being filled in, so it doesn't matter what we say about it.
   exfalso★ : ∀ guess → Contradiction grid → 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)
-    (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)
-    (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⚐
-
 
 -- let's do soundness first!
 -- roughly, this says that if you use the rules given by _[_]↝★_ to determine whether a tile is safe or a mine,
 -- it will indeed be that, for every possible way the unknown board tiles could be "filled in"
 ★⇒✓ : ∀ {bounds guess} (grid : Board Tile bounds) coords → grid [ coords ]↝★ guess → grid [ coords ]↝✓ guess
 
--- our core lemma: if a list of neighboring mines or safe tiles agrees in length with the complete list of such neighboring tiles in a filled board,
--- then any neighbor not in that list must be of the opposite tile type
-Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coords (other : Neighbor coords) guess (neighbors : Many guess neighboring★ coords on grid excluding proj₁ other)
-  (every : Enumeration ((guess ⚐✓_) Neighboring coords on grid′)) →
-  grid ↝⊞ grid′ → grid′ ✓ →
-  List.length (Neighbors★.list neighbors) ≡ List.length (Enumeration.list every) →
-    invert⚐ guess ⚐✓ lookup (proj₁ other) grid′
-
 -- 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′✓ = subst (guess ⚐✓_) (known-↝▣⇒≡ coords↦tile (grid↝⊞grid′ coords)) guess⚐✓tile
@@ -139,52 +104,30 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord
   ... | 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 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 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,
-    -- 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
-    splitNeighbors : Enumeration ((safe⚐ ⚐✓_) Neighboring safeNeighbor on grid′) × Enumeration ((mine⚐ ⚐✓_) Neighboring safeNeighbor on grid′)
-    splitNeighbors = Enum.partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeNeighbor)
-
-    safeEnumeration : Enumeration ((safe⚐ ⚐✓_) Neighboring safeNeighbor on grid′)
-    safeEnumeration = proj₁ splitNeighbors
-
-    enoughSafes : List.length (Neighbors★.list neighborSafes) ≡ List.length (Enumeration.list safeEnumeration)
-    enoughSafes = +-cancelʳ-≡ (List.length (Neighbors★.list neighborSafes)) (List.length (Enumeration.list safeEnumeration)) length-splitNeighbors where
-      open ≡-Reasoning
-      length-splitNeighbors : List.length (Neighbors★.list neighborSafes) + neighborMineCount ≡ List.length (Enumeration.list safeEnumeration) + neighborMineCount
-      length-splitNeighbors = begin
-        List.length (Neighbors★.list neighborSafes) + neighborMineCount
-          ≡⟨ neighborSafes-length ⟩
-        List.length (Enumeration.list (neighbors safeNeighbor))
-           ≡⟨ Enum.length-partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeNeighbor) ⟩
-        List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list (proj₂ splitNeighbors))
-          ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (Enum.enumeration-length-uniform (proj₂ splitNeighbors) mineEnumeration) ⟩
-        List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list mineEnumeration)
-          ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (sym neighborMineCount≡enumLength) ⟩
-        List.length (Enumeration.list safeEnumeration) + neighborMineCount ∎
 
-Neighbors★-alreadyFull grid grid′ coords other guess neighbors★ every grid↝⊞grid′ grid′✓ lengths-agree = ¬-⚐✓-invert ¬other↦guess where
+-- now we'll also show that some familiar reasoning principles used in proofsweeper are sound
+-- (and thus as a corrollary of the completeness of `_[_]↝★_`, they can be expressed in terms of those rules).
+-- our core lemma: if a list of mines or safe tiles neighboring some coordinates agrees in length with the
+-- complete list of such neighboring tiles in a filled board, then any other neighbor not in that list
+-- must be of the opposite tile type
+neighborsAlreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coords (other : Neighbor coords) guess
+  (every : Enumeration ((guess ⚐✓_) Neighboring coords on grid′)) →
+  (neighbors : List (Neighbor coords)) →
+  (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighbors) → ix₁ ≡ ix₂) →
+  All (λ neighbor → grid [ proj₁ neighbor ]↝✓ guess) neighbors →
+  All (λ neighbor → proj₁ other ≢ proj₁ neighbor) neighbors →
+  grid ↝⊞ grid′ → grid′ ✓ →
+  List.length neighbors ≡ List.length (Enumeration.list every) →
+    invert⚐ guess ⚐✓ lookup (proj₁ other) grid′
+neighborsAlreadyFull grid grid′ coords other guess every neighbors neighbors-unique neighbors↝✓guess other∉neighbors grid↝⊞grid′ grid′✓ lengths-agree = ¬-⚐✓-invert ¬other↦guess where
   -- to see that `neighbors` is the complete list of `coords`' neighbors of type `guess`, we first need to inductively verify✓ that `guess` indeed holds for them.
-  neighbors★⇒✓ : ∀ {neighbors : List (Neighbor coords)} → All (λ elem → grid [ proj₁ elem ]↝★ guess) neighbors → List ((guess ⚐✓_) Neighboring coords on grid′)
+  neighbors★⇒✓ : ∀ {neighbors : List (Neighbor coords)} → All (λ elem → grid [ proj₁ elem ]↝✓ guess) neighbors → List ((guess ⚐✓_) Neighboring coords on grid′)
   neighbors★⇒✓ {_} [] = []
-  neighbors★⇒✓ {neighbor ∷ _} (neighbor-valid★ ∷ neighbors-valid★) = (neighbor , ★⇒✓ _ _ neighbor-valid★ _ grid↝⊞grid′ grid′✓) ∷ neighbors★⇒✓ neighbors-valid★
+  neighbors★⇒✓ {neighbor ∷ _} (neighbor↝✓guess ∷ neighbors↝✓guess) = (neighbor , neighbor↝✓guess grid′ grid↝⊞grid′ grid′✓) ∷ neighbors★⇒✓ neighbors↝✓guess
 
   neighbors✓ : List (Σ[ neighbor ∈ Neighbor coords ] (guess ⚐✓ lookup (proj₁ neighbor) grid′))
-  neighbors✓ = neighbors★⇒✓ (Neighbors★.guess-valid★ neighbors★)
+  neighbors✓ = neighbors★⇒✓ neighbors↝✓guess
 
   -- `neighbors✓` has unique entries since `neighbors` does. we need a couple helpers first to see the connection, though
   ∈-neighbors★⇒✓⁻ : ∀ {neighbors neighbor neighbor✓} neighbors-valid★ →
@@ -204,7 +147,7 @@ Neighbors★-alreadyFull grid grid′ coords other guess neighbors★ every grid
   ∈-neighbors★⇒✓⁻-injective (_ ∷ neighbors-valid★) (there ix₁) (there ix₂) ★⇒✓⁻₁≡★⇒✓⁻₂ = cong there (∈-neighbors★⇒✓⁻-injective neighbors-valid★ ix₁ ix₂ (there-injective ★⇒✓⁻₁≡★⇒✓⁻₂))
 
   neighbors✓-unique : ∀ {neighbor✓} (ix₁ ix₂ : neighbor✓ ∈ neighbors✓) → ix₁ ≡ ix₂
-  neighbors✓-unique ix₁ ix₂ = ∈-neighbors★⇒✓⁻-injective _ ix₁ ix₂ (Neighbors★.unique neighbors★ (∈-neighbors★⇒✓⁻ _ ix₁) (∈-neighbors★⇒✓⁻ _ ix₂))
+  neighbors✓-unique ix₁ ix₂ = ∈-neighbors★⇒✓⁻-injective _ ix₁ ix₂ (neighbors-unique (∈-neighbors★⇒✓⁻ _ ix₁) (∈-neighbors★⇒✓⁻ _ ix₂))
 
   -- `neighbors★⇒✓` preserves length so `neighbor✓` is the same length as `Neighbors★.list neighbors★`
   length-neighbors★⇒✓ : ∀ {neighbors} neighbors-valid★ → List.length (neighbors★⇒✓ {neighbors} neighbors-valid★) ≡ List.length neighbors
@@ -215,12 +158,66 @@ Neighbors★-alreadyFull grid grid′ coords other guess neighbors★ every grid
   neighbors✓-complete : ∀ neighbor✓ → neighbor✓ ∈ neighbors✓
   neighbors✓-complete = Enum.long-list-complete every neighbors✓ neighbors✓-unique (begin
     List.length neighbors✓
-      ≡⟨ length-neighbors★⇒✓ (Neighbors★.guess-valid★ neighbors★) ⟩
-    List.length (Neighbors★.list neighbors★)
+      ≡⟨ length-neighbors★⇒✓ neighbors↝✓guess ⟩
+    List.length neighbors
       ≡⟨ lengths-agree ⟩
     List.length (Enumeration.list every) ∎)
     where open ≡-Reasoning
 
   -- `other` is not of type `guess`: it isn't in `neighbors`, so it isn't in `neighbors✓`, which is complete
   ¬other↦guess : ¬ guess ⚐✓ lookup (proj₁ other) grid′
-  ¬other↦guess other↦guess = All¬⇒¬Any (Neighbors★.exclusion neighbors★) (Any.map (cong proj₁) (∈-neighbors★⇒✓⁻ _ (neighbors✓-complete (other , other↦guess))))
+  ¬other↦guess other↦guess = All¬⇒¬Any other∉neighbors (Any.map (cong proj₁) (∈-neighbors★⇒✓⁻ _ (neighbors✓-complete (other , other↦guess))))
+
+-- from this we get that, given a safe tile with as many adjacent mines as it can have, its other neighbors must be safe
+otherNeighborIsSafe : ∀ {bounds} (grid : Board Tile bounds) neighborMineCount otherNeighbor
+  (safeCoords : (known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid)
+  (neighborMines : List (Neighbor (proj₁ (proj₁ safeCoords)))) →
+  (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighborMines) → ix₁ ≡ ix₂) →
+  All (λ neighbor → grid [ proj₁ neighbor ]↝✓ mine⚐) neighborMines →
+  All (λ neighbor → otherNeighbor ≢ proj₁ neighbor) neighborMines →
+  List.length neighborMines ≡ neighborMineCount →
+    grid [ otherNeighbor ]↝✓ safe⚐
+otherNeighborIsSafe grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborMines neighborMines-unique neighborMines↝✓mine⚐ otherNeighbor∉neighborMines neighborMines-length grid′ grid↝⊞grid′ grid′✓
+  with known-safe-✓ safeCoords grid grid′ (sym safeCoords-safe) grid↝⊞grid′ grid′✓
+...  | mineEnumeration , neighborMineCount≡enumLength =
+  neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) mine⚐ mineEnumeration neighborMines neighborMines-unique neighborMines↝✓mine⚐ otherNeighbor∉neighborMines grid↝⊞grid′ grid′✓ enoughMines
+  where
+    enoughMines : List.length neighborMines ≡ List.length (Enumeration.list mineEnumeration)
+    enoughMines = trans neighborMines-length neighborMineCount≡enumLength
+
+-- and likewise, given a safe tile with as many adjacent safe tiles as it can have, its other niehgbors must be mines
+otherNeighborIsMine : ∀ {bounds} (grid : Board Tile bounds) neighborMineCount otherNeighbor
+  (safeCoords : (known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid)
+  (neighborSafes : List (Neighbor (proj₁ (proj₁ safeCoords)))) →
+  (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighborSafes) → ix₁ ≡ ix₂) →
+  All (λ neighbor → grid [ proj₁ neighbor ]↝✓ safe⚐) neighborSafes →
+  All (λ neighbor → otherNeighbor ≢ proj₁ neighbor) neighborSafes →
+  List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeCoords)))) →
+    grid [ otherNeighbor ]↝✓ mine⚐
+otherNeighborIsMine grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborSafes neighborSafes-unique neighborSafes↝✓safe⚐ otherNeighbor∉neighborSafes neighborSafes-length grid′ grid↝⊞grid′ grid′✓
+  with known-safe-✓ safeCoords grid grid′ (sym safeCoords-safe) grid↝⊞grid′ grid′✓
+...  | mineEnumeration , neighborMineCount≡enumLength =
+  neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) safe⚐ safeEnumeration neighborSafes neighborSafes-unique neighborSafes↝✓safe⚐ otherNeighbor∉neighborSafes 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
+    splitNeighbors : Enumeration ((safe⚐ ⚐✓_) Neighboring safeCoords on grid′) × Enumeration ((mine⚐ ⚐✓_) Neighboring safeCoords on grid′)
+    splitNeighbors = Enum.partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeCoords)
+
+    safeEnumeration : Enumeration ((safe⚐ ⚐✓_) Neighboring safeCoords on grid′)
+    safeEnumeration = proj₁ splitNeighbors
+
+    enoughSafes : List.length neighborSafes ≡ List.length (Enumeration.list safeEnumeration)
+    enoughSafes = +-cancelʳ-≡ (List.length neighborSafes) (List.length (Enumeration.list safeEnumeration)) length-splitNeighbors where
+      open ≡-Reasoning
+      length-splitNeighbors : List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list safeEnumeration) + neighborMineCount
+      length-splitNeighbors = begin
+        List.length neighborSafes + neighborMineCount
+          ≡⟨ neighborSafes-length ⟩
+        List.length (Enumeration.list (neighbors safeCoords))
+           ≡⟨ Enum.length-partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeCoords) ⟩
+        List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list (proj₂ splitNeighbors))
+          ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (Enum.enumeration-length-uniform (proj₂ splitNeighbors) mineEnumeration) ⟩
+        List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list mineEnumeration)
+          ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (sym neighborMineCount≡enumLength) ⟩
+        List.length (Enumeration.list safeEnumeration) + neighborMineCount ∎