update agda to v2.6.0.1 and agda-stdlib to v1.1

I've also flipped the argument order of Minesweepeer.Board.lookup to agree with the new ordering used by Data.Vec.lookup, and I've made some implicit arguments explicit since they can't be inferred anymore.
dianne · Jul 6, 2019 · c56f3d2 · c56f3d2
1 parent 01ae0db
commit c56f3d2
Show file tree

Hide file tree

Showing 6 changed files with 78 additions and 75 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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))