well-founded induction on partially filled boards

this is the first step to proving our rules complete!
it shows that by repeatedly performing case analysis on a board,
we'll eventually consider every tile.

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

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 )