diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda index c5a1d07..2937ccd 100644 --- a/Minesweeper/Board.agda +++ b/Minesweeper/Board.agda @@ -9,10 +9,13 @@ 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.Unary using (Decidable) +open import Relation.Binary hiding (Decidable) open import Relation.Binary.PropositionalEquality +import Relation.Binary.Construct.On as On open ≡-Reasoning +open import Minesweeper.Enumeration as Enum using (Enumeration) open import Minesweeper.Coords hiding (_≟_) Board : Set → Bounds → Set @@ -24,8 +27,18 @@ lookup (x , y) grid = Vec.lookup x (Vec.lookup y grid) _[_]≔_ : ∀ {A bounds} → Board A bounds → Coords bounds → A → Board A bounds grid [ (x , y) ]≔ value = Vec.updateAt y (Vec._[ x ]≔ value) grid -_Neighboring_on_ : ∀ {A bounds} → (A → Set) → Coords bounds → Board A bounds → Set -P Neighboring coords on grid = Σ[ neighbor ∈ Neighbor coords ] P (lookup (proj₁ neighbor) grid) +-- `P Neighboring coords on grid` are the adjacent tiles to `coords` that satisfy the predicate `P`: +-- a `Neighbor coords` paired with a proof that its coordinates, when looked up on `grid`, satisfy `P`. +-- 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)} + (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) Pointwise : ∀ {ℓ A B} (_∼_ : REL A B ℓ) {bounds} → REL (Board A bounds) (Board B bounds) _ diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda index f17deb3..000e72c 100644 --- a/Minesweeper/Coords.agda +++ b/Minesweeper/Coords.agda @@ -4,15 +4,15 @@ 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 (≡?×≡?⇒≡?) +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 import Relation.Nullary.Decidable as Dec -open import Relation.Unary using () renaming (Decidable to Decidable₁) -open import Relation.Binary using () renaming (Decidable to Decidable₂) +open import Relation.Unary using () renaming (Decidable to Decidable₁) +open import Relation.Binary using (Setoid) renaming (Decidable to Decidable₂) open import Relation.Binary.PropositionalEquality -open import Relation.Binary.PropositionalEquality.WithK +import Relation.Binary.Construct.On as On open import Function open import Minesweeper.Enumeration as Enum using (Enumeration) @@ -29,11 +29,16 @@ Adjacent (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ adjacent? : ∀ {bounds} → Decidable₂ (Adjacent {bounds}) adjacent? (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ℕ≟ 1 -Neighbor : ∀ {bounds} (coords : Coords bounds) → Set -Neighbor coords = Σ[ neighbor ∈ _ ] Adjacent coords neighbor +-- a Neighbor to `coords` is an adjacent tile: another coordinate pair and a proof that it's adjacent to `coords`. +-- we don't compare the proofs for equality, so we define their setoid equality as equality on the coordinates +Neighbor : ∀ {bounds} (coords : Coords bounds) → Setoid _ _ +Neighbor {w , h} coords = On.setoid {B = ∃ (Adjacent coords)} (×-setoid (Fin.setoid w) (Fin.setoid h)) proj₁ neighbors : ∀ {bounds} (coords : Coords bounds) → Enumeration (Neighbor coords) -neighbors {w , h} coords = Enum.filter ≡-irrelevant (adjacent? coords) (Enum.allFin w Enum.⊗ Enum.allFin h) +neighbors {w , h} coords = Enum.filter (adjacent? coords) (subst (Adjacent coords) ∘ ≡×≡⇒≡) (Enum.allFin w Enum.⊗ Enum.allFin h) + +neighborCount : ∀ {bounds} (coords : Coords bounds) → ℕ +neighborCount = Enumeration.cardinality ∘ neighbors Adjacent-sym : ∀ {bounds} (coords₁ coords₂ : Coords bounds) → Adjacent coords₁ coords₂ → Adjacent coords₂ coords₁ @@ -45,8 +50,6 @@ Adjacent-sym (x₁ , y₁) (x₂ , y₂) coords₁-coords₂-Adj = begin 1 ∎ where open ≡-Reasoning -neighbor-sym : ∀ {bounds} {coords : Coords bounds} (neighbor : Neighbor coords) → Neighbor (proj₁ neighbor) -neighbor-sym {coords = coords} (neighbor , adjacency) = coords , Adjacent-sym coords neighbor adjacency _≟_ : ∀ {bounds} → Decidable₂ (_≡_ {A = Coords bounds}) diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda index 7d9b5dc..5f30bfd 100644 --- a/Minesweeper/Enumeration.agda +++ b/Minesweeper/Enumeration.agda @@ -1,331 +1,327 @@ module Minesweeper.Enumeration where -open import Data.List as List using (List; []; _∷_) -import Data.List.Categorical as List -import Data.List.Properties as ListProp -open import Data.List.Relation.Unary.Any as Any using (Any ; here ; there) -import Data.List.Any.Properties as AnyProp -open import Data.List.Membership.Propositional -import Data.List.Membership.Propositional.Properties as ∈Prop -open import Data.List.Relation.BagAndSetEquality -open import Data.Fin -import Data.Fin.Properties as FinProp -open import Data.Nat as ℕ -import Data.Nat.Properties as ℕProp -open import Data.Maybe as Maybe using (Maybe; just; nothing) +open import Data.Fin as Fin using (Fin; zero; suc) +import Data.Fin.Properties as Fin +import Data.Fin.Permutation as Fin +open import Data.Nat as ℕ hiding (_⊔_) +import Data.Nat.Properties as ℕ open import Data.Empty +open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂) open import Function -open import Function.Inverse as Inverse using (Inverse; _↔_) -open import Function.Injection as Injection using (Injection; _↣_) renaming (_∘_ to _⟪∘⟫_) -open import Function.Equality using (_⟨$⟩_) +open import Function.Equality using (Π; _⟶_; _⟨$⟩_) renaming (_∘_ to _∘⟵_) +open import Function.Equivalence using (Equivalence; _⇔_) +open import Function.Injection as Injection using (Injective; Injection; _↣_; injection) renaming (_∘_ to _∘↢_) +open import Function.Surjection as Surjection using (Surjective) renaming (_∘_ to _∘↞_) +open import Function.Bijection as Bijection using (Bijective) +open import Function.Inverse as Inverse using (Inverse; _↔_) renaming (_∘_ to _∘↔_; id to id↔; sym to sym↔) open import Relation.Nullary open import Relation.Nullary.Negation -import Relation.Nullary.Decidable as Decidable -open import Relation.Unary using () renaming (Decidable to Decidable₁ ; Irrelevant to Irrelevant₁) -open import Relation.Binary using () renaming (Decidable to Decidable₂) -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.PropositionalEquality.WithK -open import Data.Product using (Σ; ∃; _×_; _,_) -open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′) -open import Category.Monad -import Level +import Relation.Nullary.Decidable as Decidable +open import Relation.Unary using (Decidable) +open import Relation.Binary using (Setoid; _Respects_) renaming (Decidable to Decidable₂) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; →-to-⟶) +import Relation.Binary.Construct.On as On +open import Level renaming (zero to lzero; suc to lsuc) -- in order to talk about the number of mines adjacent to a tile, we define Enumeration: --- a list of all the elements of a type, with each appearing once. +-- a bijective correspondence between some type and the set of natural numbers less +-- than some `n`. then, `n` can be seen as the number of elements of that type. +-- by enumerating a type corresponding to the mines adjacent to a given tile, we can get +-- the number of how many there are. -- our goal here is to develop the necessary machinery to do that. specifically, we need --- that all Enumerations of a type have the same length (they're unique up to bag equality), --- we need to be able to be able to enumerate the adjacent mines of a tile, (which we --- get by enumerating any m×n grid and filtering by a predicate), and we need that a list with --- unique entries with the same length as an Enumeration is itself complete -record Enumeration A : Set where +-- that all Enumerations of a type have the same number of elements, we need to be able to +-- be able to enumerate the adjacent mines of a tile, (which we get by enumerating any m×n +-- grid and filtering by a predicate), and we need that a list with unique entries with +-- the same length as an Enumeration is itself complete +record Enumeration {c ℓ} (A : Setoid c ℓ) : Set (c ⊔ ℓ) where field - list : List A - complete : ∀ a → a ∈ list - entries-unique : ∀ {a} (ix₁ ix₂ : a ∈ list) → ix₁ ≡ ix₂ + cardinality : ℕ + lookup : Inverse (Fin.setoid cardinality) A open Enumeration --- first, Enumerations are unique up to bag equality and thus all equal in length -private - remove : ∀ {A : Set} {ys} {y : A} → y ∈ ys → List A - remove {ys = _ ∷ ys} (here _) = ys - remove {ys = y ∷ ys} (there y∈ys) = y ∷ remove y∈ys - - remove-subbag′ : ∀ {A : Set} (x : A) xs ys ys′ (x∈ys : x ∈ ys) (inclusion : ∀ {a} → (a ∈ x ∷ xs) ↣ (a ∈ ys ⊎ a ∈ ys′)) → - inj₁ x∈ys ≡ Injection.to inclusion ⟨$⟩ here refl → - ∀ {a} → (a ∈ xs) ↣ (a ∈ remove x∈ys ⊎ a ∈ ys′) - remove-subbag′ x xs (.x ∷ ys) ys′ (here refl) inclusion x∈ys-≡ {a} = record - { to = →-to-⟶ inclusion′ - ; injective = inclusion′-injective } +-- first, Enumerations of the same type are equal in `cardinality` +cardinality-≡ : ∀ {c ℓ} {A : Setoid c ℓ} (enum₁ enum₂ : Enumeration A) → + cardinality enum₁ ≡ cardinality enum₂ +cardinality-≡ enum₁ enum₂ = Fin.↔⇒≡ (sym↔ (lookup enum₂) ∘↔ lookup enum₁) + +-- next, if you have enough unique elements of a type, then you have all of them! +injection-surjective : ∀ {c ℓ} {A : Setoid c ℓ} (enum : Enumeration A) (f : Injection (Fin.setoid (cardinality enum)) A) → + Surjective (Injection.to f) +injection-surjective {A = A} enum f = record + { from = translateIndex-enum⟶f ∘⟵ Inverse.from (lookup enum) + ; right-inverse-of = λ a → + Inverse.injective (sym↔ (lookup enum)) + (Surjective.right-inverse-of (fin-injection-surjective translateIndex-f↣enum) + (Inverse.from (lookup enum) ⟨$⟩ a)) } + where + -- any injection `f : Fin n ↣ Fin n` is also surjective: by the pigeonhole principle, + -- if there is any `m` for which no `n` exists such that `f n ≡ m`, then there must + -- be distinct `i` and `j` with `f i ≡ f j`; however, this cannot happen, since `f` + -- is injective. + fin-injection-surjective : ∀ {n} (g : Fin n ↣ Fin n) → Surjective (Injection.to g) + fin-injection-surjective g = record + { from = →-to-⟶ (proj₁ ∘ g⁻¹) + ; right-inverse-of = proj₂ ∘ g⁻¹ } where - inclusion′-helper : ∀ {a∈xs : a ∈ xs} (a∈yss : a ∈ x ∷ ys ⊎ a ∈ ys′) → (Injection.to inclusion ⟨$⟩ there a∈xs ≡ a∈yss) → a ∈ ys ⊎ a ∈ ys′ - inclusion′-helper (inj₁ (here refl)) a↦x with Injection.injective inclusion (trans a↦x x∈ys-≡) - ... | () - inclusion′-helper (inj₁ (there a∈ys)) _ = inj₁ a∈ys - inclusion′-helper (inj₂ a∈ys′) _ = inj₂ a∈ys′ - - inclusion′ : a ∈ xs → a ∈ ys ⊎ a ∈ ys′ - inclusion′ a∈xs = inclusion′-helper (Injection.to inclusion ⟨$⟩ there a∈xs) refl where - - inclusion′-helper-spec : ∀ {a∈xs : a ∈ xs} a∈yss a↦x → - Sum.map there id (inclusion′-helper {a∈xs} a∈yss a↦x) ≡ Injection.to inclusion ⟨$⟩ there a∈xs - inclusion′-helper-spec (inj₁ (here refl)) a↦x with Injection.injective inclusion (trans a↦x x∈ys-≡) - ... | () - inclusion′-helper-spec (inj₁ (there a∈ys)) a↦x rewrite a↦x = refl - inclusion′-helper-spec (inj₂ a∈ys′) a↦x rewrite a↦x = refl - - inclusion′-spec : ∀ {a∈xs : a ∈ xs} → Sum.map there id (inclusion′ a∈xs) ≡ Injection.to inclusion ⟨$⟩ there a∈xs - inclusion′-spec = inclusion′-helper-spec _ refl - - inclusion′-injective : ∀ {a∈xs₁ a∈xs₂ : a ∈ xs} → inclusion′ a∈xs₁ ≡ inclusion′ a∈xs₂ → a∈xs₁ ≡ a∈xs₂ - inclusion′-injective {a∈xs₁} {a∈xs₂} inclusion′-≡ = AnyProp.there-injective (Injection.injective inclusion - (begin - Injection.to inclusion ⟨$⟩ there a∈xs₁ - ≡⟨ sym inclusion′-spec ⟩ - Sum.map there id (inclusion′ a∈xs₁) - ≡⟨ cong (Sum.map there id) inclusion′-≡ ⟩ - Sum.map there id (inclusion′ a∈xs₂) - ≡⟨ inclusion′-spec ⟩ - Injection.to inclusion ⟨$⟩ there a∈xs₂ ∎)) where open ≡-Reasoning - remove-subbag′ x xs (y ∷ ys) ys′ (there x∈ys) inclusion x∈ys-≡ = - shiftHead₂ ⟪∘⟫ remove-subbag′ x xs ys (y ∷ ys′) x∈ys (shiftHead₁ ⟪∘⟫ inclusion) x∈ys-≡′ where - shiftHead₂ : ∀ {a} → (a ∈ remove x∈ys ⊎ a ∈ y ∷ ys′) ↣ (a ∈ y ∷ remove x∈ys ⊎ a ∈ ys′) - shiftHead₂ = record - { to = →-to-⟶ [ (inj₁ ∘ there) , (λ { (here a≡y) → inj₁ (here a≡y) ; (there a∈ys′) → inj₂ a∈ys′ }) ]′ - ; injective = λ - { {inj₁ _} {inj₁ _} refl → refl - ; {inj₁ _} {inj₂ (here _)} () ; {inj₁ _} {inj₂ (there _)} () ; {inj₂ (here _)} {inj₁ _} () ; {inj₂ (there _)} {inj₁ _} () - ; {inj₂ (here _)} {inj₂ (here _)} refl → refl ; {inj₂ (there _)} {inj₂ (there _)} refl → refl - ; {inj₂ (here _)} {inj₂ (there _)} () ; {inj₂ (there _)} {inj₂ (here _)} () } } - shiftHead₁ : ∀ {a} → (a ∈ y ∷ ys ⊎ a ∈ ys′) ↣ (a ∈ ys ⊎ a ∈ y ∷ ys′) - shiftHead₁ = record - { to = →-to-⟶ [ (λ { (here a≡y) → inj₂ (here a≡y) ; (there a∈ys′) → inj₁ a∈ys′ }) , (inj₂ ∘ there) ]′ - ; injective = λ - { {inj₁ (here _)} {inj₁ (here _)} refl → refl ; {inj₁ (there _)} {inj₁ (there _)} refl → refl - ; {inj₁ (here _)} {inj₁ (there _)} () ; {inj₁ (there _)} {inj₁ (here _)} () - ; {inj₁ (here _)} {inj₂ _} () ; {inj₁ (there _)} {inj₂ _} () ; {inj₂ _} {inj₁ (here _)} () ; {inj₂ _} {inj₁ (there _)} () - ; {inj₂ _} {inj₂ _} refl → refl } } - x∈ys-≡′ : inj₁ x∈ys ≡ Injection.to (shiftHead₁ ⟪∘⟫ inclusion) ⟨$⟩ here refl - x∈ys-≡′ = begin - inj₁ x∈ys - ≡⟨⟩ - Injection.to shiftHead₁ ⟨$⟩ inj₁ (there x∈ys) - ≡⟨ cong (_⟨$⟩_ (Injection.to shiftHead₁)) x∈ys-≡ ⟩ - Injection.to shiftHead₁ ⟨$⟩ (Injection.to inclusion ⟨$⟩ here refl) - ≡⟨⟩ - Injection.to (shiftHead₁ ⟪∘⟫ inclusion) ⟨$⟩ here refl ∎ where open ≡-Reasoning - - remove-subbag : ∀ {A : Set} (x : A) xs ys → (inclusion : (x ∷ xs) ∼[ subbag ] ys) → xs ∼[ subbag ] remove (Injection.to inclusion ⟨$⟩ here refl) - remove-subbag x xs ys inclusion = remove-⊎ ⟪∘⟫ remove-subbag′ x xs ys [] (Injection.to inclusion ⟨$⟩ here refl) (inj₁-Injection ⟪∘⟫ inclusion) refl where - inj₁-Injection : ∀ {a} → (a ∈ ys) ↣ (a ∈ ys ⊎ a ∈ []) - inj₁-Injection = record - { to = →-to-⟶ inj₁ - ; injective = λ { refl → refl } } - remove-⊎ : ∀ {a ys′} → (a ∈ ys′ ⊎ a ∈ []) ↣ (a ∈ ys′) - remove-⊎ = record - { to = →-to-⟶ λ { (inj₁ a∈ys′) → a∈ys′ ; (inj₂ ()) } - ; injective = λ - { {inj₁ _} {inj₁ _} refl → refl - ; {inj₁ _} {inj₂ ()} _ ; {inj₂ ()} {inj₁ _} _ ; {inj₂ ()} {inj₂ ()} _ } } - - remove-length : ∀ {A : Set} {x : A} {xs} (x∈xs : x ∈ xs) → List.length xs ≡ suc (List.length (remove x∈xs)) - remove-length (here _) = refl - remove-length (there x∈xs) = cong suc (remove-length x∈xs) - - subbag-length-≤ : ∀ {A : Set} {xs ys : List A} → xs ∼[ subbag ] ys → List.length xs ℕ.≤ List.length ys - subbag-length-≤ {xs = []} {ys} xs⊑ys = z≤n - subbag-length-≤ {xs = x ∷ xs} {ys} xs⊑ys = begin - List.length (x ∷ xs) - ≈⟨⟩ - suc (List.length xs) - ≤⟨ s≤s (subbag-length-≤ (remove-subbag x xs ys xs⊑ys)) ⟩ - suc (List.length (remove (Injection.to xs⊑ys ⟨$⟩ here refl))) - ≡⟨ sym (remove-length (Injection.to xs⊑ys ⟨$⟩ here refl)) ⟩ - List.length ys ∎ where open ℕProp.≤-Reasoning - --- enumerations of the same set are permutations of each other -enumeration-bag-equals : ∀ {A} (enum₁ enum₂ : Enumeration A) → list enum₁ ∼[ bag ] list enum₂ -enumeration-bag-equals enum₁ enum₂ = record - { to = →-to-⟶ (λ _ → complete enum₂ _) - ; from = →-to-⟶ (λ _ → complete enum₁ _) - ; inverse-of = record - { left-inverse-of = λ _ → entries-unique enum₁ _ _ - ; right-inverse-of = λ _ → entries-unique enum₂ _ _ } } - --- as a consequence, they are equal in length -enumeration-length-uniform : ∀ {A} (enum₁ enum₂ : Enumeration A) → List.length (list enum₁) ≡ List.length (list enum₂) -enumeration-length-uniform enum₁ enum₂ = ℕProp.≤-antisym - (subbag-length-≤ (bag-=⇒ (enumeration-bag-equals enum₁ enum₂))) - (subbag-length-≤ (bag-=⇒ (enumeration-bag-equals enum₂ enum₁))) - - --- next, let's go the other way: lists with as many unique elements as an Enumeration are complete. -private - -- we need decidable equality in order to find the indices in our list where each element lives. thankfully, we can derive that from the Enumeration. - index-≡ : ∀ {A : Set} {xs : List A} {x y} (ix : x ∈ xs) (iy : y ∈ xs) → Any.index ix ≡ Any.index iy → x ≡ y - index-≡ (here refl) (here refl) i-≡ = refl - index-≡ (here _) (there _) () - index-≡ (there _) (here _) () - index-≡ (there ix) (there iy) i-≡ = index-≡ ix iy (FinProp.suc-injective i-≡) - - enumerable-≟ : ∀ {A} (enum : Enumeration A) → Decidable₂ (_≡_ {A = A}) - enumerable-≟ enum a b = Decidable.map′ (index-≡ _ _) (λ { refl → refl }) (Any.index (complete enum a) FinProp.≟ Any.index (complete enum b)) - - -- if a list is missing any elements, we can show it must be shorter than an Enumeration: - -- when we add the missing element it's still a subbag of the Enumeration, so it's shorter by at least one - strict-subbag-extend : ∀ {A : Set} {a : A} {xs ys} → a ∉ xs → a ∈ ys → xs ∼[ subbag ] ys → a ∷ xs ∼[ subbag ] ys - strict-subbag-extend a∉xs a∈ys xs⊑ys = record - { to = →-to-⟶ λ - { (here refl) → a∈ys - ; (there x∈xs) → Injection.to xs⊑ys ⟨$⟩ x∈xs } - ; injective = λ - { {here refl} {here refl} refl → refl - ; {here refl} {there x∈xs} images-≡ → ⊥-elim (a∉xs x∈xs) - ; {there x∈xs} {here refl} images-≡ → ⊥-elim (a∉xs x∈xs) - ; {there x∈xs₁} {there x∈xs₂} images-≡ → cong there (Injection.injective xs⊑ys images-≡) } } - - strict-subbag-length : ∀ {A : Set} {a : A} {xs ys} → a ∉ xs → a ∈ ys → xs ∼[ subbag ] ys → List.length xs ℕ.< List.length ys - strict-subbag-length {a = a} {xs} {ys} a∉xs a∈ys xs⊑ys = begin - List.length xs - <⟨ ℕProp.≤-refl ⟩ - List.length (a ∷ xs) - ≤⟨ subbag-length-≤ (strict-subbag-extend a∉xs a∈ys xs⊑ys) ⟩ - List.length ys ∎ where open ℕProp.≤-Reasoning - - unique-list-enumeration-subbag : ∀ {A} (enum : Enumeration A) (xs : List A) → (∀ {x} (ix₁ ix₂ : x ∈ xs) → ix₁ ≡ ix₂) → xs ∼[ subbag ] list enum - unique-list-enumeration-subbag enum xs xs-unique = record - { to = →-to-⟶ λ _ → complete enum _ - ; injective = λ _ → xs-unique _ _ } - -long-list-complete : ∀ {A} (enum : Enumeration A) (xs : List A) → (∀ {x} (ix₁ ix₂ : x ∈ xs) → ix₁ ≡ ix₂) → List.length xs ≡ List.length (list enum) → ∀ x → x ∈ xs -long-list-complete enum xs xs-unique lengths-≡ x with Any.any (enumerable-≟ enum x) xs -... | yes x∈xs = x∈xs -... | no x∉xs = ⊥-elim (ℕProp.<-irrefl lengths-≡ (strict-subbag-length x∉xs (complete enum x) (unique-list-enumeration-subbag enum xs xs-unique))) - - --- finally, we build towards the ability to enumerate neighboring tiles on a grid - -private - fsuc-Injection : ∀ {n} → Fin n ↣ Fin (suc n) - fsuc-Injection = record - { to = →-to-⟶ suc - ; injective = FinProp.suc-injective } - - tabulate⁻-injective : ∀ {A : Set} {n} (f : Fin n ↣ A) → ∀ {x} (ix₁ ix₂ : x ∈ List.tabulate (λ y → Injection.to f ⟨$⟩ y)) → ix₁ ≡ ix₂ - tabulate⁻-injective {n = zero} f () () - tabulate⁻-injective {n = suc n} f (here refl) (here refl) = refl - tabulate⁻-injective {n = suc n} f (here x≡fz) (there ix₂) with AnyProp.tabulate⁻ ix₂ - ... | _ , x≡fs with Injection.injective f (trans (sym x≡fz) (x≡fs)) - ... | () - tabulate⁻-injective {n = suc n} f (there ix₁) (here x≡fz) with AnyProp.tabulate⁻ ix₁ - ... | _ , x≡fs with Injection.injective f (trans (sym x≡fz) (x≡fs)) - ... | () - tabulate⁻-injective {n = suc n} f (there ix₁) (there ix₂) = cong there (tabulate⁻-injective (f Injection.∘ fsuc-Injection) ix₁ ix₂) - -allFin : ∀ n → Enumeration (Fin n) -allFin n = record - { list = List.allFin n - ; complete = λ i → AnyProp.tabulate⁺ i refl - ; entries-unique = tabulate⁻-injective Injection.id } + -- for a constructive proof we have to find the `n` for which `f n ≡ m` for each `m`. + -- conveniently, Fin.pigeonhole also gives us that: if we extend `f` with a duplicate mapping to `m`, + -- then Fin.pigeonhole finds the other one. there are no other duplicates because f is injective. + g⁻¹ : ∀ m → ∃ λ n → Injection.to g ⟨$⟩ n ≡ m + g⁻¹ m with Fin.pigeonhole ℕ.≤-refl λ { zero → m ; (suc i) → Injection.to g ⟨$⟩ i } + g⁻¹ m | zero , zero , zero≢zero , m≡m = contradiction ≡.refl zero≢zero + g⁻¹ m | zero , suc j , zero≢sucj , m≡gj = j , ≡.sym m≡gj + g⁻¹ m | suc i , zero , suci≢zero , gi≡m = i , gi≡m + g⁻¹ m | suc i , suc j , suci≢sucj , gi≡gj = contradiction (≡.cong suc (Injection.injective g gi≡gj)) suci≢sucj + + translateIndex-f↣enum : Fin (cardinality enum) ↣ Fin (cardinality enum) + translateIndex-f↣enum = Inverse.injection (sym↔ (lookup enum)) ∘↢ f + translateIndex-enum⟶f : Fin.setoid (cardinality enum) ⟶ Fin.setoid (cardinality enum) + translateIndex-enum⟶f = Surjective.from (fin-injection-surjective translateIndex-f↣enum) -private - module Product {A B} (enum₁ : Enumeration A) (enum₂ : Enumeration B) where - open RawMonad (List.monad {Level.zero}) - product-list : List (A × B) - product-list = list enum₁ ⊗ list enum₂ +-- if we have two setoids, a pair of inverse functions between them, and Enumeration for one, we can get an Enumeration of the same cardinality for the other +map : ∀ {a b ℓ₁ ℓ₂} {A : Setoid a ℓ₁} {B : Setoid b ℓ₂} (f : Inverse A B) → Enumeration A → Enumeration B +map f enum = record + { cardinality = cardinality enum + ; lookup = f ∘↔ lookup enum } + - product-complete : ∀ xy → xy ∈ product-list - product-complete (x , y) = Inverse.to ∈Prop.⊗-∈↔ ⟨$⟩ (complete enum₁ x , complete enum₂ y) +-- next, we build towards the ability to enumerate neighboring tiles on a grid + +-- to number the rows and columns of the board, we use allFin +allFin : ∀ n → Enumeration (Fin.setoid n) +allFin n = record + { cardinality = n + ; lookup = id↔ } + + +-- _⊗_: +-- 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.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.Membership.Propositional + open import Data.List.Membership.Propositional.Properties + open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_) + + -- from what I can tell, the easiest way to witness a bijection `(Fin m × Fin n) ↔ Fin (m * n)`, + -- which we want in order to construct a product enumeration, seems to be a be indirectly through + -- Data.List.Membership.Propositional.Properties.⊗-∈↔ + -- so to that end, we want bijections `Fin n ↔ tt ∈ replicate n tt`, or equivalently + -- `tt ∈ tts ↔ Fin (length tts)` in order to utilize it + + abstract + private + module _ {ℓ} {T : Set ℓ} (t : T) (T-prop : ∀ t′ → t′ ≡ t) where + ∈-lookup′ : ∀ {ts} → Fin (length ts) → t ∈ ts + ∈-lookup′ {ts} i = ≡.subst (_∈ ts) (T-prop (List.lookup ts i)) (∈-lookup ts i) + + index∘∈-lookup : (ts : List T) (i : Fin (length ts)) → index (∈-lookup ts i) ≡ i + index∘∈-lookup [] () + index∘∈-lookup (t ∷ ts) zero = ≡.refl + index∘∈-lookup (t ∷ ts) (suc i) = ≡.cong suc (index∘∈-lookup ts i) + + index∘∈-lookup′ : ∀ {ts : List T} (i : Fin (length ts)) → index (∈-lookup′ {ts} i) ≡ i + index∘∈-lookup′ {ts} i with T-prop (List.lookup ts i) + index∘∈-lookup′ {ts} i | ≡.refl = index∘∈-lookup ts i + + ∈-lookup∘index : ∀ {ts} (t∈ts : t ∈ ts) → ∈-lookup ts (index t∈ts) ≅ t∈ts + ∈-lookup∘index (here ≡.refl) = ≅.refl + ∈-lookup∘index {t′ ∷ ts} (there t∈ts) = ≅.icong (_∈ ts) (T-prop _) there (∈-lookup∘index t∈ts) + + ∈-lookup′∘index : ∀ {ts} (t∈ts : t ∈ ts) → ∈-lookup′ (index t∈ts) ≡ t∈ts + ∈-lookup′∘index {ts} t∈ts with ∈-lookup∘index t∈ts + ... | ∈-lookup∘index≅id with index t∈ts + ... | i with T-prop (List.lookup ts i) + ∈-lookup′∘index {ts} t∈ts | ≅.refl | i | ≡.refl = ≡.refl + + index↔ : ∀ {ts} → t ∈ ts ↔ Fin (length ts) + index↔ = record + { to = →-to-⟶ index + ; from = →-to-⟶ ∈-lookup′ + ; inverse-of = record + { left-inverse-of = ∈-lookup′∘index + ; right-inverse-of = index∘∈-lookup′ } } + + index↔′ : ∀ {n} → t ∈ replicate n t ↔ Fin n + index↔′ {n} = ≡.subst (λ m → t ∈ replicate n t ↔ Fin m) (length-replicate n) (index↔ {replicate n t}) + + _⊗_ : Enumeration A → Enumeration B → Enumeration (×-setoid A B) + enum₁ ⊗ enum₂ = record + { cardinality = _ -- incidentally (and not proven here), this is `cardinality enum₁ * cardinality enum₂` + ; lookup = + (lookup enum₁ ×-inverse lookup enum₂) ∘↔ + sym↔ Pointwise-≡↔≡ ∘↔ + index↔′ tt (λ { tt → ≡.refl }) ×-↔ index↔′ tt (λ { tt → ≡.refl }) ∘↔ + sym↔ ⊗-∈↔ ∘↔ + sym↔ (index↔ (tt , tt) (λ { (tt , tt) → ≡.refl })) } + + +-- filter: +-- to enumerate the neighbors of a tile, or the mines or safe tiles neighboring a tile, +-- we filter the enumeration of all coordinates to just the ones satisfying an appropriate prdciate +count : ∀ {a p m} {A : Set a} {P : A → Set p} → Decidable P → (Fin m → A) → ℕ +count {m = zero} P? f = zero +count {m = suc m} P? f with P? (f zero) +... | yes Pz = suc (count P? (f ∘ suc)) +... | no ¬Pz = count P? (f ∘ suc) + +count-≡ : ∀ {a b p q m} {A : Set a} {B : Set b} {P : A → Set p} {Q : B → Set q} + (P? : Decidable P) (Q? : Decidable Q) (f : Fin m → A) (g : Fin m → B) → + (∀ i → P (f i) ⇔ Q (g i)) → count P? f ≡ count Q? g +count-≡ {m = zero} P? Q? f g Pf⇔Qg = ≡.refl +count-≡ {m = suc m} P? Q? f g Pf⇔Qg with P? (f zero) | Q? (g zero) +count-≡ {m = suc m} P? Q? f g Pf⇔Qg | yes Pfz | yes Qgz = ≡.cong suc (count-≡ P? Q? (f ∘ suc) (g ∘ suc) (Pf⇔Qg ∘ suc)) +count-≡ {m = suc m} P? Q? f g Pf⇔Qg | yes Pfz | no ¬Qgz = contradiction (Equivalence.to (Pf⇔Qg zero) ⟨$⟩ Pfz) ¬Qgz +count-≡ {m = suc m} P? Q? f g Pf⇔Qg | no ¬Pfz | yes Qgz = contradiction (Equivalence.from (Pf⇔Qg zero) ⟨$⟩ Qgz) ¬Pfz +count-≡ {m = suc m} P? Q? f g Pf⇔Qg | no ¬Pfz | no ¬Qgz = count-≡ P? Q? (f ∘ suc) (g ∘ suc) (Pf⇔Qg ∘ suc) + +filter′ : ∀ {a p m} {A : Set a} {P : A → Set p} (P? : Decidable P) (f : Fin m → A) → + Fin (count P? f) → ∃ P +filter′ {m = zero} P? f = λ () +filter′ {m = suc m} P? f with P? (f zero) +... | yes Pz = λ { zero → f zero , Pz + ; (suc i) → filter′ P? (f ∘ suc) i } +... | no ¬Pz = filter′ P? (f ∘ suc) + + +-- filter′ preserves Enumerations: +-- the result of filtering by a predicate P is an Enumeration of all elements satisfying P +module _ {a ℓ p} {A : Setoid a ℓ} {P : Setoid.Carrier A → Set p} where + open Setoid A + open import Relation.Binary.Reasoning.Setoid A + + private + ∃-setoid : Setoid (a ⊔ p) ℓ + ∃-setoid = On.setoid {B = ∃ P} A proj₁ + + module _ (P? : Decidable P) where + filter-index : ∀ {m} (f : Fin m → Carrier) (i : Fin m) → + P (f i) → ∃ λ i′ → proj₁ (filter′ P? f i′) ≈ f i + filter-index {zero} f () + filter-index {suc m} f i with P? (f zero) + filter-index {suc m} f zero | yes Pz = const (zero , refl) + filter-index {suc m} f (suc i) | yes Pz = Σ.map suc id ∘ filter-index (f ∘ suc) i + filter-index {suc m} f zero | no ¬Pz = ⊥-elim ∘ ¬Pz + filter-index {suc m} f (suc i) | no ¬Pz = filter-index (f ∘ suc) i + + filter-index-cong : ∀ {m} (f : Fin m → Carrier) {i j : Fin m} (Pfi : P (f i)) (Pfj : P (f j)) → + P Respects _≈_ → i ≡ j → proj₁ (filter-index f i Pfi) ≡ proj₁ (filter-index f j Pfj) + filter-index-cong {zero} f {} Pfi Pfj P-resp-≈ i≡j + filter-index-cong {suc m} f {i} Pfi Pfj P-resp-≈ ≡.refl with P? (f zero) + filter-index-cong {suc m} f {zero} Pfi Pfj P-resp-≈ ≡.refl | yes Pz = ≡.refl + filter-index-cong {suc m} f {suc i} Pfi Pfj P-resp-≈ ≡.refl | yes Pz = ≡.cong suc (filter-index-cong (f ∘ suc) Pfi Pfj P-resp-≈ ≡.refl) + filter-index-cong {suc m} f {zero} Pfi Pfj P-resp-≈ ≡.refl | no ¬Pz = ⊥-elim (¬Pz Pfi) + filter-index-cong {suc m} f {suc i} Pfi Pfj P-resp-≈ ≡.refl | no ¬Pz = filter-index-cong (f ∘ suc) Pfi Pfj P-resp-≈ ≡.refl + + unfilter-index : ∀ {m} (f : Fin m → Carrier) (i′ : Fin (count P? f)) → + ∃ λ i → proj₁ (filter′ P? f i′) ≈ f i + unfilter-index {zero} f () + unfilter-index {suc m} f i′ with P? (f zero) + unfilter-index {suc m} f zero | yes Pz = zero , refl + unfilter-index {suc m} f (suc i′) | yes Pz = Σ.map suc id (unfilter-index (f ∘ suc) i′) + unfilter-index {suc m} f i′ | no ¬Pz = Σ.map suc id (unfilter-index (f ∘ suc) i′) + + unfilter-index-injective : ∀ {m} (f : Fin m → Carrier) → + Injective (→-to-⟶ {B = Fin.setoid m} (proj₁ ∘ unfilter-index f)) + unfilter-index-injective {zero} f {} {} ui′≡uj′ + unfilter-index-injective {suc m} f {i′} {j′} ui′≡uj′ with P? (f zero) + unfilter-index-injective {suc m} f {zero} {zero} ui′≡uj′ | yes Pz = ≡.refl + unfilter-index-injective {suc m} f {zero} {suc j′} () | yes Pz + unfilter-index-injective {suc m} f {suc i′} {zero} () | yes Pz + unfilter-index-injective {suc m} f {suc i′} {suc j′} ui′≡uj′ | yes Pz = ≡.cong suc (unfilter-index-injective (f ∘ suc) (Fin.suc-injective ui′≡uj′)) + unfilter-index-injective {suc m} f {i′} {j′} ui′≡uj′ | no ¬Pz = unfilter-index-injective (f ∘ suc) (Fin.suc-injective ui′≡uj′) + + filter : Decidable P → P Respects _≈_ → Enumeration A → Enumeration ∃-setoid + filter P? P-resp-≈ enum = record + { cardinality = count P? enum-lookup + ; lookup = Inverse.fromBijection record + { to = →-to-⟶ (filter′ P? enum-lookup) + ; bijective = filter′-bijective } } + where + enum-lookup : Fin (cardinality enum) → Carrier + enum-lookup = Inverse.to (lookup enum) ⟨$⟩_ + + enum-index : Carrier → Fin (cardinality enum) + enum-index = Inverse.from (lookup enum) ⟨$⟩_ + + lookup∘index : ∀ x → enum-lookup (enum-index x) ≈ x + lookup∘index = Inverse.right-inverse-of (lookup enum) abstract - -- hide the internals of ⊗-∈↔ away from the typechecker so it doesn't diverge (?? agda bug ??) - ⊗-∈↔-abstract : ∀ {x y} → (x ∈ list enum₁ × y ∈ list enum₂) ↔ (x , y) ∈ product-list - ⊗-∈↔-abstract = ∈Prop.⊗-∈↔ - - split-∈ : ∀ {x y} → (x , y) ∈ product-list → x ∈ list enum₁ × y ∈ list enum₂ - split-∈ xy-ix = Inverse.from ⊗-∈↔-abstract ⟨$⟩ xy-ix - - pairs-unique : ∀ {x y} (ixs₁ ixs₂ : x ∈ list enum₁ × y ∈ list enum₂) → ixs₁ ≡ ixs₂ - pairs-unique (x-ix₁ , y-ix₁) (x-ix₂ , y-ix₂) with entries-unique enum₁ x-ix₁ x-ix₂ | entries-unique enum₂ y-ix₁ y-ix₂ - ... | refl | refl = refl - - product-unique : ∀ {xy} (xy-ix₁ xy-ix₂ : xy ∈ product-list) → xy-ix₁ ≡ xy-ix₂ - product-unique xy-ix₁ xy-ix₂ = Inverse.injective (Inverse.sym ⊗-∈↔-abstract) (pairs-unique (split-∈ xy-ix₁) (split-∈ xy-ix₂)) - -_⊗_ : ∀ {A B} → Enumeration A → Enumeration B → Enumeration (A × B) -enum₁ ⊗ enum₂ = record - { list = product-list - ; complete = product-complete - ; entries-unique = product-unique } - where open Product enum₁ enum₂ - - --- this is public since we define Σfilter ourself. it's convenient to see it elsewhere in order to write proofs about it -module Filter {A : Set} {P : A → Set} (P? : Decidable₁ P) where - Σfilter : List A → List (Σ A P) - Σfilter = List.mapMaybe (λ x → Maybe.map (x ,_) (Maybe.decToMaybe (P? x))) - - Σfilter-∈ : ∀ {xs x} → x ∈ xs → Irrelevant₁ P → (Px : P x) → (x , Px) ∈ Σfilter xs - Σfilter-∈ {x ∷ xs} (here refl) P-irrelevant Px with P? x - ... | yes Px′ rewrite P-irrelevant Px Px′ = here refl - ... | no ¬Px = contradiction Px ¬Px - Σfilter-∈ {y ∷ xs} (there x∈xs) P-irrelevant Px with P? y - ... | yes _ = there (Σfilter-∈ x∈xs P-irrelevant Px) - ... | no _ = Σfilter-∈ x∈xs P-irrelevant Px - - Σfilter-∋ : ∀ {xs x} (Px : P x) → (x , Px) ∈ Σfilter xs → x ∈ xs - Σfilter-∋ {[]} Px () - Σfilter-∋ {y ∷ xs} Px x∈xs with P? y - Σfilter-∋ {y ∷ xs} _ (here refl) | yes _ = here refl - Σfilter-∋ {y ∷ xs} Px (there x∈xs) | yes _ = there (Σfilter-∋ Px x∈xs) - ... | no _ = there (Σfilter-∋ Px x∈xs) - - Σfilter-∋-injective : ∀ {xs x} Px (ix₁ ix₂ : (x , Px) ∈ Σfilter xs) → Σfilter-∋ {xs} Px ix₁ ≡ Σfilter-∋ Px ix₂ → ix₁ ≡ ix₂ - Σfilter-∋-injective {[]} Px () () eq - Σfilter-∋-injective {y ∷ xs} Px ix₁ ix₂ eq with P? y - Σfilter-∋-injective {y ∷ xs} .p (here refl) (here refl) eq | yes p = refl - Σfilter-∋-injective {y ∷ xs} .p (here refl) (there ix₂) () | yes p - Σfilter-∋-injective {y ∷ xs} .p (there ix₁) (here refl) () | yes p - Σfilter-∋-injective {y ∷ xs} Px (there ix₁) (there ix₂) eq | yes p = cong there (Σfilter-∋-injective _ _ _ (AnyProp.there-injective eq)) - Σfilter-∋-injective {y ∷ xs} Px ix₁ ix₂ eq | no ¬p = Σfilter-∋-injective _ _ _ (AnyProp.there-injective eq) - -filter : ∀ {A : Set} {P : A → Set} → Irrelevant₁ P → Decidable₁ P → Enumeration A → Enumeration (Σ A P) -filter P-irrelevant P? enum = record - { list = Σfilter (list enum) - ; complete = λ { (x , Px) → Σfilter-∈ (complete enum x) P-irrelevant Px } - ; entries-unique = λ ix₁ ix₂ → Σfilter-∋-injective _ _ _ (entries-unique enum (Σfilter-∋ _ ix₁) (Σfilter-∋ _ ix₂)) } - where open Filter P? - - --- in order to reason about how the total number of neighbors a tile has equals the sum of its safe neighbors and mine-containing neighbors, --- we can `partition` its neighbors into separate enumerations of safe neighbors and mines -partition : ∀ {A} {P Q : A → Set} → Irrelevant₁ P → Irrelevant₁ Q → (∀ x → P x ⊎ Q x) → (∀ {x} → P x → ¬ Q x) → - Enumeration A → Enumeration (Σ A P) × Enumeration (Σ A Q) -partition P-irrelevant Q-irrelevant which? PQ-disjoint enum = filter P-irrelevant ([ yes , no ∘ flip PQ-disjoint ]′ ∘ which?) enum , filter Q-irrelevant ([ no ∘ PQ-disjoint , yes ]′ ∘ which?) enum - -length-partition : ∀ {A} {P Q : A → Set} (P-irrelevant : Irrelevant₁ P) (Q-irrelevant : Irrelevant₁ Q) (which? : ∀ x → P x ⊎ Q x) (PQ-disjoint : ∀ {x} → P x → ¬ Q x) enum → - List.length (list enum) ≡ List.length (list (Σ.proj₁ (partition P-irrelevant Q-irrelevant which? PQ-disjoint enum))) - ℕ.+ List.length (list (Σ.proj₂ (partition P-irrelevant Q-irrelevant which? PQ-disjoint enum))) -length-partition P-irrelevant Q-irrelevant which? PQ-disjoint enum = length-Σfilter (list enum) where - length-Σfilter : ∀ xs → List.length xs ≡ List.length (Filter.Σfilter ([ yes , no ∘ flip PQ-disjoint ]′ ∘ which?) xs) ℕ.+ List.length (Filter.Σfilter ([ no ∘ PQ-disjoint , yes ]′ ∘ which?) xs) - length-Σfilter [] = refl - length-Σfilter (x ∷ xs) with which? x - ... | inj₁ Px = cong suc (length-Σfilter xs) - ... | inj₂ Qx = trans (cong suc (length-Σfilter xs)) (sym (ℕProp.+-suc _ _)) - - --- if we have two types, a pair of inverse functions between them, and Enumeration for one, we can get an Enumeration of the same length for the other -map : ∀ {A B : Set} (f : A ↔ B) → Enumeration A → Enumeration B -map f enum = record - { list = List.map (Inverse.to f ⟨$⟩_) (list enum) - ; complete = λ b → subst (_∈ List.map (Inverse.to f ⟨$⟩_) (list enum)) (Inverse.right-inverse-of f b) (∈Prop.∈-map⁺ _ (complete enum (Inverse.from f ⟨$⟩ b))) - ; entries-unique = λ ix₁ ix₂ → Inverse.injective (Inverse.sym (∈Prop.map-∈↔ _)) (images-unique (Inverse.from (∈Prop.map-∈↔ _) ⟨$⟩ ix₁) (Inverse.from (∈Prop.map-∈↔ _) ⟨$⟩ ix₂)) } where - images-unique : ∀ {b} (ix₁ ix₂ : ∃ λ a → a ∈ list enum × b ≡ Inverse.to f ⟨$⟩ a) → ix₁ ≡ ix₂ - images-unique (a₁ , a₁∈enum , b≡fa₁) (a₂ , a₂∈enum , b≡fa₂) with Inverse.injective f (trans (sym b≡fa₁) (b≡fa₂)) - images-unique (a₁ , a₁∈enum , b≡fa₁) (.a₁ , a₂∈enum , b≡fa₂) | refl = cong (a₁ ,_) (cong₂ _,_ (entries-unique enum a₁∈enum a₂∈enum) (≡-irrelevant b≡fa₁ b≡fa₂)) - -length-map : ∀ {A B : Set} (f : A ↔ B) (enum : Enumeration A) → List.length (list (map f enum)) ≡ List.length (list enum) -length-map f enum = ListProp.length-map (Inverse.to f ⟨$⟩_) (list enum) + filter′-bijective : Bijective (→-to-⟶ (filter′ P? enum-lookup)) + filter′-bijective = record + { injective = λ {i′} {j′} f′i′≈f′j′ → + unfilter-index-injective P? enum-lookup + (Inverse.injective (lookup enum) + (begin + enum-lookup (proj₁ (unfilter-index P? enum-lookup i′)) ≈⟨ sym (proj₂ (unfilter-index P? enum-lookup i′)) ⟩ + proj₁ (filter′ P? enum-lookup i′) ≈⟨ f′i′≈f′j′ ⟩ + proj₁ (filter′ P? enum-lookup j′) ≈⟨ proj₂ (unfilter-index P? enum-lookup j′) ⟩ + enum-lookup (proj₁ (unfilter-index P? enum-lookup j′)) ∎)) + ; surjective = record + { from = record + { _⟨$⟩_ = λ { (x , Px) → + proj₁ (filter-index P? enum-lookup + (enum-index x) + (P-resp-≈ (sym (lookup∘index x)) Px)) } + ; cong = λ { {x , Px} {y , Py} x≈y → + filter-index-cong P? enum-lookup + (P-resp-≈ (sym (lookup∘index x)) Px) + (P-resp-≈ (sym (lookup∘index y)) Py) + P-resp-≈ + (Π.cong (Inverse.from (lookup enum)) x≈y) } } + ; right-inverse-of = λ { (x , Px) → + begin + _ ≈⟨ proj₂ (filter-index P? enum-lookup (enum-index x) (P-resp-≈ (sym (lookup∘index x)) Px)) ⟩ + enum-lookup (enum-index x) ≈⟨ lookup∘index x ⟩ + x ∎ } } } + + +-- the total number of neighbors a tile has equals the sum of its safe neighbors and mine-containing neighbors. +-- in general, given an enumeration of a setoid, an enumeration of its elements satisfying a predicate, and another +-- of those satisfying its negation, the cardinality of the whole setoid will equal the sum of the cardinalities of +-- the two parts. +module _ {a ℓ p} {A : Setoid a ℓ} {P : Setoid.Carrier A → Set p} (P? : Decidable P) (P-resp-≈ : P Respects (Setoid._≈_ A)) where + open import Relation.Binary.Consequences using (P-resp⟶¬P-resp) + + filter¬ : Enumeration A → Enumeration (On.setoid {B = ∃ (¬_ ∘ P)} A proj₁) + filter¬ = filter (¬? ∘ P?) (P-resp⟶¬P-resp {P = P} (Setoid.sym A) P-resp-≈) + + cardinality-filter : ∀ enum → + cardinality enum ≡ cardinality (filter P? P-resp-≈ enum) ℕ.+ cardinality (filter¬ enum) + cardinality-filter enum = count-partition′ (Inverse.to (lookup enum) ⟨$⟩_) where + count-partition′ : ∀ {m} (f : Fin m → Setoid.Carrier A) → m ≡ count P? f ℕ.+ count (¬? ∘ P?) f + count-partition′ {zero} f = ≡.refl + count-partition′ {suc m} f with P? (f zero) + count-partition′ {suc m} f | yes Pz = ≡.cong suc (count-partition′ (f ∘ suc)) + count-partition′ {suc m} f | no ¬Pz = ≡.trans (≡.cong suc (count-partition′ (f ∘ suc))) (≡.sym (ℕ.+-suc _ _)) + +cardinality-partition : ∀ {a ℓ p} {A : Setoid a ℓ} {P : Setoid.Carrier A → Set p} (P-resp-≈ : P Respects (Setoid._≈_ A)) + (enumA : Enumeration A) + (enum∃P : Enumeration (On.setoid {B = ∃ P} A proj₁)) + (enum∃¬P : Enumeration (On.setoid {B = ∃ (¬_ ∘ P)} A proj₁)) → + cardinality enumA ≡ cardinality enum∃P ℕ.+ cardinality enum∃¬P +cardinality-partition {A = A} {P = P} P-resp-≈ enumA enum∃P enum∃¬P = begin + cardinality enumA ≡⟨ cardinality-filter P? P-resp-≈ enumA ⟩ + cardinality (filter P? P-resp-≈ enumA) ℕ.+ cardinality (filter¬ P? P-resp-≈ enumA) ≡⟨ ≡.cong₂ ℕ._+_ + (cardinality-≡ (filter P? P-resp-≈ enumA) enum∃P) + (cardinality-≡ (filter¬ P? P-resp-≈ enumA) enum∃¬P) ⟩ + cardinality enum∃P ℕ.+ cardinality enum∃¬P ∎ + where + open ≡.≡-Reasoning + open Setoid A + + _≈?_ : Decidable₂ _≈_ + _≈?_ = Decidable.via-injection (Inverse.injection (sym↔ (lookup enumA))) Fin._≟_ + + P? : Decidable P + P? x with Fin.any? ((_≈? x) ∘ proj₁ ∘ (Inverse.to (lookup enum∃P) ⟨$⟩_)) + P? x | yes ∃i = yes (P-resp-≈ (proj₂ ∃i) (proj₂ (Inverse.to (lookup enum∃P) ⟨$⟩ proj₁ ∃i))) + P? x | no ¬∃i = no (¬∃i ∘ λ Px → Inverse.from (lookup enum∃P) ⟨$⟩ (x , Px) , Inverse.right-inverse-of (lookup enum∃P) (x , Px)) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index 519881a..15adb28 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -6,7 +6,6 @@ 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 @@ -90,7 +89,7 @@ known-↝▣⇒≡ refl (↝▣known _) = refl -- `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) + Σ[ 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]✓ diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda index 7b928f9..7dfe5f8 100644 --- a/Minesweeper/Reasoning.agda +++ b/Minesweeper/Reasoning.agda @@ -4,29 +4,32 @@ module Minesweeper.Reasoning where open import Relation.Nullary +open import Relation.Binary open import Relation.Binary.PropositionalEquality open import Data.Empty -open import Data.List as List using (List; []; _∷_) -open import Data.List.Relation.Unary.All as All using (All; []; _∷_) -open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any) -open import Data.List.Relation.Unary.Any as Any using (Any; here; there) -open import Data.List.Relation.Unary.Any.Properties using (there-injective) -open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_) -open import Data.List.Membership.Propositional open import Data.Product as Σ open import Data.Product.Properties +open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡) open import Data.Nat open import Data.Nat.Properties +open import Data.Fin.Properties as Fin +open import Data.Fin using (Fin; zero; suc) open import Function -open import Function.Inverse as Inverse using (_↔_) +open import Function.Equality using (_⟨$⟩_) +open import Function.Equivalence using (_⇔_; equivalence) +open import Function.Injection as Injection using (Injection) +open import Function.Surjection as Surjection using (Surjective) +open import Function.Inverse as Inverse using (Inverse) -open import Data.Fin using (Fin) open import Minesweeper.Enumeration as Enum using (Enumeration) -open import Minesweeper.Coords as Coords using (Coords ; Neighbor ; neighbors) +open import Minesweeper.Coords as Coords using (Coords ; Neighbor) open import Minesweeper.Board as Board using (Board ; _Neighboring_on_ ; lookup ; _[_]≔_) open import Minesweeper.Rules open import Minesweeper.Moves +open Enumeration using (cardinality) + + -- our inductive family for minesweeper proofs! data _[_]↝★_ {bounds} (grid : Board Tile bounds) (coords : Coords bounds) : Guess → Set record Contradiction {bounds} (grid : Board Tile bounds) : Set @@ -40,9 +43,9 @@ record Contradiction {bounds} grid where coords : Coords bounds supposedMineCount : ℕ coords-mineCount : lookup coords grid ≡ known (safe supposedMineCount) - neighborGuesses : List Guess - neighborsKnown★ : Pointwise (λ neighbor guess → grid [ proj₁ neighbor ]↝★ guess) (Enumeration.list (neighbors coords)) neighborGuesses - disparity : supposedMineCount ≢ List.length (List.filter (mine⚐ ≟⚐_) neighborGuesses) + 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 @@ -82,142 +85,125 @@ data _[_]↝★_ {bounds} grid coords where ★⇒✓ grid coords (exfalso★ guess contradiction) grid′ grid↝⊞grid′ grid′✓ = ⊥-elim (disparity (begin supposedMineCount ≡⟨ testCoords-mineCount✓ ⟩ - List.length (Enumeration.list (neighboringMines grid′ testCoords)) - ≡⟨ mineCountsConsistent neighborsKnown★ ⟩ - List.length (List.filter (mine⚐ ≟⚐_) neighborGuesses) ∎)) + cardinality (neighboringMines grid′ testCoords) + ≡⟨ Enum.count-≡ _ _ _ _ (λ i → guesses-agree✓ (★⇒✓ _ _ (neighborsKnown★ i) _ grid↝⊞grid′ grid′✓)) ⟩ + Enum.count (mine⚐ ≟⚐_) neighborGuesses ∎)) where open ≡-Reasoning open Contradiction contradiction renaming (coords to testCoords ; coords-mineCount to testCoords-mineCount) - open Enum.Filter {A = Neighbor testCoords} (λ { (neighbor , _) → mine⚐ ⚐✓? (lookup neighbor grid′) }) renaming (Σfilter to filterMines) - - mineCountsConsistent : ∀ {neighbors : List (Neighbor testCoords)} {guesses} → Pointwise (λ neighbor guess → grid [ proj₁ neighbor ]↝★ guess) neighbors guesses → - List.length (filterMines neighbors) ≡ List.length (List.filter (mine⚐ ≟⚐_) guesses) - mineCountsConsistent [] = refl - mineCountsConsistent {(neighbor , _) ∷ _} (neighbor↝★guess ∷ _) with mine⚐ ⚐✓? (lookup neighbor grid′) | ★⇒✓ _ _ neighbor↝★guess _ grid↝⊞grid′ grid′✓ - mineCountsConsistent {(neighbor , _) ∷ _} (_ ∷ _) | yes mine⚐✓tile | guess⚐✓tile with lookup neighbor grid′ - mineCountsConsistent (_ ∷ neighbors↝★guesses) | yes ⚐✓mine | ⚐✓mine | .mine = cong suc (mineCountsConsistent neighbors↝★guesses) - mineCountsConsistent {(neighbor , _) ∷ _} (_ ∷ _) | no ¬mine⚐✓tile | guess⚐✓tile with lookup neighbor grid′ | ¬-⚐✓-invert ¬mine⚐✓tile - 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)) + + guesses-agree✓ : ∀ {guess tile} → guess ⚐✓ tile → mine⚐ ⚐✓ tile ⇔ mine⚐ ≡ guess + guesses-agree✓ ⚐✓mine = equivalence (const refl) (const ⚐✓mine) + guesses-agree✓ (⚐✓safe n) = equivalence (λ ()) (λ ()) + + testCoords-mineCount✓ : supposedMineCount ≡ cardinality (neighboringMines grid′ testCoords) 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)) + ... | mines′ , supposedMineCount≡cardinality-mines′ = + trans supposedMineCount≡cardinality-mines′ (Enum.cardinality-≡ mines′ (neighboringMines grid′ testCoords)) -- now we'll also show that some familiar reasoning principles used in proofsweeper are sound -- (and thus as a corrollary of the completeness of `_[_]↝★_`, they can be expressed in terms of those rules). +-- specifically, we want to capture that if you have a known safe tile that already has as many adjacent safe +-- tiles or mines as it can, then any other tile neighboring it must be of the other sort. for representing +-- that conveniently, here's the following record: a given number of unique neighbors of a tile, all either +-- safe or mines, excluding some other tile (which we wish to prove is of the opposite type) +record _Unique_Neighboring_on_Excluding_ {bounds} (count : ℕ) (guess : Guess) (coords : Coords bounds) (grid : Board Tile bounds) (other : Coords bounds) : Set where + field + neighbors : Injection (Fin.setoid count) (Neighbor coords) + neighbors↝✓guess : ∀ i → grid [ proj₁ (Injection.to neighbors ⟨$⟩ i) ]↝✓ guess + other∉neighbors : ∀ i → proj₁ (Injection.to neighbors ⟨$⟩ i) ≢ other + -- our core lemma: if a list of mines or safe tiles neighboring some coordinates agrees in length with the -- complete list of such neighboring tiles in a filled board, then any other neighbor not in that list -- must be of the opposite tile type -neighborsAlreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coords (other : Neighbor coords) guess +neighborsAlreadyFull : ∀ {bounds} (grid : Board Tile bounds) grid′ coords (other : Setoid.Carrier (Neighbor coords)) guess (every : Enumeration ((guess ⚐✓_) Neighboring coords on grid′)) → - (neighbors : List (Neighbor coords)) → - (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighbors) → ix₁ ≡ ix₂) → - All (λ neighbor → grid [ proj₁ neighbor ]↝✓ guess) neighbors → - All (λ neighbor → proj₁ other ≢ proj₁ neighbor) neighbors → - grid ↝⊞ grid′ → grid′ ✓ → - List.length neighbors ≡ List.length (Enumeration.list every) → + cardinality every Unique guess Neighboring coords on grid Excluding proj₁ other → + grid ↝⊞ grid′ → + grid′ ✓ → invert⚐ guess ⚐✓ lookup (proj₁ other) grid′ -neighborsAlreadyFull grid grid′ coords other guess every neighbors neighbors-unique neighbors↝✓guess other∉neighbors grid↝⊞grid′ grid′✓ lengths-agree = ¬-⚐✓-invert ¬other↦guess where - -- to see that `neighbors` is the complete list of `coords`' neighbors of type `guess`, we first need to inductively verify✓ that `guess` indeed holds for them. - neighbors★⇒✓ : ∀ {neighbors : List (Neighbor coords)} → All (λ elem → grid [ proj₁ elem ]↝✓ guess) neighbors → List ((guess ⚐✓_) Neighboring coords on grid′) - neighbors★⇒✓ {_} [] = [] - neighbors★⇒✓ {neighbor ∷ _} (neighbor↝✓guess ∷ neighbors↝✓guess) = (neighbor , neighbor↝✓guess grid′ grid↝⊞grid′ grid′✓) ∷ neighbors★⇒✓ neighbors↝✓guess - - neighbors✓ : List (Σ[ neighbor ∈ Neighbor coords ] (guess ⚐✓ lookup (proj₁ neighbor) grid′)) - neighbors✓ = neighbors★⇒✓ neighbors↝✓guess - - -- `neighbors✓` has unique entries since `neighbors` does. we need a couple helpers first to see the connection, though - ∈-neighbors★⇒✓⁻ : ∀ {neighbors neighbor neighbor✓} neighbors-valid★ → - (neighbor , neighbor✓) ∈ neighbors★⇒✓ {neighbors} neighbors-valid★ → - neighbor ∈ neighbors - ∈-neighbors★⇒✓⁻ [] () - ∈-neighbors★⇒✓⁻ (_ ∷ neighbors-valid★) (here refl) = here refl - ∈-neighbors★⇒✓⁻ (_ ∷ neighbors-valid★) (there ix) = there (∈-neighbors★⇒✓⁻ neighbors-valid★ ix) - - ∈-neighbors★⇒✓⁻-injective : ∀ {neighbors neighbor✓} neighbors-valid★ (ix₁ ix₂ : neighbor✓ ∈ neighbors★⇒✓ {neighbors} neighbors-valid★) → - ∈-neighbors★⇒✓⁻ neighbors-valid★ ix₁ ≡ ∈-neighbors★⇒✓⁻ neighbors-valid★ ix₂ → - ix₁ ≡ ix₂ - ∈-neighbors★⇒✓⁻-injective [] () ix₂ ★⇒✓⁻₁≡★⇒✓⁻₂ - ∈-neighbors★⇒✓⁻-injective (_ ∷ neighbors-valid★) (here refl) (here refl) ★⇒✓⁻₁≡★⇒✓⁻₂ = refl - ∈-neighbors★⇒✓⁻-injective (_ ∷ neighbors-valid★) (here refl) (there _) () - ∈-neighbors★⇒✓⁻-injective (_ ∷ neighbors-valid★) (there _) (here refl) () - ∈-neighbors★⇒✓⁻-injective (_ ∷ neighbors-valid★) (there ix₁) (there ix₂) ★⇒✓⁻₁≡★⇒✓⁻₂ = cong there (∈-neighbors★⇒✓⁻-injective neighbors-valid★ ix₁ ix₂ (there-injective ★⇒✓⁻₁≡★⇒✓⁻₂)) - - neighbors✓-unique : ∀ {neighbor✓} (ix₁ ix₂ : neighbor✓ ∈ neighbors✓) → ix₁ ≡ ix₂ - neighbors✓-unique ix₁ ix₂ = ∈-neighbors★⇒✓⁻-injective _ ix₁ ix₂ (neighbors-unique (∈-neighbors★⇒✓⁻ _ ix₁) (∈-neighbors★⇒✓⁻ _ ix₂)) - - -- `neighbors★⇒✓` preserves length so `neighbor✓` is the same length as `Neighbors★.list neighbors★` - length-neighbors★⇒✓ : ∀ {neighbors} neighbors-valid★ → List.length (neighbors★⇒✓ {neighbors} neighbors-valid★) ≡ List.length neighbors - length-neighbors★⇒✓ [] = refl - length-neighbors★⇒✓ (_ ∷ neighbors★-valid) = cong suc (length-neighbors★⇒✓ neighbors★-valid) - - -- because its elements are unique and it's as long as the complete list of all neighbors of type `guess`, `neighbors✓` is also complete - neighbors✓-complete : ∀ neighbor✓ → neighbor✓ ∈ neighbors✓ - neighbors✓-complete = Enum.long-list-complete every neighbors✓ neighbors✓-unique (begin - List.length neighbors✓ - ≡⟨ length-neighbors★⇒✓ neighbors↝✓guess ⟩ - List.length neighbors - ≡⟨ lengths-agree ⟩ - List.length (Enumeration.list every) ∎) - where open ≡-Reasoning - - -- `other` is not of type `guess`: it isn't in `neighbors`, so it isn't in `neighbors✓`, which is complete +neighborsAlreadyFull grid grid′ coords other guess every neighbors′ grid↝⊞grid′ grid′✓ = ¬-⚐✓-invert ¬other↦guess where + open _Unique_Neighboring_on_Excluding_ neighbors′ + + -- by observing that `neighbors`'s elements are of type `guess` and there are as many of them as there are neighbors of `coords` in `grid′`, + -- we can see that `neighbors` contains every `guess`-type neighbor of `coords` + neighbors✓ : Injection (Fin.setoid (cardinality every)) ((guess ⚐✓_) Neighboring coords on grid′) + neighbors✓ = record + { to = →-to-⟶ λ i → Injection.to neighbors ⟨$⟩ i , neighbors↝✓guess i grid′ grid↝⊞grid′ grid′✓ + ; injective = Injection.injective neighbors } + + neighbors✓-full : Surjective (Injection.to neighbors✓) + 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 other↦guess = All¬⇒¬Any other∉neighbors (Any.map (cong proj₁) (∈-neighbors★⇒✓⁻ _ (neighbors✓-complete (other , other↦guess)))) + ¬other↦guess other↦guess = other∉neighbors + (Surjective.from neighbors✓-full ⟨$⟩ (other , other↦guess)) + (≡×≡⇒≡ (Surjective.right-inverse-of neighbors✓-full (other , other↦guess))) -- from this we get that, given a safe tile with as many adjacent mines as it can have, its other neighbors must be safe otherNeighborIsSafe : ∀ {bounds} (grid : Board Tile bounds) neighborMineCount otherNeighbor - (safeCoords : (known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid) - (neighborMines : List (Neighbor (proj₁ (proj₁ safeCoords)))) → - (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighborMines) → ix₁ ≡ ix₂) → - All (λ neighbor → grid [ proj₁ neighbor ]↝✓ mine⚐) neighborMines → - All (λ neighbor → otherNeighbor ≢ proj₁ neighbor) neighborMines → - List.length neighborMines ≡ neighborMineCount → + (safeCoords : Setoid.Carrier ((known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid)) → + neighborMineCount Unique mine⚐ Neighboring proj₁ (proj₁ safeCoords) on grid Excluding otherNeighbor → grid [ otherNeighbor ]↝✓ safe⚐ -otherNeighborIsSafe grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborMines neighborMines-unique neighborMines↝✓mine⚐ otherNeighbor∉neighborMines neighborMines-length grid′ grid↝⊞grid′ grid′✓ +otherNeighborIsSafe grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborMines grid′ grid↝⊞grid′ grid′✓ with known-safe-✓ safeCoords grid grid′ (sym safeCoords-safe) grid↝⊞grid′ grid′✓ -... | mineEnumeration , neighborMineCount≡enumLength = - neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) mine⚐ mineEnumeration neighborMines neighborMines-unique neighborMines↝✓mine⚐ otherNeighbor∉neighborMines grid↝⊞grid′ grid′✓ enoughMines - where - enoughMines : List.length neighborMines ≡ List.length (Enumeration.list mineEnumeration) - enoughMines = trans neighborMines-length neighborMineCount≡enumLength - --- and likewise, given a safe tile with as many adjacent safe tiles as it can have, its other niehgbors must be mines +... | mineEnumeration , neighborMineCount≡enumCardinality = + neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) + mine⚐ + mineEnumeration + (subst _ neighborMineCount≡enumCardinality neighborMines) + grid↝⊞grid′ + grid′✓ + +-- and likewise, given a safe tile with as many adjacent safe tiles as it can have, its other neighbors must be mines otherNeighborIsMine : ∀ {bounds} (grid : Board Tile bounds) neighborMineCount otherNeighbor - (safeCoords : (known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid) - (neighborSafes : List (Neighbor (proj₁ (proj₁ safeCoords)))) → - (∀ {neighbor} (ix₁ ix₂ : neighbor ∈ neighborSafes) → ix₁ ≡ ix₂) → - All (λ neighbor → grid [ proj₁ neighbor ]↝✓ safe⚐) neighborSafes → - All (λ neighbor → otherNeighbor ≢ proj₁ neighbor) neighborSafes → - List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list (neighbors (proj₁ (proj₁ safeCoords)))) → + (safeCoords : Setoid.Carrier ((known (safe neighborMineCount) ≡_) Neighboring otherNeighbor on grid)) → + (Coords.neighborCount (proj₁ (proj₁ safeCoords)) ∸ neighborMineCount) Unique safe⚐ Neighboring proj₁ (proj₁ safeCoords) on grid Excluding otherNeighbor → grid [ otherNeighbor ]↝✓ mine⚐ -otherNeighborIsMine grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborSafes neighborSafes-unique neighborSafes↝✓safe⚐ otherNeighbor∉neighborSafes neighborSafes-length grid′ grid↝⊞grid′ grid′✓ +otherNeighborIsMine grid neighborMineCount otherNeighbor ((safeCoords , safeCoords-Adj) , safeCoords-safe) neighborSafes grid′ grid↝⊞grid′ grid′✓ with known-safe-✓ safeCoords grid grid′ (sym safeCoords-safe) grid↝⊞grid′ grid′✓ -... | mineEnumeration , neighborMineCount≡enumLength = - neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) safe⚐ safeEnumeration neighborSafes neighborSafes-unique neighborSafes↝✓safe⚐ otherNeighbor∉neighborSafes grid↝⊞grid′ grid′✓ enoughSafes +... | mineEnumeration , neighborMineCount≡enumCardinality = + neighborsAlreadyFull grid grid′ safeCoords (otherNeighbor , Coords.Adjacent-sym otherNeighbor safeCoords safeCoords-Adj) + safe⚐ + safeEnumeration + (subst (_Unique safe⚐ Neighboring safeCoords on grid Excluding otherNeighbor) enoughSafes neighborSafes) + grid↝⊞grid′ + grid′✓ where -- since the number of safe neighbors a tile has is defined by how many are left when you take away the mines, - -- we need to do a bit of arithmetic--splitting all of safeNeighbor's neighbors into safe tiles and mines--to see that our list really has all of them - splitNeighbors : Enumeration ((safe⚐ ⚐✓_) Neighboring safeCoords on grid′) × Enumeration ((mine⚐ ⚐✓_) Neighboring safeCoords on grid′) - splitNeighbors = Enum.partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeCoords) - + -- we need to do a bit of arithmetic--splitting all of safeNeighbor's neighbors into safe tiles and mines--to see that our list really has all of them. safeEnumeration : Enumeration ((safe⚐ ⚐✓_) Neighboring safeCoords on grid′) - safeEnumeration = proj₁ splitNeighbors - - enoughSafes : List.length neighborSafes ≡ List.length (Enumeration.list safeEnumeration) - enoughSafes = +-cancelʳ-≡ (List.length neighborSafes) (List.length (Enumeration.list safeEnumeration)) length-splitNeighbors where - open ≡-Reasoning - length-splitNeighbors : List.length neighborSafes + neighborMineCount ≡ List.length (Enumeration.list safeEnumeration) + neighborMineCount - length-splitNeighbors = begin - List.length neighborSafes + neighborMineCount - ≡⟨ neighborSafes-length ⟩ - List.length (Enumeration.list (neighbors safeCoords)) - ≡⟨ Enum.length-partition ⚐✓-irrelevance ⚐✓-irrelevance (tileType ∘ flip lookup grid′ ∘ proj₁) guessesDisjoint (neighbors safeCoords) ⟩ - List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list (proj₂ splitNeighbors)) - ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (Enum.enumeration-length-uniform (proj₂ splitNeighbors) mineEnumeration) ⟩ - List.length (Enumeration.list safeEnumeration) + List.length (Enumeration.list mineEnumeration) - ≡⟨ cong (List.length (Enumeration.list safeEnumeration) +_) (sym neighborMineCount≡enumLength) ⟩ - List.length (Enumeration.list safeEnumeration) + neighborMineCount ∎ + safeEnumeration = Board.filterNeighbors (safe⚐ ⚐✓?_) grid′ safeCoords + + -- Enum.cardinality-partition gives us that the number total number of neighbors a tile has equals the sum of its safe and non-safe neighbors. + -- this bijection gets us the rest of the way there: the non-safe neighbors and mines are the same: + mine⚐↔¬safe⚐ : Inverse ((mine⚐ ⚐✓_) Neighboring safeCoords on grid′) ((¬_ ∘ (safe⚐ ⚐✓_)) Neighboring safeCoords on grid′) + mine⚐↔¬safe⚐ = record + { to = record { _⟨$⟩_ = Σ.map₂ mine⚐⇒¬safe⚐ ; cong = id } + ; from = record { _⟨$⟩_ = Σ.map₂ ¬safe⚐⇒mine⚐ ; cong = id } + ; inverse-of = record + { left-inverse-of = λ _ → refl , refl + ; right-inverse-of = λ _ → refl , refl } } + where + mine⚐⇒¬safe⚐ : ∀ {tile} → mine⚐ ⚐✓ tile → ¬ safe⚐ ⚐✓ tile + mine⚐⇒¬safe⚐ ⚐✓mine () + ¬safe⚐⇒mine⚐ : ∀ {tile} → ¬ safe⚐ ⚐✓ tile → mine⚐ ⚐✓ tile + ¬safe⚐⇒mine⚐ {mine} ¬safe⚐ = ⚐✓mine + ¬safe⚐⇒mine⚐ {safe n} ¬safe⚐ = ⊥-elim (¬safe⚐ (⚐✓safe n)) + + enoughSafes : Coords.neighborCount safeCoords ∸ neighborMineCount ≡ cardinality safeEnumeration + enoughSafes = begin + Coords.neighborCount safeCoords ∸ neighborMineCount ≡⟨ cong (_∸ neighborMineCount) + (Enum.cardinality-partition + (subst ((safe⚐ ⚐✓_) ∘ flip lookup grid′) ∘ ≡×≡⇒≡) + (Coords.neighbors safeCoords) + safeEnumeration + (Enum.map mine⚐↔¬safe⚐ mineEnumeration)) ⟩ + cardinality safeEnumeration + cardinality mineEnumeration ∸ neighborMineCount ≡⟨ cong (cardinality safeEnumeration + cardinality mineEnumeration ∸_) + neighborMineCount≡enumCardinality ⟩ + cardinality safeEnumeration + cardinality mineEnumeration ∸ cardinality mineEnumeration ≡⟨ m+n∸n≡m (cardinality safeEnumeration) (cardinality mineEnumeration) ⟩ + cardinality safeEnumeration ∎ + where open ≡-Reasoning diff --git a/Minesweeper/Rules.agda b/Minesweeper/Rules.agda index 18c7d92..63cdb31 100644 --- a/Minesweeper/Rules.agda +++ b/Minesweeper/Rules.agda @@ -35,7 +35,7 @@ data _⚐✓_ : Guess → KnownTile → Set where _[_]✓ : ∀ {bounds} → Board KnownTile bounds → Coords bounds → Set _[_]✓ {bounds} grid coords with lookup coords grid ... | mine = ⊤ -... | safe n = Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) ] n ≡ length (Enumeration.list neighboringMines) +... | safe n = Σ[ neighboringMines ∈ Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) ] n ≡ Enumeration.cardinality neighboringMines -- a board is good if all positions on it are good _✓ : ∀ {bounds} → Board KnownTile bounds → Set @@ -48,17 +48,6 @@ mine⚐ ⚐✓? safe _ = no λ { () } safe⚐ ⚐✓? mine = no λ { () } safe⚐ ⚐✓? safe n = yes (⚐✓safe n) -tileType : ∀ tile → (safe⚐ ⚐✓ tile) ⊎ (mine⚐ ⚐✓ tile) -tileType mine = inj₂ ⚐✓mine -tileType (safe n) = inj₁ (⚐✓safe n) - -guessesDisjoint : ∀ {tile} → safe⚐ ⚐✓ tile → ¬ mine⚐ ⚐✓ tile -guessesDisjoint () ⚐✓mine - -⚐✓-irrelevance : Irrelevant₂ _⚐✓_ -⚐✓-irrelevance ⚐✓mine ⚐✓mine = refl -⚐✓-irrelevance (⚐✓safe n) (⚐✓safe .n) = refl - _≟⚐_ : Decidable₂ (_≡_ {A = Guess}) mine⚐ ≟⚐ mine⚐ = yes refl mine⚐ ≟⚐ safe⚐ = no λ () @@ -66,19 +55,19 @@ safe⚐ ≟⚐ mine⚐ = no λ () safe⚐ ≟⚐ safe⚐ = yes refl neighboringMines : ∀ {bounds} (grid : Board KnownTile bounds) (coords : Coords bounds) → Enumeration ((mine⚐ ⚐✓_) Neighboring coords on grid) -neighboringMines grid coords = Enum.filter ⚐✓-irrelevance (λ { (neighbor , _) → mine⚐ ⚐✓? (lookup neighbor grid) }) (neighbors coords) +neighboringMines = filterNeighbors (mine⚐ ⚐✓?_) _[_]✓? : ∀ {bounds} → Decidable₂ (_[_]✓ {bounds}) grid [ coords ]✓? with lookup coords grid ... | mine = yes tt -... | safe n with n ℕ.≟ length (Enumeration.list (neighboringMines grid coords)) +... | safe n with n ℕ.≟ Enumeration.cardinality (neighboringMines grid coords) ... | yes n≡len = yes (neighboringMines grid coords , n≡len) ... | no n≢len = no λ { (mines′ , n≡len) → n≢len (begin n ≡⟨ n≡len ⟩ - length (Enumeration.list mines′) - ≡⟨ Enum.enumeration-length-uniform mines′ (neighboringMines grid coords) ⟩ - length (Enumeration.list (neighboringMines grid coords)) ∎) } + Enumeration.cardinality mines′ + ≡⟨ Enum.cardinality-≡ mines′ (neighboringMines grid coords) ⟩ + Enumeration.cardinality (neighboringMines grid coords) ∎) } where open ≡-Reasoning _✓? : ∀ {bounds} → Decidable₁ (_✓ {bounds})