From 588a21fb271749ff44100e40f92c35b8cfa34dcd Mon Sep 17 00:00:00 2001 From: dianne Date: Wed, 13 Feb 2019 19:34:23 -0800 Subject: [PATCH] a couple lemmas to beautify the soundness proof --- Minesweeper/Moves.agda | 18 +++++++++++++++++- Minesweeper/Reasoning.agda | 21 +++++++-------------- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index c83ada3..519881a 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -1,10 +1,12 @@ -- a hopefully-self-evident description of valid minesweeper moves +-- and several lemmas about it module Minesweeper.Moves where open import Data.Empty open import Data.Product open import Data.Sum +import Data.List as List open import Data.Vec as Vec using (Vec; []; _∷_; _++_) open import Data.Vec.Relation.Unary.Any as Any using (Any; any) import Data.Vec.Relation.Unary.Any.Properties as AnyProp @@ -24,6 +26,7 @@ open import Induction.WellFounded as WF open import Induction.Nat using (<-wellFounded) open import Function +open import Minesweeper.Enumeration using (Enumeration) open import Minesweeper.Coords as Coords open import Minesweeper.Board open import Minesweeper.Rules @@ -73,11 +76,24 @@ invert⚐ safe⚐ = mine⚐ ¬-⚐✓-invert {safe⚐} {mine} ¬guess⚐✓tile = ⚐✓mine ¬-⚐✓-invert {safe⚐} {safe n} ¬guess⚐✓tile = ⊥-elim (¬guess⚐✓tile (⚐✓safe n)) - unknown? : Decidable₁ (unknown ≡_) unknown? (known s) = no λ () unknown? unknown = yes refl +-- if a tile is already known, it can only be filled that way. +-- usually when we know a tile is known it's from a separate equality such as `known tile ≡ lookup coords grid`, +-- so this is specialized to account for that case +known-↝▣⇒≡ : ∀ {tile knowntile knowntile′} → tile ≡ known knowntile → tile ↝▣ knowntile′ → knowntile ≡ knowntile′ +known-↝▣⇒≡ refl (↝▣known _) = refl + +-- if a tile is specifically known to be safe with `n` adjacent mines on a consistent board `grid′`, we can go further: +-- `grid′ ✓` gives us an Enumeration of that tile's neighboring mines with exactly `n` members. +-- that is, on `grid′` it indeed does have `n` adjacent mines +known-safe-✓ : ∀ {bounds} (coords : Coords bounds) grid grid′ {n} → lookup coords grid ≡ known (safe n) → grid ↝⊞ grid′ → grid′ ✓ → + Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid′) ] n ≡ List.length (Enumeration.list neighboringMines) +known-safe-✓ coords grid grid′ coords↦safe grid↝⊞grid′ grid′✓ with grid′✓ coords +... | grid′[coords]✓ rewrite sym (known-↝▣⇒≡ coords↦safe (grid↝⊞grid′ coords)) = grid′[coords]✓ + -- specificity: a partially filled board is more specific than another if it agrees on all known tiles -- and has strictly more tiles known. this is helpful in writing inductive proofs as it is well-founded: diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda index a9af769..cd0aa09 100644 --- a/Minesweeper/Reasoning.agda +++ b/Minesweeper/Reasoning.agda @@ -100,9 +100,7 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord -- 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′✓ with grid↝⊞grid′ coords -... | 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 +★⇒✓ grid coords (known★ tile guess coords↦tile guess⚐✓tile) grid′ grid↝⊞grid′ grid′✓ = subst (guess ⚐✓_) (known-↝▣⇒≡ coords↦tile (grid↝⊞grid′ coords)) 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 @@ -137,17 +135,14 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord mineCountsConsistent (_ ∷ neighbors↝★guesses) | no ¬mine⚐✓tile | ⚐✓safe .n | .(safe n) | ⚐✓safe n = mineCountsConsistent neighbors↝★guesses testCoords-mineCount✓ : supposedMineCount ≡ List.length (Enumeration.list (neighboringMines grid′ testCoords)) - testCoords-mineCount✓ with grid↝⊞grid′ testCoords | grid′✓ testCoords - ... | tile↝▣tile | testCoords✓ rewrite testCoords-mineCount with lookup testCoords grid′ - testCoords-mineCount✓ | ↝▣known _ | mines′ , supposedMineCount≡length-mines′ | _ = + testCoords-mineCount✓ with known-safe-✓ testCoords grid grid′ testCoords-mineCount grid↝⊞grid′ grid′✓ + ... | 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 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 _) = + 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) @@ -155,10 +150,8 @@ Neighbors★-alreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coord -- 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 grid↝⊞grid′ safeNeighbor | grid′✓ safeNeighbor -... | 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 _) = + 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,