From 0c54565bc0b0ac5179139a12714f22ef9720f0bc Mon Sep 17 00:00:00 2001 From: dianne Date: Mon, 14 Jan 2019 22:09:42 -0800 Subject: [PATCH] =?UTF-8?q?relationship=20between=20=5F=E2=89=A5=5F=20and?= =?UTF-8?q?=20=5F=E2=86=9D=E2=8A=9E=5F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Minesweeper/Moves.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index 04c0c47..bd93d82 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -183,3 +183,14 @@ holey⊎filled grid with any (any unknown?) grid (∈.toAny (∈.∈-lookup (proj₂ coords) grid) (subst (_∈ Vec.lookup (proj₂ coords) grid) coords↦unknown (∈.∈-lookup (proj₁ coords) (Vec.lookup (proj₂ coords) grid))))) + + +-- _≥_ and _↝⊞_ obey a sort of transitivity: if you can fill in a board, then any more general board +-- can be filled the same way +≽-↝▣-trans : ∀ {filled holey} → filled ≽ holey → ∀ {definitelyFilled} → filled ↝▣ definitelyFilled → holey ↝▣ definitelyFilled +≽-↝▣-trans [ known≻unknown ] (↝▣known tile) = ↝▣unknown tile +≽-↝▣-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)