Documentation

MIPRE.Foundations.SAT.Formula

Boolean formulas and their circuits #

A formula (Fml) is a tree of and, or, not over input bits and constants. Its post-order flattening (Fml.flattenAt) is a circuit in which every gate is read at most once (input bits are read through fresh input gates, which Circuit.WellFormed does not count), so a formula's circuit is well-formed whatever the formula (Fml.toCircuit_wellFormed), and computes the formula (Fml.eval_toCircuit). The describer of the succinct Cook–Levin theorem is built as a formula, which confines the circuit bookkeeping to this file (planning/succinct-cook-levin.md, S3).

source
inductive MIPRE.SAT.Fml :
Type

Boolean formulas over input bits.

Instances For
    source
    @[instance_reducible]
    instance MIPRE.SAT.instDecidableEqFml :
    DecidableEq Fml
    Equations
    source
    def MIPRE.SAT.instDecidableEqFml.decEq (x✝ x✝¹ : Fml) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance MIPRE.SAT.instReprFml :
      Repr Fml
      Equations
      source
      def MIPRE.SAT.instReprFml.repr :
      Fml → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance MIPRE.SAT.instInhabitedFml :
        Inhabited Fml
        Equations
        source
        def MIPRE.SAT.Fml.eval (x : ℕ → Bool) :
        Fml → Bool

        The value of a formula on the input bits x.

        Equations
        Instances For
          source
          def MIPRE.SAT.Fml.size :
          Fml → ℕ

          The number of nodes: the number of gates of the circuit.

          Equations
          Instances For
            source
            theorem MIPRE.SAT.Fml.size_pos (f : Fml) :
            0 < f.size
            source
            def MIPRE.SAT.Fml.InputsLt (n : ℕ) :
            Fml → Prop

            Every input bit read is below n.

            Equations
            Instances For
              source
              theorem MIPRE.SAT.Fml.InputsLt.mono {n m : ℕ} (h : n ≤ m) {f : Fml} (hf : InputsLt n f) :
              InputsLt m f

              Formulas as data: the post-order serialization #

              source
              inductive MIPRE.SAT.Fml.Node :
              Type

              The nodes of the post-order (reverse Polish) serialization of a formula.

              Instances For
                source
                def MIPRE.SAT.Fml.instDecidableEqNode.decEq (x✝ x✝¹ : Node) :
                Decidable (x✝ = x✝¹)
                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance MIPRE.SAT.Fml.instDecidableEqNode :
                  DecidableEq Node
                  Equations
                  source
                  def MIPRE.SAT.Fml.instReprNode.repr :
                  Node → ℕ → Std.Format
                  Equations
                  Instances For
                    source
                    @[instance_reducible]
                    instance MIPRE.SAT.Fml.instReprNode :
                    Repr Node
                    Equations
                    source
                    @[instance_reducible]
                    instance MIPRE.SAT.Fml.instInhabitedNode :
                    Inhabited Node
                    Equations
                    source
                    def MIPRE.SAT.Fml.Node.toData :
                    Node → Cost.Data

                    Nodes as data: a unary tag and the payload.

                    Equations
                    Instances For
                      source
                      def MIPRE.SAT.Fml.Node.ofData? :
                      Cost.Data → Option Node

                      Decoding nodes.

                      Equations
                      Instances For
                        source
                        theorem MIPRE.SAT.Fml.Node.ofData?_toData (nd : Node) :
                        ofData? nd.toData = some nd
                        source
                        @[instance_reducible]
                        instance MIPRE.SAT.Fml.Node.instSizedEncoding :
                        Cost.SizedEncoding Node
                        Equations
                        source
                        theorem MIPRE.SAT.Fml.Node.encode_inp (i : ℕ) :
                        Cost.encode (inp i) = (Cost.Data.ofNat 0).cons (Cost.encode i)
                        source
                        theorem MIPRE.SAT.Fml.Node.encode_const (b : Bool) :
                        Cost.encode (const b) = (Cost.Data.ofNat 1).cons (Cost.encode b)
                        source
                        theorem MIPRE.SAT.Fml.Node.encode_and :
                        Cost.encode and = (Cost.Data.ofNat 2).cons Cost.Data.nil
                        source
                        theorem MIPRE.SAT.Fml.Node.encode_or :
                        Cost.encode or = (Cost.Data.ofNat 3).cons Cost.Data.nil
                        source
                        theorem MIPRE.SAT.Fml.Node.encode_not :
                        Cost.encode not = (Cost.Data.ofNat 4).cons Cost.Data.nil
                        source
                        def MIPRE.SAT.Fml.rpn :
                        Fml → List Node

                        The post-order serialization of a formula.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem MIPRE.SAT.Fml.length_rpn (f : Fml) :
                          f.rpn.length = f.size
                          source
                          def MIPRE.SAT.Fml.parseStep (st : List Fml) :
                          Node → List Fml

                          One step of parsing a post-order serialization with a stack of formulas (a malformed input leaves the stack unchanged).

                          Equations
                          Instances For
                            source
                            theorem MIPRE.SAT.Fml.foldl_parseStep_rpn (f : Fml) (rest : List Node) (st : List Fml) :
                            List.foldl parseStep st (f.rpn ++ rest) = List.foldl parseStep (f :: st) rest
                            source
                            def MIPRE.SAT.Fml.parse (l : List Node) :
                            Option Fml

                            Parsing a post-order serialization.

                            Equations
                            Instances For
                              source
                              theorem MIPRE.SAT.Fml.parse_rpn (f : Fml) :
                              parse f.rpn = some f
                              source
                              @[instance_reducible]
                              instance MIPRE.SAT.Fml.instSizedEncoding :
                              Cost.SizedEncoding Fml

                              Formulas encode as their post-order serializations, so that a program builds a formula by appending lists.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              source
                              theorem MIPRE.SAT.Fml.encode_fml (f : Fml) :
                              Cost.encode f = Cost.encode f.rpn
                              source
                              noncomputable def MIPRE.SAT.Fml.rpnF :
                              Cost.PolyTimeFun Fml (List Node)

                              The serialization, as a polynomial-time function (the encoding is the same).

                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem MIPRE.SAT.Fml.rpnF_apply (f : Fml) :
                                rpnF.toFun f = f.rpn
                                source
                                noncomputable def MIPRE.SAT.Fml.inpF :
                                Cost.PolyTimeFun ℕ Fml

                                The constructors as polynomial-time functions.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  source
                                  noncomputable def MIPRE.SAT.Fml.constF :
                                  Cost.PolyTimeFun Bool Fml
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    noncomputable def MIPRE.SAT.Fml.andF :
                                    Cost.PolyTimeFun (Fml × Fml) Fml
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      noncomputable def MIPRE.SAT.Fml.orF :
                                      Cost.PolyTimeFun (Fml × Fml) Fml
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        source
                                        noncomputable def MIPRE.SAT.Fml.notF :
                                        Cost.PolyTimeFun Fml Fml
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          @[simp]
                                          theorem MIPRE.SAT.Fml.inpF_apply (i : ℕ) :
                                          inpF.toFun i = inp i
                                          source
                                          @[simp]
                                          theorem MIPRE.SAT.Fml.constF_apply (b : Bool) :
                                          constF.toFun b = const b
                                          source
                                          @[simp]
                                          theorem MIPRE.SAT.Fml.andF_apply (p : Fml × Fml) :
                                          andF.toFun p = p.1.and p.2
                                          source
                                          @[simp]
                                          theorem MIPRE.SAT.Fml.orF_apply (p : Fml × Fml) :
                                          orF.toFun p = p.1.or p.2
                                          source
                                          @[simp]
                                          theorem MIPRE.SAT.Fml.notF_apply (f : Fml) :
                                          notF.toFun f = f.not

                                          Flattening to a circuit #

                                          source
                                          def MIPRE.SAT.Fml.flattenAt (base : ℕ) :
                                          Fml → List Gate

                                          The post-order gate list of a formula whose first gate is at position base: the output gate is the last one, at base + size - 1.

                                          Equations
                                          Instances For
                                            source
                                            @[simp]
                                            theorem MIPRE.SAT.Fml.length_flattenAt (base : ℕ) (f : Fml) :
                                            (flattenAt base f).length = f.size
                                            source
                                            def MIPRE.SAT.Fml.toCircuit (n : ℕ) (f : Fml) :
                                            Circuit

                                            The circuit of a formula on n inputs.

                                            Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem MIPRE.SAT.Fml.toCircuit_inputs (n : ℕ) (f : Fml) :
                                              (toCircuit n f).inputs = n
                                              source
                                              @[simp]
                                              theorem MIPRE.SAT.Fml.toCircuit_size (n : ℕ) (f : Fml) :
                                              (toCircuit n f).size = f.size
                                              source
                                              theorem MIPRE.SAT.Fml.refs_flattenAt (base : ℕ) (f : Fml) (k : ℕ) (hk : k < (flattenAt base f).length) (u : ℕ) :
                                              u ∈ (flattenAt base f)[k].refs → base ≤ u ∧ u < base + k

                                              Every reference of the gate at position k of flattenAt base f lies in [base, base + k).

                                              source
                                              def MIPRE.SAT.Fml.refCount (gs : List Gate) (u : ℕ) :
                                              ℕ

                                              The number of references to u in a gate list.

                                              Equations
                                              Instances For
                                                source
                                                @[simp]
                                                theorem MIPRE.SAT.Fml.refCount_nil (u : ℕ) :
                                                refCount [] u = 0
                                                source
                                                @[simp]
                                                theorem MIPRE.SAT.Fml.refCount_append (gs hs : List Gate) (u : ℕ) :
                                                refCount (gs ++ hs) u = refCount gs u + refCount hs u
                                                source
                                                @[simp]
                                                theorem MIPRE.SAT.Fml.refCount_singleton (g : Gate) (u : ℕ) :
                                                refCount [g] u = List.count u g.refs
                                                source
                                                theorem MIPRE.SAT.Fml.refCount_eq_zero_of_forall (gs : List Gate) (u : ℕ) (h : ∀ (k : ℕ) (hk : k < gs.length), u ∉ gs[k].refs) :
                                                refCount gs u = 0

                                                A gate list whose references at position k are in [base, base + k) references no u outside [base, base + length - 1).

                                                source
                                                theorem MIPRE.SAT.Fml.refCount_flattenAt_eq_zero (base : ℕ) (f : Fml) (u : ℕ) (hu : u < base ∨ base + f.size - 1 ≤ u) :
                                                refCount (flattenAt base f) u = 0
                                                source
                                                theorem MIPRE.SAT.Fml.refCount_flattenAt_le (base : ℕ) (f : Fml) (u : ℕ) :
                                                refCount (flattenAt base f) u ≤ 1

                                                Every gate of the circuit of a formula is read at most once, and the output gate is read by no gate.

                                                source
                                                theorem MIPRE.SAT.Fml.inputsLt_of_mem_flattenAt {n : ℕ} (base : ℕ) (f : Fml) :
                                                InputsLt n f → ∀ (i : ℕ), Gate.input i ∈ flattenAt base f → i < n
                                                source
                                                theorem MIPRE.SAT.Fml.toCircuit_wellFormed {n : ℕ} (f : Fml) (hf : InputsLt n f) :
                                                (toCircuit n f).WellFormed

                                                The circuit of a formula is well-formed.

                                                Evaluation #

                                                source
                                                theorem MIPRE.SAT.Fml.Circuit.valueAt_append (n : ℕ) (gs post : List Gate) (x : ℕ → Bool) (k : ℕ) (hk : k < gs.length) :
                                                { inputs := n, gates := gs ++ post }.valueAt x k = { inputs := n, gates := gs }.valueAt x k

                                                The value of a gate depends only on the gates up to it: appending gates changes nothing.

                                                source
                                                theorem MIPRE.SAT.Fml.Circuit.getD_ofFn_valueAt (C : Circuit) (x : ℕ → Bool) (k u : ℕ) (hu : u < k) :
                                                (List.ofFn fun (i : Fin k) => C.valueAt x ↑i).getD u false = C.valueAt x u

                                                The values of the earlier gates, as read by a gate.

                                                source
                                                theorem MIPRE.SAT.Fml.valueAt_flattenAt (n : ℕ) (x : ℕ → Bool) (f : Fml) (pre post : List Gate) :
                                                { inputs := n, gates := pre ++ flattenAt pre.length f ++ post }.valueAt x (pre.length + f.size - 1) = eval x f

                                                The output gate of flattenAt placed after pre computes the formula, whatever follows.

                                                source
                                                theorem MIPRE.SAT.Fml.eval_toCircuit (n : ℕ) (f : Fml) (x : ℕ → Bool) :
                                                (toCircuit n f).eval x = eval x f

                                                The circuit of a formula computes it.

                                                source
                                                theorem MIPRE.SAT.Fml.evalBits_toCircuit (n : ℕ) (f : Fml) (l : List Bool) :
                                                (toCircuit n f).evalBits l = eval (fun (i : ℕ) => l.getD i false) f