Documentation

MIPRE.TM.CookLevin.Tableau

The Cook–Levin tableau of a multi-input machine #

The 3SAT formula tableau M s₀ s₁ S fixed chk of a run of S steps of the machine M (planning/succinct-cook-levin.md, S1; answer_reduction.tex prop:standard-succinct-sat):

The check circuit is a parameter with its specification IsCheckCircuit: chk.evalBits (winBits win) = true ↔ checkPred M acc win; the correctness of the tableau (Correct.lean) is proved against the specification, and S3 supplies the circuit.

Positions #

source
def MIPRE.TM.CookLevin.numCells (S : ℕ) :
ℕ

The number of cells of a tape of the tableau of S steps.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPRE.TM.CookLevin.Pos (S : ℕ) :
    Type

    A cell position.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev MIPRE.TM.CookLevin.Center (S : ℕ) :
      Type

      A window center, offset by two: the window of center c covers the cells c .. c + 4, its middle cell being c + 2.

      Equations
      Instances For
        source
        def MIPRE.TM.CookLevin.cellIdx {S : ℕ} (c : Center S) (δ : Fin 5) :
        Pos S

        The cell at offset δ of the window of center c.

        Equations
        Instances For
          source
          def MIPRE.TM.CookLevin.center {S : ℕ} (c : Center S) :
          Pos S

          The middle cell of a window.

          Equations
          Instances For
            source
            def MIPRE.TM.CookLevin.Pos.IsBdry {S : ℕ} (p : Pos S) :
            Prop

            A boundary cell: the first two and the last two.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance MIPRE.TM.CookLevin.instDecidableIsBdry {S : ℕ} (p : Pos S) :
              Decidable p.IsBdry
              Equations
              source
              def MIPRE.TM.CookLevin.startCell {i w : ℕ} (S : ℕ) :
              Tape i w → Pos S

              The cell of a head at time 0: an input head starts on the first symbol, position value 1, cell 3; a work head at position 0, cell S + 3.

              Equations
              Instances For
                source
                def MIPRE.TM.CookLevin.inputCellVal {Symbol : Type u_1} {S : ℕ} (x : List Symbol) (p : Pos S) :
                CellVal Symbol

                The value of cell p of an input tape holding x: the boundary marker on boundary cells, the symbols of x on cells 3 .. |x| + 2, blanks elsewhere.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def MIPRE.TM.CookLevin.workCellVal₀ {Symbol : Type u_1} {S : ℕ} (p : Pos S) :
                  CellVal Symbol

                  The value of cell p of a work tape at time 0.

                  Equations
                  Instances For

                    Variables #

                    source
                    inductive MIPRE.TM.CookLevin.TabVar (i w : ℕ) (Symbol : Type u_1) (State : Type u_2) (S G : ℕ) :
                    Type (max u_1 u_2)

                    The variables of the tableau.

                    Instances For
                      source
                      @[instance_reducible]
                      instance MIPRE.TM.CookLevin.instDecidableEqTabVar {i✝ w✝ : ℕ} {Symbol✝ : Type u_1} {State✝ : Type u_2} {S✝ G✝ : ℕ} [DecidableEq Symbol✝] [DecidableEq State✝] :
                      DecidableEq (TabVar i✝ w✝ Symbol✝ State✝ S✝ G✝)
                      Equations
                      source
                      def MIPRE.TM.CookLevin.instDecidableEqTabVar.decEq {i✝ w✝ : ℕ} {Symbol✝ : Type u_1} {State✝ : Type u_2} {S✝ G✝ : ℕ} [DecidableEq Symbol✝] [DecidableEq State✝] (x✝ x✝¹ : TabVar i✝ w✝ Symbol✝ State✝ S✝ G✝) :
                      Decidable (x✝ = x✝¹)
                      Equations
                      Instances For
                        source
                        def MIPRE.TM.CookLevin.winVarOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (t : Fin S) (js : Tape i w → Center S) :
                        WinVar i w Symbol State → TabVar i w Symbol State S G

                        The tableau variable of a window variable, at step t and centers js.

                        Equations
                        Instances For
                          source
                          @[reducible, inline]
                          abbrev MIPRE.TM.CookLevin.winCard (i w : ℕ) (Symbol : Type u_3) (State : Type u_4) [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] :
                          ℕ

                          The number of window variables: the number of inputs of a check circuit.

                          Equations
                          Instances For
                            source
                            noncomputable def MIPRE.TM.CookLevin.winBits {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] (win : WinVar i w Symbol State → Bool) :
                            List Bool

                            The bits of a window, in the canonical order.

                            Equations
                            Instances For
                              source
                              def MIPRE.TM.CookLevin.IsCheckCircuit {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) (chk : SAT.Circuit) :
                              Prop

                              chk computes local consistency of a window: its specification, the hypothesis of the correctness of the tableau (Correct.lean); S3 supplies the circuit.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                noncomputable def MIPRE.TM.CookLevin.inpOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S G : ℕ} (t : Fin S) (js : Tape i w → Center S) (n : ℕ) :
                                TabVar i w Symbol State S G

                                The input variables of the check circuit at a window: the n-th window variable.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  def MIPRE.TM.CookLevin.auxOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (t : Fin S) (js : Tape i w → Center S) (g : ℕ) :
                                  TabVar i w Symbol State S G

                                  The gate variables of the check circuit at a window.

                                  Equations
                                  Instances For
                                    source
                                    def MIPRE.TM.CookLevin.unit {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (v : TabVar i w Symbol State S G) (b : Bool) :
                                    SAT.Clause3 (TabVar i w Symbol State S G)

                                    A unit clause.

                                    Equations
                                    Instances For
                                      source
                                      def MIPRE.TM.CookLevin.imp2 {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a b : TabVar i w Symbol State S G) :
                                      SAT.Clause3 (TabVar i w Symbol State S G)

                                      The clause ¬a ∨ b.

                                      Equations
                                      Instances For
                                        source
                                        def MIPRE.TM.CookLevin.nand2 {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a b : TabVar i w Symbol State S G) :
                                        SAT.Clause3 (TabVar i w Symbol State S G)

                                        The clause ¬a ∨ ¬b.

                                        Equations
                                        Instances For
                                          source
                                          def MIPRE.TM.CookLevin.startClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] (S G : ℕ) (M : Turing.MultiInputTM i w Symbol State) (fixed : Fin i → Option (List Symbol)) :
                                          SAT.Cnf3 (TabVar i w Symbol State S G)

                                          The start rows: heads on their first cells, the start state, the fixed input tapes holding their strings, the work tapes blank.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            def MIPRE.TM.CookLevin.freeClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (S G : ℕ) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) :
                                            SAT.Cnf3 (TabVar i w Symbol State S G)

                                            The free input tapes at time 0: boundary cells, the cell before the input blank, the other cells one of s₀, s₁, blank, exactly one of them, with blanks trailing.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              source
                                              def MIPRE.TM.CookLevin.bdryClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (S G : ℕ) :
                                              SAT.Cnf3 (TabVar i w Symbol State S G)

                                              The boundary rows: boundary cells hold the marker and carry no head, at every time.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                def MIPRE.TM.CookLevin.emitClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (S G : ℕ) :
                                                SAT.Cnf3 (TabVar i w Symbol State S G)

                                                The emission bookkeeping: nothing emitted before time 0, emitted (t + 1) ↔ emitted t ∨ emitOne t, no emission after an emission, nothing but acc ever emitted.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  def MIPRE.TM.CookLevin.finalClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (S G : ℕ) :
                                                  SAT.Cnf3 (TabVar i w Symbol State S G)

                                                  The acceptance row: halted at time S, and acc emitted.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    source
                                                    noncomputable def MIPRE.TM.CookLevin.windowClauses {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] (S : ℕ) (chk : SAT.Circuit) :
                                                    SAT.Cnf3 (TabVar i w Symbol State S chk.gates.length)

                                                    The window clauses: the circuit-to-3SAT formula of the check circuit at every step and window.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      source
                                                      noncomputable def MIPRE.TM.CookLevin.tableau {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (S : ℕ) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) :
                                                      SAT.Cnf3 (TabVar i w Symbol State S chk.gates.length)

                                                      The tableau formula.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        The assignment of a run #

                                                        source
                                                        def MIPRE.TM.CookLevin.cellValAt {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (d : Tape i w) (p : Pos S) :
                                                        CellVal Symbol

                                                        The value of cell p of tape d in a configuration.

                                                        Equations
                                                        Instances For
                                                          source
                                                          def MIPRE.TM.CookLevin.headCell {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) :
                                                          Tape i w → ℤ

                                                          The cell of the head of tape d, as an integer.

                                                          Equations
                                                          Instances For
                                                            source
                                                            def MIPRE.TM.CookLevin.cfgAt {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} (M : Turing.MultiInputTM i w Symbol State) {input : Fin i → List Symbol} (t : ℕ) :
                                                            Turing.MultiInputTM.Cfg i w Symbol State input

                                                            The configuration at time t of the run on input.

                                                            Equations
                                                            Instances For
                                                              source
                                                              def MIPRE.TM.CookLevin.baseAssign {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (G : ℕ) :
                                                              TabVar i w Symbol State S G → Bool

                                                              The assignment of the run on the non-auxiliary variables.

                                                              Equations
                                                              Instances For
                                                                source
                                                                noncomputable def MIPRE.TM.CookLevin.runAssign {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (chk : SAT.Circuit) :
                                                                TabVar i w Symbol State S chk.gates.length → Bool

                                                                The assignment of the run: the encodings of its configurations, and on the auxiliary variables the gate values of the check circuit at every window.

                                                                Equations
                                                                Instances For