From c0cd81d43d56115650a0634b3e895947b99616f8 Mon Sep 17 00:00:00 2001
From: dianne <diannes.gm@gmail.com>
Date: Fri, 28 Dec 2018 15:05:49 -0800
Subject: [PATCH] fix up inductive definition of valid moves

oops! I'd forgotten a condition and the old definition was too weak.
when making an "a tile already has as many neighboring mines as it can, so its
other neighbors are safe" statement, the list of neighboring mines provided as
evidence must have unique elements!
---
 Minesweeper/Reasoning.agda | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda
index 992409c..45a8386 100644
--- a/Minesweeper/Reasoning.agda
+++ b/Minesweeper/Reasoning.agda
@@ -8,6 +8,7 @@ open import Relation.Binary.PropositionalEquality
 open import Data.List as List using (List)
 open import Data.List.Membership.Propositional
 open import Data.Product
+open import Data.List.All as All using (All; []; _∷_)
 open import Data.Nat
 
 open import Data.Fin using (Fin)
@@ -20,7 +21,18 @@ 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
 data _[_]↝★_ {bounds} (grid : Board Tile bounds) (coords : Coords bounds) : Guess → Set
-record _Neighboring★_on_excluding_ {bounds} (guess : Guess) (neighbor : Coords bounds) (grid : Board Tile bounds) (exclusion : Coords 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
 
 data _[_]↝★_ {bounds} grid coords where
   -- known tiles already have a proven identity
@@ -29,20 +41,14 @@ data _[_]↝★_ {bounds} grid coords where
   -- 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 : List (mine⚐ Neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords)) →
-    List.length neighborMines ≡ neighborMineCount →
+    (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 : List (safe⚐ Neighboring★ proj₁ (proj₁ safeNeighbor) on grid excluding coords)) →
-    List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeNeighbor)))) →
+    (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⚐
 
-record _Neighboring★_on_excluding_ {bounds} guess neighbor grid exclusion where
-  inductive
-  field
-    coords : Coords bounds
-    deduction : grid [ coords ]↝★ guess
-    ≢exclusion : coords ≢ exclusion