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)