diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda index e3ccbf8..89cd2d0 100644 --- a/Minesweeper/Board.agda +++ b/Minesweeper/Board.agda @@ -2,11 +2,14 @@ module Minesweeper.Board where open import Data.Vec as Vec using (Vec) import Data.Vec.Properties as VecProp +import Data.Vec.Relation.Pointwise.Inductive as VecIndPointwise +import Data.Vec.Relation.Pointwise.Extensional as VecExtPointwise open import Data.Fin using (_≟_) open import Data.Product open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡) open import Function open import Relation.Nullary +open import Relation.Binary open import Relation.Binary.PropositionalEquality open ≡-Reasoning @@ -25,6 +28,18 @@ _Neighboring_on_ : ∀ {A bounds} → (A → Set) → Coords bounds → Board A P Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] P (lookup (proj₁ neighbor) grid) +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⇒VecPointwise : ∀ {ℓ A B} {_∼_ : REL A B ℓ} {bounds} {grid₁ : Board A bounds} {grid₂ : Board B bounds} → + Pointwise _∼_ grid₁ grid₂ → + VecIndPointwise.Pointwise (VecIndPointwise.Pointwise _∼_) grid₁ grid₂ +Pointwise⇒VecPointwise ₁∼₂ = + VecExtPointwise.extensional⇒inductive (VecExtPointwise.ext λ y → + VecExtPointwise.extensional⇒inductive (VecExtPointwise.ext λ x → + ₁∼₂ (x , y) ) ) + + lookup∘update : ∀ {A bounds} (coords : Coords bounds) (grid : Board A bounds) value → lookup coords (grid [ coords ]≔ value) ≡ value lookup∘update (x , y) grid value = begin diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index be5b8bf..5663294 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -3,7 +3,20 @@ module Minesweeper.Moves where open import Data.Empty +open import Data.Product +open import Data.Vec as Vec using (Vec; []; _∷_; _++_) +open import Data.Vec.Relation.Pointwise.Inductive as VecPointwise using ([]; _∷_) +open import Data.Nat hiding (_>_; _≥_) +import Data.Nat.Properties as ℕProp +open import Data.Fin as Fin using (Fin; zero; suc) open import Relation.Nullary +open import Relation.Unary renaming (Decidable to Decidable₁) +open import Relation.Binary renaming (Decidable to Decidable₂) +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Construct.Closure.Reflexive as Refl renaming (Refl to ReflexiveClosure) +open import Induction +open import Induction.WellFounded as WF +open import Induction.Nat using (<-wellFounded) open import Minesweeper.Coords open import Minesweeper.Board @@ -20,7 +33,7 @@ data _↝▣_ : Tile → KnownTile → Set where -- board filling: can a fully filled board be reached by filling in the unknown tiles of a partial board? _↝⊞_ : ∀ {bounds} → Board Tile bounds → Board KnownTile bounds → Set -holey ↝⊞ filled = ∀ coords → lookup coords holey ↝▣ lookup coords filled +_↝⊞_ = Pointwise _↝▣_ -- move validity: a guess as to a tile's identity on a board is valid when it holds in every rule-respecting way to fill the board's unfilled tiles @@ -53,3 +66,84 @@ invert⚐ safe⚐ = mine⚐ ¬-⚐✓-invert {mine⚐} {safe n} ¬guess⚐✓tile = ⚐✓safe n ¬-⚐✓-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 + + +-- 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: +-- boards are finite, so by filling one in step-by-step, eventually you'll have filled the whole board +data _≻_ : Tile → Tile → Set where + known≻unknown : ∀ {s} → known s ≻ unknown + +_≽_ : Rel Tile _ +_≽_ = ReflexiveClosure _≻_ + +_≥_ : ∀ {bounds} → Rel (Board Tile bounds) _ +_≥_ = Pointwise _≽_ + +record _>_ {bounds} (filled : Board Tile bounds) (holey : Board Tile bounds) : Set where + field + >⇒≥ : filled ≥ holey + >-strict : ∃[ coords ] (lookup coords filled ≻ lookup coords holey) + +open _>_ public + +>-Rec : ∀ {ℓ bounds} → RecStruct (Board Tile bounds) ℓ ℓ +>-Rec = WfRec _>_ + +-- more specific boards have fewer unknown tiles. then since _<_ on ℕ is well-founded, so is _>_ on Boards +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 + 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 + count-++ (unknown ∷ xs) ys = cong suc (count-++ xs ys) + + countUnknowns♭-monotone : ∀ {m} → VecPointwise.Pointwise _≽_ {m = m} =[ Vec.count unknown? ]⇒ _≤_ + countUnknowns♭-monotone [] = z≤n + countUnknowns♭-monotone ([ known≻unknown ] ∷ ts≽us) = ℕProp.≤-step (countUnknowns♭-monotone ts≽us) + 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 → + 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 → + 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 + suc (countUnknowns (ts ∷ tss)) ≡⟨ cong suc (count-++ ts (Vec.concat tss)) ⟩ + + suc (Vec.count unknown? ts + Vec.count unknown? (Vec.concat tss)) ≤⟨ ℕProp.+-mono-<-≤ (countUnknowns♭-strict-monotone x ti≻ui ts≽us) + (countUnknowns♭-monotone (VecPointwise.concat⁺ tss≽uss)) ⟩ + Vec.count unknown? us + Vec.count unknown? (Vec.concat uss) ≡⟨ sym (count-++ us (Vec.concat uss)) ⟩ + + countUnknowns (us ∷ uss) ∎ + where open ℕProp.≤-Reasoning + countUnknowns-strict-monotone′ {_} {ts ∷ tss} {us ∷ uss} (x , suc y) ti≻ui (ts≽us ∷ tss≽uss) = begin + suc (countUnknowns (ts ∷ tss)) ≡⟨ cong suc (count-++ ts (Vec.concat tss)) ⟩ + + suc (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) ⟩ + Vec.count unknown? us + Vec.count unknown? (Vec.concat uss) ≡⟨ sym (count-++ us (Vec.concat uss)) ⟩ + + countUnknowns (us ∷ uss) ∎ + where open ℕProp.≤-Reasoning + +>-wellFounded : ∀ {bounds} → WellFounded (_>_ {bounds}) +>-wellFounded = WF.Subrelation.wellFounded countUnknowns-strict-monotone (WF.Inverse-image.wellFounded countUnknowns <-wellFounded) + +module _ {ℓ bounds} where + open WF.All (>-wellFounded {bounds}) ℓ public + renaming ( wfRecBuilder to >-recBuilder + ; wfRec to >-rec )