From 0dc43fc64eb5e470927e0ac1c514af7abcd19b3b Mon Sep 17 00:00:00 2001 From: zbrachinara Date: Wed, 27 Nov 2024 16:44:43 -0500 Subject: [PATCH] begin defining solution ndpa for two-column --- NpTetris/Proofs/S3_2_TwoColumn/NDPA.lean | 1 + .../Proofs/S3_2_TwoColumn/SolutionNDPA.lean | 80 +++++++++++++++++++ 2 files changed, 81 insertions(+) create mode 100644 NpTetris/Proofs/S3_2_TwoColumn/SolutionNDPA.lean diff --git a/NpTetris/Proofs/S3_2_TwoColumn/NDPA.lean b/NpTetris/Proofs/S3_2_TwoColumn/NDPA.lean index dcbf1b7..818826c 100644 --- a/NpTetris/Proofs/S3_2_TwoColumn/NDPA.lean +++ b/NpTetris/Proofs/S3_2_TwoColumn/NDPA.lean @@ -7,6 +7,7 @@ structure NDPA (Stack_α String_α State: Type) where initial : Set State initial_stack : Stack_α accept : Set State +finite: Fintype State step : State → Stack_α → Option String_α → Set (State × List Stack_α) namespace NDPA diff --git a/NpTetris/Proofs/S3_2_TwoColumn/SolutionNDPA.lean b/NpTetris/Proofs/S3_2_TwoColumn/SolutionNDPA.lean new file mode 100644 index 0000000..d4b6431 --- /dev/null +++ b/NpTetris/Proofs/S3_2_TwoColumn/SolutionNDPA.lean @@ -0,0 +1,80 @@ +import NpTetris.Proofs.S3_2_TwoColumn.NDPA +import NpTetris.Mino.LekMino + +namespace Solution + +/-- +This type acts as the stack language of the equivalent NDPA to a two-column $≤k$-tris game. They are +one-to-one with the state of a $k$-tris "stack", the shape that the filled cells on a board form. To +see this, let `Left` represent rows where the left column is filled, `Right` represent the same for +the right column. + +For any $k$-tris stack, there must be a contiguous range of rows starting from the bottom and going +up to a maximum height where all the rows are either filled on the left and right column, and all +other rows are empty. If, for example, there was an empty row separating two such contiguous ranges, +this would imply that there is a placement which was anchored on nothing. But this is impossible by +the definition of $≤k$-tris, so such a situation cannot happen. A full row is irrelevant because it +can be eliminated with a line clear. +-/ +inductive FilledColumn where +| Left +| Right + +inductive State (rows k : ℕ+) where +/-- +The explicit failure state, which the machine enteers when it cannot spawn the next piece in the +queue +-/ +| terminal +/-- +In this state, the machine is in the process of resolving the state of the board after locking a +piece. Here are the parts of this state: +- The number of rows currently filled. Once this grows so large that the next piece cannot be + spawned, the machine transitions to the failure state (`none`). +- The row-wise residue of the piece, from the bottom (the side closer to the bottom of the board) to + the top. While a piece's residue needs not be connected, rows which are full must still be + represented, because they will act like a "rim" which stops the piece from clearing any more + lines. As an example, think about an s/z piece in 2-column 4-tris. + + This residue is used to decide whether a row can be cleared. If the next residue is the opposite + of the next stack symbol (that is, if the left and right column interlock to fill a row), then the + residue is popped and the process repeats again. If the next residue is not the opposite of the + next stack symbol, then the residue is pushed onto the stack. Note that rows of residue which are + entirely filled are `none`. +- There are at most `k` rows of residue to consider, corresponding to the smallest bounding box + containing all spawnable $≤k$-minos. This puts a finite bound on the number of states, which is + required to show that an algorithm for acceptability is polynomial. +-/ +| resolving (filled : Fin rows) (residue : List (Option FilledColumn)) (rlen: residue.length ≤ k) +/-- +In this state, the board is ready to receive the next piece in the queue. The number of rows is +recorded so that the machine knows whether to transition to the terminal state. +-/ +| ready (filled : Fin rows) + +-- inductive State (k rows : ℕ+) where +-- /-- The explicit failure state, which is entered when a piece cannot be spawned -/ +-- | terminal +-- | stepping (height : Fin rows) + +/-- Explanation of the types given to the NDPA: + +- **Stack**: See [WellRow] +- **String**: The strings that the NDPA accepts are exactly piece queues, no suprises there. +- **State**: The row at which the cutoff happens between partially filled and completely unfilled + rows. Note that this number does not have to reach `rows - 1` to end in a failure state -- it only + has to prevent the next piece in the queue from spawning (that is, there is no position at which + the piece could be positioned so that it touches the top of the board while not intersecting + filled cells). +-/ +def machine (rows k: ℕ+) : NDPA (Option FilledColumn) (LeKShape k) (State rows k) where +-- start with an empty board +initial := {State.ready 0} +initial_stack := none +-- Once the queue is exhausted it doesn't matter whether or not a piece can be spawned +accept x := ∃ k, x = State.ready k +finite := by + constructor + case elems => sorry + case complete => sorry +step state := sorry