From c56f3d2ebb0d84def57d8f274369a2d40acff98c Mon Sep 17 00:00:00 2001 From: dianne Date: Sat, 6 Jul 2019 13:12:53 -0700 Subject: [PATCH] update agda to v2.6.0.1 and agda-stdlib to v1.1 I've also flipped the argument order of Minesweepeer.Board.lookup to agree with the new ordering used by Data.Vec.lookup, and I've made some implicit arguments explicit since they can't be inferred anymore. --- Minesweeper/Board.agda | 36 +++++++++++----------- Minesweeper/Coords.agda | 5 +-- Minesweeper/Enumeration.agda | 4 ++- Minesweeper/Moves.agda | 60 ++++++++++++++++++------------------ Minesweeper/Reasoning.agda | 44 +++++++++++++------------- Minesweeper/Rules.agda | 4 +-- 6 files changed, 78 insertions(+), 75 deletions(-) diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda index 7c725d5..37d30dd 100644 --- a/Minesweeper/Board.agda +++ b/Minesweeper/Board.agda @@ -24,8 +24,8 @@ open import Minesweeper.Coords hiding (_≟_) Board : Set → Bounds → Set Board A (w , h) = Vec (Vec A w) h -lookup : ∀ {A bounds} → Coords bounds → Board A bounds → A -lookup (x , y) grid = Vec.lookup x (Vec.lookup y grid) +lookup : ∀ {A bounds} → Board A bounds → Coords bounds → A +lookup grid (x , y) = Vec.lookup (Vec.lookup grid y) x _[_]≔_ : ∀ {A bounds} → Board A bounds → Coords bounds → A → Board A bounds grid [ (x , y) ]≔ value = Vec.updateAt y (Vec._[ x ]≔ value) grid @@ -35,17 +35,17 @@ grid [ (x , y) ]≔ value = Vec.updateAt y (Vec._[ x ]≔ value) grid -- we don't compare the proofs for equality, so we define their setoid equality as equality on the Neighbors _Neighboring_on_ : ∀ {p A bounds} → (A → Set p) → Coords bounds → Board A bounds → Setoid _ _ P Neighboring coords on grid = On.setoid - {B = Σ[ neighbor ∈ Setoid.Carrier (Neighbor coords) ] P (lookup (proj₁ neighbor) grid)} + {B = Σ[ neighbor ∈ Setoid.Carrier (Neighbor coords) ] P (lookup grid (proj₁ neighbor))} (Neighbor coords) proj₁ -- in order to get the neighbors of some coords satisfying P, we can filter all of its neighbors to just the ones satisfying P filterNeighbors : ∀ {p A bounds} {P : A → Set p} (P? : Decidable P) (grid : Board A bounds) (coords : Coords bounds) → Enumeration (P Neighboring coords on grid) -filterNeighbors {P = P} P? grid coords = Enum.filter (P? ∘ flip lookup grid ∘ proj₁) (subst (P ∘ flip lookup grid) ∘ ≡×≡⇒≡) (neighbors coords) +filterNeighbors {P = P} P? grid coords = Enum.filter (P? ∘ lookup grid ∘ proj₁) (subst (P ∘ lookup grid) ∘ ≡×≡⇒≡) (neighbors coords) Pointwise : ∀ {ℓ A B} (_∼_ : REL A B ℓ) {bounds} → REL (Board A bounds) (Board B bounds) _ -Pointwise _∼_ grid₁ grid₂ = ∀ coords → lookup coords grid₁ ∼ lookup coords grid₂ +Pointwise _∼_ grid₁ grid₂ = ∀ coords → lookup grid₁ coords ∼ lookup grid₂ coords Pointwise⇒VecPointwise : ∀ {ℓ A B} {_∼_ : REL A B ℓ} {bounds} {grid₁ : Board A bounds} {grid₂ : Board B bounds} → Pointwise _∼_ grid₁ grid₂ → @@ -57,23 +57,23 @@ Pointwise⇒VecPointwise ₁∼₂ = lookup∘update : ∀ {A bounds} (coords : Coords bounds) (grid : Board A bounds) value → - lookup coords (grid [ coords ]≔ value) ≡ value + lookup (grid [ coords ]≔ value) coords ≡ value lookup∘update (x , y) grid value = begin - lookup (x , y) (grid [ x , y ]≔ value) + lookup (grid [ x , y ]≔ value) (x , y) ≡⟨⟩ - Vec.lookup x (Vec.lookup y (Vec.updateAt y (Vec._[ x ]≔ value) grid)) - ≡⟨ cong (Vec.lookup x) (VecProp.lookup∘updateAt y grid) ⟩ - Vec.lookup x (Vec.lookup y grid Vec.[ x ]≔ value) - ≡⟨ VecProp.lookup∘update x (Vec.lookup y grid) value ⟩ + Vec.lookup (Vec.lookup (Vec.updateAt y (Vec._[ x ]≔ value) grid) y) x + ≡⟨ cong (flip Vec.lookup x) (VecProp.lookup∘updateAt y grid) ⟩ + Vec.lookup (Vec.lookup grid y Vec.[ x ]≔ value) x + ≡⟨ VecProp.lookup∘update x (Vec.lookup grid y) 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 (grid [ coords₂ ]≔ value) coords₁ ≡ lookup grid coords₁ lookup∘update′ {coords₁ = x₁ , y₁} {x₂ , y₂} coords₁≢coords₂ grid value with y₁ ≟ y₂ -... | no y₁≢y₂ = cong (Vec.lookup x₁) (VecProp.lookup∘updateAt′ y₁ y₂ y₁≢y₂ grid) +... | no y₁≢y₂ = cong (flip Vec.lookup x₁) (VecProp.lookup∘updateAt′ y₁ y₂ y₁≢y₂ grid) ... | yes refl = begin - lookup (x₁ , y₁) (grid [ x₂ , y₁ ]≔ value) - ≡⟨ cong (Vec.lookup x₁) (VecProp.lookup∘updateAt y₁ grid) ⟩ - 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) ∎ + lookup (grid [ x₂ , y₁ ]≔ value) (x₁ , y₁) + ≡⟨ cong (flip Vec.lookup x₁) (VecProp.lookup∘updateAt y₁ grid) ⟩ + Vec.lookup (Vec.lookup grid y₁ Vec.[ x₂ ]≔ value) x₁ + ≡⟨ VecProp.lookup∘update′ (coords₁≢coords₂ ∘ flip (curry ≡×≡⇒≡) refl) (Vec.lookup grid y₁) value ⟩ + Vec.lookup (Vec.lookup grid y₁) x₁ ∎ diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda index 4375c0d..3efc628 100644 --- a/Minesweeper/Coords.agda +++ b/Minesweeper/Coords.agda @@ -4,7 +4,8 @@ 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.Product.Relation.Pointwise.NonDependent using (×-setoid; ≡×≡⇒≡; ≡?×≡?⇒≡?) +import Data.Product.Properties as × +open import Data.Product.Relation.Pointwise.NonDependent using (×-setoid; ≡×≡⇒≡) open import Data.Fin renaming (_≟_ to _Fin≟_) import Data.Fin.Properties as Fin open import Relation.Nullary @@ -55,7 +56,7 @@ Adjacent-sym (x₁ , y₁) (x₂ , y₂) coords₁-coords₂-Adj = begin _≟_ : ∀ {bounds} → Decidable₂ (_≡_ {A = Coords bounds}) -_≟_ = ≡?×≡?⇒≡? _Fin≟_ _Fin≟_ +_≟_ = ×.≡-dec _Fin≟_ _Fin≟_ all? : ∀ {bounds p} {P : Coords bounds → Set p} → Decidable₁ P → diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda index 5f30bfd..043b02e 100644 --- a/Minesweeper/Enumeration.agda +++ b/Minesweeper/Enumeration.agda @@ -102,10 +102,12 @@ allFin n = record -- to enumerate coordinates on a board, we take the cartesian product of the rows and columns module _ {a b ℓ₁ ℓ₂} {A : Setoid a ℓ₁} {B : Setoid b ℓ₂} where open import Data.Product.Relation.Binary.Pointwise.NonDependent + open import Data.Product.Function.NonDependent.Setoid + open import Data.Product.Function.NonDependent.Propositional open import Data.Unit open import Data.List as List hiding (lookup) open import Data.List.Properties using (length-replicate) - open import Data.List.Relation.Unary.Any + open import Data.List.Relation.Unary.Any hiding (lookup) open import Data.List.Membership.Propositional open import Data.List.Membership.Propositional.Properties open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index a61a700..f15d2e9 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -58,7 +58,7 @@ _[_]↝✓_ : ∀ {bounds} → Board Tile bounds → Coords bounds → Guess → grid [ coords ]↝✓ guess = ∀ grid′ → grid ↝⊞ grid′ → grid′ ✓ → - guess ⚐✓ lookup coords grid′ + guess ⚐✓ lookup grid′ coords @@ -85,7 +85,7 @@ 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′ ✓ → +known-safe-✓ : ∀ {bounds} (coords : Coords bounds) grid grid′ {n} → lookup grid coords ≡ known (safe n) → grid ↝⊞ grid′ → grid′ ✓ → Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid′) ] n ≡ Enumeration.cardinality 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]✓ @@ -106,7 +106,7 @@ _≥_ = Pointwise _≽_ record _>_ {bounds} (filled : Board Tile bounds) (holey : Board Tile bounds) : Set where field >⇒≥ : filled ≥ holey - >-strict : ∃[ coords ] (lookup coords filled ≻ lookup coords holey) + >-strict : ∃[ coords ] (lookup filled coords ≻ lookup holey coords) open _>_ public @@ -118,7 +118,7 @@ countUnknowns : ∀ {bounds} → Board Tile bounds → ℕ countUnknowns grid = Vec.count unknown? (Vec.concat grid) countUnknowns-strict-monotone : ∀ {bounds} → _>_ {bounds} =[ countUnknowns ]⇒ _<_ -countUnknowns-strict-monotone filled>holey = uncurry countUnknowns-strict-monotone′ (>-strict filled>holey) (Pointwise⇒VecPointwise (>⇒≥ filled>holey)) where +countUnknowns-strict-monotone {_} {filled} {holey} filled>holey = uncurry (countUnknowns-strict-monotone′ filled holey) (>-strict filled>holey) (Pointwise⇒VecPointwise (>⇒≥ filled>holey)) where count-++ : ∀ {m n} (xs : Vec Tile m) (ys : Vec Tile n) → Vec.count unknown? (xs Vec.++ ys) ≡ Vec.count unknown? xs + Vec.count unknown? ys count-++ [] ys = refl count-++ (known _ ∷ xs) ys = count-++ xs ys @@ -130,16 +130,16 @@ countUnknowns-strict-monotone filled>holey = uncurry countUnknowns-strict-monoto countUnknowns♭-monotone (refl {known _} ∷ ts≽us) = countUnknowns♭-monotone ts≽us countUnknowns♭-monotone (refl {unknown} ∷ ts≽us) = s≤s (countUnknowns♭-monotone ts≽us) - countUnknowns♭-strict-monotone : ∀ {n} {filled holey : Vec Tile n} ix → Vec.lookup ix filled ≻ Vec.lookup ix holey → + countUnknowns♭-strict-monotone : ∀ {n} {filled holey : Vec Tile n} ix → Vec.lookup filled ix ≻ Vec.lookup holey ix → VecPointwise.Pointwise _≽_ filled holey → Vec.count unknown? filled < Vec.count unknown? holey countUnknowns♭-strict-monotone zero known≻unknown (_ ∷ ts≽us) = s≤s (countUnknowns♭-monotone ts≽us) countUnknowns♭-strict-monotone (suc i) ti≻ui ([ known≻unknown ] ∷ ts≽us) = ℕProp.≤-step (countUnknowns♭-strict-monotone i ti≻ui ts≽us) countUnknowns♭-strict-monotone (suc i) ti≻ui (refl {known _} ∷ ts≽us) = countUnknowns♭-strict-monotone i ti≻ui ts≽us countUnknowns♭-strict-monotone (suc i) ti≻ui (refl {unknown} ∷ ts≽us) = s≤s (countUnknowns♭-strict-monotone i ti≻ui ts≽us) - countUnknowns-strict-monotone′ : ∀ {bounds} {filled holey : Board Tile bounds} coords → lookup coords filled ≻ lookup coords holey → + countUnknowns-strict-monotone′ : ∀ {bounds} (filled holey : Board Tile bounds) coords → lookup filled coords ≻ lookup holey coords → VecPointwise.Pointwise (VecPointwise.Pointwise _≽_) filled holey → countUnknowns filled < countUnknowns holey - countUnknowns-strict-monotone′ {_} {ts ∷ tss} {us ∷ uss} (x , zero) ti≻ui (ts≽us ∷ tss≽uss) = begin-strict + countUnknowns-strict-monotone′ (ts ∷ tss) (us ∷ uss) (x , zero) ti≻ui (ts≽us ∷ tss≽uss) = begin-strict countUnknowns (ts ∷ tss) ≡⟨ count-++ ts (Vec.concat tss) ⟩ Vec.count unknown? ts + Vec.count unknown? (Vec.concat tss) <⟨ ℕProp.+-mono-<-≤ (countUnknowns♭-strict-monotone x ti≻ui ts≽us) @@ -148,11 +148,11 @@ countUnknowns-strict-monotone filled>holey = uncurry countUnknowns-strict-monoto countUnknowns (us ∷ uss) ∎ where open ℕProp.≤-Reasoning - countUnknowns-strict-monotone′ {_} {ts ∷ tss} {us ∷ uss} (x , suc y) ti≻ui (ts≽us ∷ tss≽uss) = begin-strict + countUnknowns-strict-monotone′ (ts ∷ tss) (us ∷ uss) (x , suc y) ti≻ui (ts≽us ∷ tss≽uss) = begin-strict countUnknowns (ts ∷ tss) ≡⟨ count-++ ts (Vec.concat tss) ⟩ Vec.count unknown? ts + Vec.count unknown? (Vec.concat tss) <⟨ ℕProp.+-mono-≤-< (countUnknowns♭-monotone ts≽us) - (countUnknowns-strict-monotone′ (x , y) ti≻ui tss≽uss) ⟩ + (countUnknowns-strict-monotone′ tss uss (x , y) ti≻ui tss≽uss) ⟩ Vec.count unknown? us + Vec.count unknown? (Vec.concat uss) ≡˘⟨ count-++ us (Vec.concat uss) ⟩ countUnknowns (us ∷ uss) ∎ @@ -167,13 +167,13 @@ module _ {ℓ bounds} where ; wfRec to >-rec ) -- in order to use this, a helper: filling in an unknown tile results in a more specific board -fill-> : ∀ {bounds} coords (grid : Board Tile bounds) tile → lookup coords grid ≡ unknown → +fill-> : ∀ {bounds} coords (grid : Board Tile bounds) tile → lookup grid coords ≡ unknown → (grid [ coords ]≔ known tile) > grid fill-> coords grid tile coords↦unknown = record { >⇒≥ = fill-≥ ; >-strict = coords , fill-≻ } where - fill-≻ : lookup coords (grid [ coords ]≔ known tile) ≻ lookup coords grid + fill-≻ : lookup (grid [ coords ]≔ known tile) coords ≻ lookup grid coords fill-≻ rewrite lookup∘update coords grid (known tile) | coords↦unknown = known≻unknown fill-≥ : (grid [ coords ]≔ known tile) ≥ grid @@ -183,18 +183,18 @@ fill-> coords grid tile coords↦unknown = record -- and also to help: a board either has an unknown tile or all of its tiles are known holey⊎filled : ∀ {bounds} (grid : Board Tile bounds) → - (∃ λ coords → lookup coords grid ≡ unknown) ⊎ (∀ coords → ∃ λ tile → lookup coords grid ≡ known tile) + (∃ λ coords → lookup grid coords ≡ unknown) ⊎ (∀ coords → ∃ λ tile → lookup grid coords ≡ known tile) holey⊎filled grid with any (any unknown?) grid ... | yes any-unknown = inj₁ ( (Any.index (AnyProp.lookup-index any-unknown) , Any.index any-unknown) , sym (AnyProp.lookup-index (AnyProp.lookup-index any-unknown)) ) ... | no ¬any-unknown = inj₂ allKnown where - allKnown : ∀ coords → ∃ λ tile → lookup coords grid ≡ known tile - allKnown coords with lookup coords grid | inspect (lookup coords) grid + allKnown : ∀ coords → ∃ λ tile → lookup grid coords ≡ known tile + allKnown coords with lookup grid coords | inspect (lookup grid) coords ... | known tile | _ = tile , refl ... | unknown | [ coords↦unknown ] = ⊥-elim (¬any-unknown (∈.toAny (∈.∈-lookup (proj₂ coords) grid) - (subst (_∈ Vec.lookup (proj₂ coords) grid) coords↦unknown - (∈.∈-lookup (proj₁ coords) (Vec.lookup (proj₂ coords) grid))))) + (subst (_∈ Vec.lookup grid (proj₂ coords)) coords↦unknown + (∈.∈-lookup (proj₁ coords) (Vec.lookup grid (proj₂ coords)))))) -- _≥_ and _↝⊞_ obey a sort of transitivity: if you can fill in a board, then any more general board @@ -204,26 +204,26 @@ holey⊎filled grid with any (any unknown?) grid ≽-↝▣-trans refl (↝▣known tile) = ↝▣known tile ≽-↝▣-trans refl (↝▣unknown tile) = ↝▣unknown tile -≥-↝⊞-trans : ∀ {bounds} {filled holey : Board Tile bounds} → filled ≥ holey → ∀ {fullyFilled} → filled ↝⊞ fullyFilled → holey ↝⊞ fullyFilled -≥-↝⊞-trans filled≥holey filled↝⊞fullyFilled coords = ≽-↝▣-trans (filled≥holey coords) (filled↝⊞fullyFilled coords) +≥-↝⊞-trans : ∀ {bounds} (filled holey : Board Tile bounds) → filled ≥ holey → ∀ fullyFilled → filled ↝⊞ fullyFilled → holey ↝⊞ fullyFilled +≥-↝⊞-trans filled holey filled≥holey fullyFilled filled↝⊞fullyFilled coords = ≽-↝▣-trans (filled≥holey coords) (filled↝⊞fullyFilled coords) -- if we know all the tiles of a board, we can get a board of KnownTiles from it in order to -- check it against the rules for filled boards in Minesweeper.Rules -unwrap : ∀ {bounds} {grid : Board Tile bounds} → (∀ coords → ∃ λ tile → lookup coords grid ≡ known tile) → Board KnownTile bounds -unwrap grid-filled = Vec.tabulate (λ y → Vec.tabulate (λ x → proj₁ (grid-filled (x , y)))) - -lookup∘unwrap : ∀ {bounds} {grid} grid-filled coords → lookup coords (unwrap {bounds} {grid} grid-filled) ≡ proj₁ (grid-filled coords) -lookup∘unwrap {grid = grid} grid-filled coords = begin - lookup coords (unwrap grid-filled) - ≡⟨ cong (Vec.lookup (proj₁ coords)) (VecProp.lookup∘tabulate (λ y → Vec.tabulate (λ x → proj₁ (grid-filled (x , y)))) (proj₂ coords)) ⟩ - Vec.lookup (proj₁ coords) (Vec.tabulate (λ x → proj₁ (grid-filled (x , proj₂ coords)))) +unwrap : ∀ {bounds} (grid : Board Tile bounds) → (∀ coords → ∃ λ tile → lookup grid coords ≡ known tile) → Board KnownTile bounds +unwrap grid grid-filled = Vec.tabulate (λ y → Vec.tabulate (λ x → proj₁ (grid-filled (x , y)))) + +lookup∘unwrap : ∀ {bounds} grid grid-filled coords → lookup (unwrap {bounds} grid grid-filled) coords ≡ proj₁ (grid-filled coords) +lookup∘unwrap grid grid-filled coords = begin + lookup (unwrap grid grid-filled) coords + ≡⟨ cong (flip Vec.lookup (proj₁ coords)) (VecProp.lookup∘tabulate (λ y → Vec.tabulate (λ x → proj₁ (grid-filled (x , y)))) (proj₂ coords)) ⟩ + Vec.lookup (Vec.tabulate (λ x → proj₁ (grid-filled (x , proj₂ coords)))) (proj₁ coords) ≡⟨ VecProp.lookup∘tabulate (λ x → proj₁ (grid-filled (x , proj₂ coords))) (proj₁ coords) ⟩ proj₁ (grid-filled coords) ∎ where open ≡-Reasoning -↝⊞-unwrap : ∀ {bounds} {grid} grid-filled → - grid ↝⊞ unwrap {bounds} {grid} grid-filled -↝⊞-unwrap grid-filled coords +↝⊞-unwrap : ∀ {bounds} grid grid-filled → + grid ↝⊞ unwrap {bounds} grid grid-filled +↝⊞-unwrap grid grid-filled coords rewrite proj₂ (grid-filled coords) - | lookup∘unwrap grid-filled coords = ↝▣known (proj₁ (grid-filled coords)) + | lookup∘unwrap grid grid-filled coords = ↝▣known (proj₁ (grid-filled coords)) diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda index ed69efb..a2d1b32 100644 --- a/Minesweeper/Reasoning.agda +++ b/Minesweeper/Reasoning.agda @@ -45,14 +45,14 @@ record Contradiction {bounds} grid where field coords : Coords bounds supposedMineCount : ℕ - coords-mineCount : lookup coords grid ≡ known (safe supposedMineCount) + coords-mineCount : lookup grid coords ≡ known (safe supposedMineCount) neighborGuesses : Fin (cardinality (Coords.neighbors coords)) → Guess neighborsKnown★ : ∀ i → grid [ proj₁ (Inverse.to (Enumeration.lookup (Coords.neighbors coords)) ⟨$⟩ i) ]↝★ neighborGuesses i disparity : supposedMineCount ≢ Enum.count (mine⚐ ≟⚐_) neighborGuesses 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 + known★ : ∀ tile guess → lookup grid coords ≡ 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. @@ -76,15 +76,15 @@ data _[_]↝★_ {bounds} grid coords where -- when considering proofs formed with the cases★ rule, for any way of completing our board, we can see which case actually applies to that final board. -- inductively, we may assume the proof given by that case is sound, so our guess holds for whichever tile we're looking at. -★⇒✓ grid coords (cases★ testCoords guess cases) grid′ grid↝⊞grid′ grid′✓ = ★⇒✓ _ _ (cases (lookup testCoords grid′)) grid′ gridWithTest↝⊞grid′ grid′✓ where +★⇒✓ grid coords (cases★ testCoords guess cases) grid′ grid↝⊞grid′ grid′✓ = ★⇒✓ _ _ (cases (lookup grid′ testCoords)) grid′ gridWithTest↝⊞grid′ grid′✓ where -- when looking at a specific case given by cases★, we update our board `grid` to include information about which case we're in. -- in order to show that the results we get from this still apply to whichever final board `grid′` we're looking at, we have the following lemma: - gridWithTest↝⊞grid′ : (grid [ testCoords ]≔ known (lookup testCoords grid′)) ↝⊞ grid′ + gridWithTest↝⊞grid′ : (grid [ testCoords ]≔ known (lookup grid′ testCoords)) ↝⊞ grid′ gridWithTest↝⊞grid′ coords′ with coords′ Coords.≟ testCoords -- at the test coordinates, we've updated the tile to be the known tile at those coordinates on `grid′`. this is fine since it's present on `grid′` by construction - ... | yes refl rewrite Board.lookup∘update coords′ grid (known (lookup coords′ grid′)) = ↝▣known (lookup coords′ grid′) + ... | yes refl rewrite Board.lookup∘update coords′ grid (known (lookup grid′ coords′)) = ↝▣known (lookup grid′ coords′) -- 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′ + ... | no coords′≢testCoords rewrite Board.lookup∘update′ coords′≢testCoords grid (known (lookup grid′ testCoords)) = grid↝⊞grid′ coords′ -- when we have a Contradiction, there's no valid completion of our board; consequently, any guess will hold, vacuously ★⇒✓ grid coords (exfalso★ guess contradiction) grid′ grid↝⊞grid′ grid′✓ = ⊥-elim (disparity (begin @@ -132,21 +132,21 @@ data _[_]↝★_ {bounds} grid coords where guess λ fullyFilled filled↝⊞fullyFilled fullyFilled✓ → coords↝✓guess fullyFilled - (≥-↝⊞-trans (>⇒≥ (fill-> unfilledCoords grid tile unfilledCoords-unknown)) filled↝⊞fullyFilled) + (≥-↝⊞-trans (grid [ unfilledCoords ]≔ known tile) grid (>⇒≥ (fill-> unfilledCoords grid tile unfilledCoords-unknown)) fullyFilled filled↝⊞fullyFilled) fullyFilled✓ -- otherwise, `grid` is entirely filled. our assumption `coords↝✓guess` that `grid [ coords ]↝✓ guess` guarantees that -- if there are no contradictions in `grid`, then we can find `guess` at `coords`. - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled with unwrap grid-filled ✓? + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled with unwrap grid grid-filled ✓? -- in the case that `guess` can be found on `grid` at `coords`, we can use the `known★` rule - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | yes grid′✓ with coords↝✓guess (unwrap grid-filled) (↝⊞-unwrap grid-filled) grid′✓ - ... | guess⚐✓tile rewrite lookup∘unwrap grid-filled coords = + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | yes grid′✓ with coords↝✓guess (unwrap grid grid-filled) (↝⊞-unwrap grid grid-filled) grid′✓ + ... | guess⚐✓tile rewrite lookup∘unwrap grid grid-filled coords = known★ (proj₁ (grid-filled coords)) guess (proj₂ (grid-filled coords)) guess⚐✓tile -- otherwise, there must be a contradiction somewhere on `grid`, so we can use the `exfalso★` rule - ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | no ¬grid′✓ with identify-contradiction (unwrap grid-filled) ¬grid′✓ - ... | badCoords , ¬grid′[badCoords]✓ rewrite lookup∘unwrap grid-filled badCoords with grid-filled badCoords + ✓⇒★′ grid ✓⇒★-rec coords guess coords↝✓guess | inj₂ grid-filled | no ¬grid′✓ with identify-contradiction (unwrap grid grid-filled) ¬grid′✓ + ... | badCoords , ¬grid′[badCoords]✓ rewrite lookup∘unwrap grid grid-filled badCoords with grid-filled badCoords -- the contradiction can't be at a mine, since only safe tiles are considered when determining if a board is consistent ... | mine , badCoords↦badTile = ⊥-elim (¬grid′[badCoords]✓ tt) @@ -171,21 +171,21 @@ data _[_]↝★_ {bounds} grid coords where neighbors : Fin (Coords.neighborCount badCoords) → Coords bounds neighbors = proj₁ ∘ (Inverse.to (Enumeration.lookup (Coords.neighbors badCoords)) ⟨$⟩_) - neighbors-filled : ∀ i → ∃[ tile ] (lookup (neighbors i) grid ≡ known tile) + neighbors-filled : ∀ i → ∃[ tile ] (lookup grid (neighbors i) ≡ known tile) neighbors-filled = grid-filled ∘ neighbors neighborGuesses : Fin (Coords.neighborCount badCoords) → Guess neighborGuesses = tileType ∘ proj₁ ∘ neighbors-filled - mineCounts-agree : Enum.count (mine⚐ ≟⚐_) neighborGuesses ≡ cardinality (neighboringMines (unwrap grid-filled) badCoords) + mineCounts-agree : Enum.count (mine⚐ ≟⚐_) neighborGuesses ≡ cardinality (neighboringMines (unwrap grid grid-filled) badCoords) mineCounts-agree = Enum.count-≡ _ _ _ _ (guesses-agree ∘ neighbors) where - guesses-agree : ∀ coords → mine⚐ ≡ tileType (proj₁ (grid-filled coords)) ⇔ mine⚐ ⚐✓ lookup coords (unwrap grid-filled) - guesses-agree coords rewrite lookup∘unwrap grid-filled coords with proj₁ (grid-filled coords) - ... | mine = equivalence (const ⚐✓mine) (const refl) - ... | safe _ = equivalence (λ ()) (λ ()) + guesses-agree : ∀ coords → mine⚐ ≡ tileType (proj₁ (grid-filled coords)) ⇔ mine⚐ ⚐✓ lookup (unwrap grid grid-filled) coords + guesses-agree coords rewrite lookup∘unwrap grid grid-filled coords with proj₁ (grid-filled coords) + ... | mine = equivalence (const ⚐✓mine) (const refl) + ... | safe _ = equivalence (λ ()) (λ ()) n≢mineCount : n ≢ Enum.count (mine⚐ ≟⚐_) neighborGuesses - n≢mineCount = ¬grid′[badCoords]✓ ∘ (neighboringMines (unwrap grid-filled) badCoords ,_) ∘ flip trans mineCounts-agree + n≢mineCount = ¬grid′[badCoords]✓ ∘ (neighboringMines (unwrap grid grid-filled) badCoords ,_) ∘ flip trans mineCounts-agree @@ -209,7 +209,7 @@ neighborsAlreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coords (o cardinality every Unique guess Neighboring coords on grid Excluding proj₁ other → grid ↝⊞ grid′ → grid′ ✓ → - invert⚐ guess ⚐✓ lookup (proj₁ other) grid′ + invert⚐ guess ⚐✓ lookup grid′ (proj₁ other) neighborsAlreadyFull grid grid′ coords other guess every neighbors′ grid↝⊞grid′ grid′✓ = ¬-⚐✓-invert ¬other↦guess where open _Unique_Neighboring_on_Excluding_ neighbors′ @@ -224,7 +224,7 @@ neighborsAlreadyFull grid grid′ coords other guess every neighbors′ grid↝ neighbors✓-full = Enum.injection-surjective every neighbors✓ -- `other` is not of type `guess`: it isn't in `neighbors`, so it isn't in `neighbors✓`, which it would be if it was of type `guess` - ¬other↦guess : ¬ guess ⚐✓ lookup (proj₁ other) grid′ + ¬other↦guess : ¬ guess ⚐✓ lookup grid′ (proj₁ other) ¬other↦guess other↦guess = other∉neighbors (Surjective.from neighbors✓-full ⟨$⟩ (other , other↦guess)) (≡×≡⇒≡ (Surjective.right-inverse-of neighbors✓-full (other , other↦guess))) @@ -284,7 +284,7 @@ otherNeighborIsMine grid neighborMineCount otherNeighbor ((safeCoords , safeCoor enoughSafes = begin Coords.neighborCount safeCoords ∸ neighborMineCount ≡⟨ cong (_∸ neighborMineCount) (Enum.cardinality-partition - (subst ((safe⚐ ⚐✓_) ∘ flip lookup grid′) ∘ ≡×≡⇒≡) + (subst ((safe⚐ ⚐✓_) ∘ lookup grid′) ∘ ≡×≡⇒≡) (Coords.neighbors safeCoords) safeEnumeration (Enum.map mine⚐↔¬safe⚐ mineEnumeration)) ⟩ diff --git a/Minesweeper/Rules.agda b/Minesweeper/Rules.agda index 5751fca..f0a6da9 100644 --- a/Minesweeper/Rules.agda +++ b/Minesweeper/Rules.agda @@ -39,7 +39,7 @@ data _⚐✓_ : Guess → KnownTile → Set where -- consistency: `grid [ coords ]✓` means that if `grid` has a safe tile at `coords`, then the number on it agrees with the number of mines adjacent to it. -- since only safe tiles are checked in this way, coordinates with mines are always regarded as valid, regardless of if they have adjacent inconsistent safe tiles. _[_]✓ : ∀ {bounds} → Board KnownTile bounds → Coords bounds → Set -_[_]✓ {bounds} grid coords with lookup coords grid +_[_]✓ {bounds} grid coords with lookup grid coords ... | mine = ⊤ ... | safe n = Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) ] n ≡ Enumeration.cardinality neighboringMines @@ -72,7 +72,7 @@ neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords neighboringMines = filterNeighbors (mine⚐ ⚐✓?_) _[_]✓? : ∀ {bounds} → Decidable₂ (_[_]✓ {bounds}) -grid [ coords ]✓? with lookup coords grid +grid [ coords ]✓? with lookup grid coords ... | mine = yes tt ... | safe n with n ℕ.≟ Enumeration.cardinality (neighboringMines grid coords) ... | yes n≡len = yes (neighboringMines grid coords , n≡len)