relationship between _≥_ and _↝⊞_

dianne · Jan 15, 2019 · 0c54565 · 0c54565
1 parent be365af
commit 0c54565
Showing 1 changed file with 11 additions and 0 deletions.
diff --git 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)