Tilings one exponential up
Lax822549.WideTilings · concepts/Lax822549/WideTilings.lean · lax-822549
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A tile system gives tiles, horizontal and vertical compatibilities, the tiles allowed on the first row and its edges, and accepting tiles. Over an instance of the wide tiling vocabulary, the system tiles the square whose sides are the addresses of the instance; the square tiling problem asks whether that square has a tiling, and the corridor tiling problem whether the corridor of width and unbounded height has one, both on a well-formed instance.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Algebra.BigOperators.Finprod |
| 2 | import Mathlib.Data.Set.Finite.Lemmas |
| 3 | import Mathlib.Data.Fintype.EquivFin |
| 4 | import Mathlib.Data.Set.Card |
| 5 | import Mathlib.SetTheory.Cardinal.Finite |
| 6 | import Mathlib.Logic.Equiv.Prod |
| 7 | import Mathlib.ModelTheory.Order |
| 8 | import Mathlib.ModelTheory.Semantics |
| 9 | import Mathlib.ModelTheory.Complexity |
| 10 | import Mathlib.Tactic.FinCases |
| 11 | import Mathlib.Order.PiLex |
| 12 | import Mathlib.Data.Prod.Lex |
| 13 | import Mathlib.Logic.Equiv.Fin.Basic |
| 14 | import Mathlib.Data.Finite.Sigma |
| 15 | import Mathlib.Data.Fintype.Lattice |
| 16 | import Mathlib.Order.Lattice.Nat |
| 17 | import Mathlib.Data.Fintype.Pigeonhole |
| 18 | import Mathlib.Dynamics.FixedPoints.Basic |
| 19 | import Lax822549.WideMachines |
| 20 | import Lax904597.Machines |
| 21 | import Lax904597.Problems |
| 22 | import Lax485149.Problems |
| 23 | |
| 24 | /-! |
| 25 | --- |
| 26 | title: Tilings one exponential up |
| 27 | type: definition |
| 28 | --- |
| 29 | A tile system gives tiles, horizontal and vertical compatibilities, the |
| 30 | tiles allowed on the first row and its edges, and accepting tiles. Over an |
| 31 | instance of the wide tiling vocabulary, the system tiles the square whose |
| 32 | sides are the addresses of the instance; the square tiling problem |
| 33 | asks whether that square has a tiling, and the corridor tiling problem |
| 34 | whether the corridor of width and unbounded height has one, both on a |
| 35 | well-formed instance. |
| 36 | -/ |
| 37 | |
| 38 | namespace Lax822549.WideTilings |
| 39 | |
| 40 | open Lax822549.WideMachines Lax904597.Machines |
| 41 | |
| 42 | section Ripple |
| 43 | |
| 44 | variable {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop} |
| 45 | |
| 46 | /-- `p` is a highest position. -/ |
| 47 | def MaxPos (Le : A → A → Prop) (Posn : A → Prop) (p : A) : Prop := |
| 48 | Posn p ∧ ∀ q, Posn q → Le q p |
| 49 | |
| 50 | end Ripple |
| 51 | |
| 52 | open FirstOrder |
| 53 | |
| 54 | open Language Structure |
| 55 | |
| 56 | /-- **A tile system**, read off an instance: the positions with their order, |
| 57 | the tiles with their compatibilities, the bottom row and the accepting tiles. |
| 58 | As with `TMData`, the record is a plain bundle of |
| 59 | predicates, so everything about tilings is stated once and read at whatever |
| 60 | structure supplies them. -/ |
| 61 | structure TileData (A : Type) where |
| 62 | /-- Being a position – a column, and equally a row. -/ |
| 63 | Posn : A → Prop |
| 64 | /-- The order on positions. -/ |
| 65 | Le : A → A → Prop |
| 66 | /-- Being a tile. -/ |
| 67 | Tile : A → Prop |
| 68 | /-- Being an accepting tile. -/ |
| 69 | Acc : A → Prop |
| 70 | /-- The right neighbor may carry this tile. -/ |
| 71 | Horiz : A → A → Prop |
| 72 | /-- The upper neighbor may carry this tile. -/ |
| 73 | Vert : A → A → Prop |
| 74 | /-- The bottom row's cell in this column may carry this tile. -/ |
| 75 | First : A → A → Prop |
| 76 | /-- Being a base tile: what a column the description says nothing about |
| 77 | carries in the bottom row. -/ |
| 78 | Base : A → Prop |
| 79 | /-- Being a start tile: what the corner of the grid carries. -/ |
| 80 | Start : A → Prop |
| 81 | /-- Being a left-edge tile: what the leftmost column may carry. -/ |
| 82 | EdgeL : A → Prop |
| 83 | /-- Being a right-edge tile: what the rightmost column may carry. -/ |
| 84 | EdgeR : A → Prop |
| 85 | |
| 86 | namespace TileData |
| 87 | |
| 88 | variable {A : Type} (T : TileData A) |
| 89 | |
| 90 | /-- **The tiles the bottom row may carry in a column**: the ones the |
| 91 | description names there, and the base tiles in a column it names none. This is |
| 92 | `TMData.InitTape`'s device – a description of the row |
| 93 | rather than a listing – and it is what lets an expansion carry it. -/ |
| 94 | def FirstTile (x t : A) : Prop := |
| 95 | T.First x t ∨ ((∀ u, ¬T.First x u) ∧ T.Base t) |
| 96 | |
| 97 | /-- **A tiling of the square**: every cell carries a tile, the bottom row is one |
| 98 | the description allows, the two edge columns carry tiles allowed there, |
| 99 | horizontal and vertical neighbors are compatible, and some cell carries an |
| 100 | accepting tile. |
| 101 | |
| 102 | The two **edge conditions** are what the classical border colors of a tiling |
| 103 | problem do. A condition on neighbors says nothing about a column with no |
| 104 | neighbor on one side, so without them a tile whose meaning is “something is |
| 105 | arriving from the left” could stand in the leftmost column, justified by nothing; |
| 106 | a machine drawn as a tiling would then grow a head out of nowhere. -/ |
| 107 | def IsTiling (τ : A → A → A) : Prop := |
| 108 | (∀ x y, T.Posn x → T.Posn y → T.Tile (τ x y)) ∧ |
| 109 | (∀ x y, T.Posn x → MinPos T.Le T.Posn y → |
| 110 | ((MinPos T.Le T.Posn x → T.Start (τ x y)) ∧ |
| 111 | (¬MinPos T.Le T.Posn x → T.FirstTile x (τ x y)))) ∧ |
| 112 | (∀ x y, T.Posn y → MinPos T.Le T.Posn x → T.EdgeL (τ x y)) ∧ |
| 113 | (∀ x y, T.Posn y → MaxPos T.Le T.Posn x → T.EdgeR (τ x y)) ∧ |
| 114 | (∀ x x' y, SuccPos T.Le T.Posn x x' → T.Posn y → T.Horiz (τ x y) (τ x' y)) ∧ |
| 115 | (∀ x y y', T.Posn x → SuccPos T.Le T.Posn y y' → T.Vert (τ x y) (τ x y')) ∧ |
| 116 | ∃ x y, T.Posn x ∧ T.Posn y ∧ T.Acc (τ x y) |
| 117 | |
| 118 | /-- **The square is tileable**: some assignment of tiles to cells is a tiling. |
| 119 | The assignment is a function on the whole universe – what it does off the grid |
| 120 | is not read, so nothing is lost by not restricting it. -/ |
| 121 | def Tileable : Prop := ∃ τ : A → A → A, T.IsTiling τ |
| 122 | |
| 123 | /-- **Well-formedness**, folded into the yes-instances exactly as |
| 124 | `TMData.WellFormed` is: the order is linear, and there is |
| 125 | a position to index the grid by. -/ |
| 126 | def WellFormed : Prop := IsLinOrd T.Le ∧ ∃ p, T.Posn p |
| 127 | |
| 128 | open FirstOrder |
| 129 | |
| 130 | open Language Structure |
| 131 | |
| 132 | variable {A : Type} (T : TileData A) |
| 133 | |
| 134 | /-- **A tiling of the corridor up to a given height**: every cell of the strip |
| 135 | carries a tile, the bottom row is one the description allows, the two edge |
| 136 | columns carry tiles allowed there, neighbors in a row and rows one above the |
| 137 | other are compatible, and the top row carries an accepting tile. |
| 138 | |
| 139 | The height is where a corridor differs from |
| 140 | `TileData.IsTiling`: nothing in the instance bounds it, |
| 141 | and the tiles above the accepting row are not asked about at all. -/ |
| 142 | def IsCorridor (h : ℕ) (τ : ℕ → A → A) : Prop := |
| 143 | (∀ k x, k ≤ h → T.Posn x → T.Tile (τ k x)) ∧ |
| 144 | (∀ x, T.Posn x → |
| 145 | ((MinPos T.Le T.Posn x → T.Start (τ 0 x)) ∧ |
| 146 | (¬MinPos T.Le T.Posn x → T.FirstTile x (τ 0 x)))) ∧ |
| 147 | (∀ k x, k ≤ h → MinPos T.Le T.Posn x → T.EdgeL (τ k x)) ∧ |
| 148 | (∀ k x, k ≤ h → MaxPos T.Le T.Posn x → T.EdgeR (τ k x)) ∧ |
| 149 | (∀ k x x', k ≤ h → SuccPos T.Le T.Posn x x' → T.Horiz (τ k x) (τ k x')) ∧ |
| 150 | (∀ k x, k < h → T.Posn x → T.Vert (τ k x) (τ (k + 1) x)) ∧ |
| 151 | ∃ x, T.Posn x ∧ T.Acc (τ h x) |
| 152 | |
| 153 | /-- **The corridor can be tiled**: some assignment of tiles to its cells is a |
| 154 | tiling of it, of some height. -/ |
| 155 | def CorridorTileable : Prop := ∃ (h : ℕ) (τ : ℕ → A → A), T.IsCorridor h τ |
| 156 | |
| 157 | end TileData |
| 158 | |
| 159 | open FirstOrder |
| 160 | |
| 161 | open FirstOrder.Language |
| 162 | |
| 163 | /-- Relation symbols of wide tile-system instances: the tiles of |
| 164 | `FirstOrder.Language.tiling` with their compatibilities, and the positions and |
| 165 | their order replaced by an order on the elements – the digits of an address. -/ |
| 166 | inductive wtileRel : ℕ → Type |
| 167 | /-- `wtLe x y`: the order on the elements, along which an address is read as a |
| 168 | binary number. -/ |
| 169 | | wle : wtileRel 2 |
| 170 | /-- `wtDig x`: `x` is a digit – one of the elements the grid's coordinates are |
| 171 | subsets of. -/ |
| 172 | | dig : wtileRel 1 |
| 173 | /-- `wtTile t`: `t` is a tile. -/ |
| 174 | | tile : wtileRel 1 |
| 175 | /-- `wtAcc t`: `t` is an accepting tile. -/ |
| 176 | | tacc : wtileRel 1 |
| 177 | /-- `wtHoriz t t'`: `t'` may stand immediately to the right of `t`. -/ |
| 178 | | horiz : wtileRel 2 |
| 179 | /-- `wtVert t t'`: `t'` may stand immediately above `t`. -/ |
| 180 | | vert : wtileRel 2 |
| 181 | /-- `wtFirst x t`: the bottom row's cell of `x` may carry `t`. -/ |
| 182 | | first : wtileRel 2 |
| 183 | /-- `wtBase t`: `t` is a base tile – what the bottom row carries where the |
| 184 | description says nothing. -/ |
| 185 | | base : wtileRel 1 |
| 186 | /-- `wtStart t`: `t` is a start tile – what the corner of the grid carries. -/ |
| 187 | | tstart : wtileRel 1 |
| 188 | /-- `wtEdgeL t`: `t` may stand in the leftmost column. -/ |
| 189 | | ledge : wtileRel 1 |
| 190 | /-- `wtEdgeR t`: `t` may stand in the rightmost column. -/ |
| 191 | | redge : wtileRel 1 |
| 192 | deriving DecidableEq |
| 193 | |
| 194 | /-- The relational vocabulary of wide tile-system instances. -/ |
| 195 | def wtile : Language := |
| 196 | ⟨fun _ => Empty, wtileRel⟩ |
| 197 | |
| 198 | instance instIsRelationalWtile : wtile.IsRelational := |
| 199 | fun _ => (inferInstance : IsEmpty Empty) |
| 200 | |
| 201 | /-- The order on the elements of the instance. -/ |
| 202 | abbrev wtLe : wtile.Relations 2 := .wle |
| 203 | |
| 204 | /-- The digit symbol. -/ |
| 205 | abbrev wtDig : wtile.Relations 1 := .dig |
| 206 | |
| 207 | /-- The tile symbol. -/ |
| 208 | abbrev wtTile : wtile.Relations 1 := .tile |
| 209 | |
| 210 | /-- The accepting-tile symbol. -/ |
| 211 | abbrev wtAcc : wtile.Relations 1 := .tacc |
| 212 | |
| 213 | /-- The horizontal-compatibility symbol. -/ |
| 214 | abbrev wtHoriz : wtile.Relations 2 := .horiz |
| 215 | |
| 216 | /-- The vertical-compatibility symbol. -/ |
| 217 | abbrev wtVert : wtile.Relations 2 := .vert |
| 218 | |
| 219 | /-- The bottom-row symbol. -/ |
| 220 | abbrev wtFirst : wtile.Relations 2 := .first |
| 221 | |
| 222 | /-- The base-tile symbol. -/ |
| 223 | abbrev wtBase : wtile.Relations 1 := .base |
| 224 | |
| 225 | /-- The start-tile symbol. -/ |
| 226 | abbrev wtStart : wtile.Relations 1 := .tstart |
| 227 | |
| 228 | /-- The left-edge symbol. -/ |
| 229 | abbrev wtEdgeL : wtile.Relations 1 := .ledge |
| 230 | |
| 231 | /-- The right-edge symbol. -/ |
| 232 | abbrev wtEdgeR : wtile.Relations 1 := .redge |
| 233 | |
| 234 | open FirstOrder |
| 235 | |
| 236 | open Language Structure |
| 237 | |
| 238 | section Shorthands |
| 239 | |
| 240 | variable {A : Type} [wtile.Structure A] |
| 241 | |
| 242 | /-- The order on the elements. -/ |
| 243 | def WTLe (a b : A) : Prop := RelMap wtLe ![a, b] |
| 244 | |
| 245 | /-- Being a digit: one of the elements the grid's coordinates are subsets of. -/ |
| 246 | def WTDig (a : A) : Prop := RelMap wtDig ![a] |
| 247 | |
| 248 | /-- Being a tile. -/ |
| 249 | def WTTile (a : A) : Prop := RelMap wtTile ![a] |
| 250 | |
| 251 | /-- Being an accepting tile. -/ |
| 252 | def WTAcc (a : A) : Prop := RelMap wtAcc ![a] |
| 253 | |
| 254 | /-- Horizontal compatibility. -/ |
| 255 | def WTHoriz (a b : A) : Prop := RelMap wtHoriz ![a, b] |
| 256 | |
| 257 | /-- Vertical compatibility. -/ |
| 258 | def WTVert (a b : A) : Prop := RelMap wtVert ![a, b] |
| 259 | |
| 260 | /-- The bottom row, at the cell of an element. -/ |
| 261 | def WTFirst (a b : A) : Prop := RelMap wtFirst ![a, b] |
| 262 | |
| 263 | /-- Being a base tile. -/ |
| 264 | def WTBase (a : A) : Prop := RelMap wtBase ![a] |
| 265 | |
| 266 | /-- Being a start tile. -/ |
| 267 | def WTStart (a : A) : Prop := RelMap wtStart ![a] |
| 268 | |
| 269 | /-- Being a left-edge tile: one the leftmost column may carry. -/ |
| 270 | def WTEdgeL (a : A) : Prop := RelMap wtEdgeL ![a] |
| 271 | |
| 272 | /-- Being a right-edge tile: one the rightmost column may carry. -/ |
| 273 | def WTEdgeR (a : A) : Prop := RelMap wtEdgeR ![a] |
| 274 | |
| 275 | /-- **An element the bottom row is described at**: one whose cell carries a |
| 276 | tile. These are the elements the file has cells for. -/ |
| 277 | def WTHasFirst (a : A) : Prop := ∃ t : A, WTFirst a t |
| 278 | |
| 279 | end Shorthands |
| 280 | |
| 281 | section System |
| 282 | |
| 283 | variable {A : Type} [wtile.Structure A] |
| 284 | |
| 285 | /-- Being a position: an address is one exactly when it holds digits alone, so |
| 286 | the grid is indexed by the subsets of the *marked* part of the instance. That is |
| 287 | what leaves the instance room for its tiles: a tile is an element like any |
| 288 | other, and only the digits are coordinates. -/ |
| 289 | def wtpPosn : WPoint A → Prop |
| 290 | | Sum.inl s => ∀ x, s x → WTDig x |
| 291 | | Sum.inr _ => False |
| 292 | |
| 293 | /-- The order on the universe of the tiling: addresses first, in the |
| 294 | binary-number order they inherit from the instance's own order, then the tiles |
| 295 | in that same order. -/ |
| 296 | def wtpLe : WPoint A → WPoint A → Prop |
| 297 | | Sum.inl s, Sum.inl t => WMSetLe WTLe s t |
| 298 | | Sum.inl _, Sum.inr _ => True |
| 299 | | Sum.inr _, Sum.inl _ => False |
| 300 | | Sum.inr x, Sum.inr y => WTLe x y |
| 301 | |
| 302 | /-- The bottom row: the cell of `x` – the segment `x` cuts among the elements |
| 303 | the description names – may carry the tiles of `x`, and every other address a |
| 304 | base tile. That is the same device as the register channel's input |
| 305 | (`wpInpReg`): a file of cells, not the ruler of all the |
| 306 | segments, because a clocked machine's tape is described the same way and that is |
| 307 | where this problem's hardness comes from. -/ |
| 308 | def wtpFirst : WPoint A → WPoint A → Prop |
| 309 | | Sum.inl s, Sum.inr y => ∃ x, WMFileSeg WTLe WTHasFirst s x ∧ WTFirst x y |
| 310 | | _, _ => False |
| 311 | |
| 312 | variable (A) in |
| 313 | /-- **The wide tile system an instance describes**: the tiles read off the |
| 314 | instance, the positions being the addresses. -/ |
| 315 | def wideTileData : TileData (WPoint A) where |
| 316 | Posn := wtpPosn |
| 317 | Le := wtpLe |
| 318 | Tile := wpMark WTTile |
| 319 | Acc := wpMark WTAcc |
| 320 | Horiz := wpAttr WTHoriz |
| 321 | Vert := wpAttr WTVert |
| 322 | First := wtpFirst |
| 323 | Base := wpMark WTBase |
| 324 | Start := wpMark WTStart |
| 325 | EdgeL := wpMark WTEdgeL |
| 326 | EdgeR := wpMark WTEdgeR |
| 327 | |
| 328 | end System |
| 329 | |
| 330 | open Lax904597.Problems Lax485149.Problems |
| 331 | |
| 332 | /-- **Square tiling one exponential up.** -/ |
| 333 | def WideTiling : DecisionProblem wtile := |
| 334 | DecisionProblem.ofPred fun A _ => (wideTileData A).WellFormed ∧ (wideTileData A).Tileable |
| 335 | |
| 336 | /-- **Corridor tiling one exponential up.** -/ |
| 337 | def WideCorridor : DecisionProblem wtile := |
| 338 | DecisionProblem.ofPred fun A _ => (wideTileData A).WellFormed ∧ (wideTileData A).CorridorTileable |
| 339 | |
| 340 | end Lax822549.WideTilings |
| 341 |
From Mathlib
Mathlib.Algebra.BigOperators.FinprodMathlib.Data.Finite.SigmaMathlib.Data.Fintype.EquivFinMathlib.Data.Fintype.LatticeMathlib.Data.Fintype.PigeonholeMathlib.Data.Prod.LexMathlib.Data.Set.CardMathlib.Data.Set.Finite.LemmasMathlib.Dynamics.FixedPoints.BasicMathlib.Logic.Equiv.Fin.BasicMathlib.Logic.Equiv.ProdMathlib.ModelTheory.ComplexityMathlib.ModelTheory.OrderMathlib.ModelTheory.SemanticsMathlib.Order.Lattice.NatMathlib.Order.PiLexMathlib.SetTheory.Cardinal.FiniteMathlib.Tactic.FinCases
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments