Documentation

Complexity.Computability.Circuit.Boolean.Formula.Restriction

Restrictions of De Morgan formulas #

Restricting a De Morgan formula by a partial assignment ρ (Formula.restrict) replaces the leaves of the fixed inputs by constants and simplifies bottom up: constants are propagated through the gates, and double negations cancel. The result computes the restricted function F.eval ∘ ρ.fill (Formula.eval_restrict) and keeps only the leaves of the free inputs (Formula.leafSize_restrict_le). It is a constant or a simplified formula (Formula.IsSimplified): one without constants or double negations, which has at most 3 L - 2 operation nodes for L leaves (Formula.IsSimplified.size_add_two_le). In particular a formula whose restriction has no leaves restricts to a constant (Formula.exists_restrict_eq_const).

The formula size Boolean.formulaSize f of a Boolean function is the least leaf size of a De Morgan formula computing it, Jukna's L(f) Jukna, Chapter 6. Restrictions do not increase it (Boolean.formulaSize_comp_fill_le), and a function depending only on a set S of inputs has a formula of least leaf size whose leaves all read inputs in S (Boolean.leafSizeIn_eq_leafSize_of_dependsOn). Every function has a formula of least leaf size with at most 3 L(f) - 2 operation nodes, or a constant (Boolean.exists_computes_size_le).

Main definitions #

Main results #

References #

Simplifying gates #

source
def Cslib.Circuits.Formula.constValue? {n : ℕ} :
Formula Boolean.signature n → Option Bool

The value of a constant formula, and none for every other formula.

Instances For
    source
    @[simp]
    theorem Cslib.Circuits.Formula.constValue?_const {n : ℕ} (b : Bool) :
    (const b).constValue? = some b

    constValue? of a constant formula const b is some b.

    source
    theorem Cslib.Circuits.Formula.eq_const_of_constValue? {n : ℕ} {F : Formula Boolean.signature n} {b : Bool} (h : F.constValue? = some b) :
    F = const b

    A formula with a constant value is that constant.

    source
    theorem Cslib.Circuits.Formula.eq_const_or_constValue?_eq_none {n : ℕ} (F : Formula Boolean.signature n) :
    (∃ (b : Bool), F = const b) ∨ F.constValue? = none

    A formula is either a constant or has constValue? = none.

    source
    def Cslib.Circuits.Formula.mkNot {n : ℕ} :
    Formula Boolean.signature n → Formula Boolean.signature n

    Negation, cancelling a double negation and evaluating a negated constant.

    Instances For
      source
      def Cslib.Circuits.Formula.mkAnd {n : ℕ} (F G : Formula Boolean.signature n) :
      Formula Boolean.signature n

      Conjunction, simplifying constant arguments.

      Instances For
        source
        def Cslib.Circuits.Formula.mkOr {n : ℕ} (F G : Formula Boolean.signature n) :
        Formula Boolean.signature n

        Disjunction, simplifying constant arguments.

        Instances For
          source
          theorem Cslib.Circuits.Formula.gate_not_eq {n : ℕ} (args : Fin (Boolean.signature.Arity Boolean.Op.not) → Formula Boolean.signature n) :
          gate Boolean.Op.not args = (args 0).not

          A unary node is the negation of its argument.

          source
          theorem Cslib.Circuits.Formula.gate_and_eq {n : ℕ} (args : Fin (Boolean.signature.Arity Boolean.Op.and) → Formula Boolean.signature n) :
          gate Boolean.Op.and args = (args 0).and (args 1)

          A binary .and node is the conjunction of its arguments.

          source
          theorem Cslib.Circuits.Formula.gate_or_eq {n : ℕ} (args : Fin (Boolean.signature.Arity Boolean.Op.or) → Formula Boolean.signature n) :
          gate Boolean.Op.or args = (args 0).or (args 1)

          A binary .or node is the disjunction of its arguments.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkNot_const {n : ℕ} (b : Bool) :
          (const b).mkNot = const !b

          mkNot of a constant const b is const (!b).

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkNot_not {n : ℕ} (F : Formula Boolean.signature n) :
          F.not.mkNot = F

          mkNot cancels a double negation.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkNot_input {n : ℕ} (i : Fin n) :
          (input i).mkNot = (input i).not

          mkNot of an input leaf is its negation.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkNot_and {n : ℕ} (F G : Formula Boolean.signature n) :
          (F.and G).mkNot = (F.and G).not

          mkNot of a conjunction is its negation.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkNot_or {n : ℕ} (F G : Formula Boolean.signature n) :
          (F.or G).mkNot = (F.or G).not

          mkNot of a disjunction is its negation.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.eval_mkNot {n : ℕ} (x : BitString n) (F : Formula Boolean.signature n) :
          F.mkNot.eval Boolean.interpretation x = !F.eval Boolean.interpretation x

          mkNot F evaluates to the negation of F.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.leafSize_mkNot {n : ℕ} (F : Formula Boolean.signature n) :
          F.mkNot.leafSize = F.leafSize

          mkNot preserves leaf size.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.eval_mkAnd {n : ℕ} (x : BitString n) (F G : Formula Boolean.signature n) :
          (F.mkAnd G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x && G.eval Boolean.interpretation x)

          mkAnd F G evaluates to the conjunction of F and G.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.eval_mkOr {n : ℕ} (x : BitString n) (F G : Formula Boolean.signature n) :
          (F.mkOr G).eval Boolean.interpretation x = (F.eval Boolean.interpretation x || G.eval Boolean.interpretation x)

          mkOr F G evaluates to the disjunction of F and G.

          source
          theorem Cslib.Circuits.Formula.leafSize_mkAnd_le {n : ℕ} (F G : Formula Boolean.signature n) :
          (F.mkAnd G).leafSize ≤ F.leafSize + G.leafSize

          The leaf size of mkAnd F G is at most F.leafSize + G.leafSize.

          source
          theorem Cslib.Circuits.Formula.leafSize_mkOr_le {n : ℕ} (F G : Formula Boolean.signature n) :
          (F.mkOr G).leafSize ≤ F.leafSize + G.leafSize

          The leaf size of mkOr F G is at most F.leafSize + G.leafSize.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkAnd_const_false_left {n : ℕ} (G : Formula Boolean.signature n) :
          (const false).mkAnd G = const false

          mkAnd with const false on the left simplifies to const false.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkAnd_const_true_left {n : ℕ} (G : Formula Boolean.signature n) :
          (const true).mkAnd G = G

          mkAnd with const true on the left simplifies to the right argument.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkAnd_const_false_right {n : ℕ} (F : Formula Boolean.signature n) :
          F.mkAnd (const false) = const false

          mkAnd with const false on the right simplifies to const false.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkAnd_const_true_right {n : ℕ} (F : Formula Boolean.signature n) :
          F.mkAnd (const true) = F

          mkAnd with const true on the right simplifies to the left argument.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkOr_const_true_left {n : ℕ} (G : Formula Boolean.signature n) :
          (const true).mkOr G = const true

          mkOr with const true on the left simplifies to const true.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkOr_const_false_left {n : ℕ} (G : Formula Boolean.signature n) :
          (const false).mkOr G = G

          mkOr with const false on the left simplifies to the right argument.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkOr_const_true_right {n : ℕ} (F : Formula Boolean.signature n) :
          F.mkOr (const true) = const true

          mkOr with const true on the right simplifies to const true.

          source
          @[simp]
          theorem Cslib.Circuits.Formula.mkOr_const_false_right {n : ℕ} (F : Formula Boolean.signature n) :
          F.mkOr (const false) = F

          mkOr with const false on the right simplifies to the left argument.

          Restriction #

          source
          def Cslib.Circuits.Formula.restrict {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) :
          Formula Boolean.signature n → Formula Boolean.signature n

          The restriction of a formula by a partial assignment ρ: the leaves of the inputs fixed by ρ become constants, and constants and double negations are simplified bottom up.

          Instances For
            source
            @[simp]
            theorem Cslib.Circuits.Formula.restrict_input {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (i : Fin n) :
            restrict ρ (input i) = (ρ i).elim (input i) const

            Restricting an input leaf input i by ρ yields const b if ρ i = some b and input i otherwise.

            source
            @[simp]
            theorem Cslib.Circuits.Formula.restrict_const {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (b : Bool) :
            restrict ρ (const b) = const b

            Restricting a constant formula const b leaves it unchanged.

            source
            @[simp]
            theorem Cslib.Circuits.Formula.restrict_not {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (F : Formula Boolean.signature n) :
            restrict ρ F.not = (restrict ρ F).mkNot

            Restricting a negation applies mkNot to the restricted argument.

            source
            @[simp]
            theorem Cslib.Circuits.Formula.restrict_and {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (F G : Formula Boolean.signature n) :
            restrict ρ (F.and G) = (restrict ρ F).mkAnd (restrict ρ G)

            Restricting a conjunction applies mkAnd to the restricted arguments.

            source
            @[simp]
            theorem Cslib.Circuits.Formula.restrict_or {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (F G : Formula Boolean.signature n) :
            restrict ρ (F.or G) = (restrict ρ F).mkOr (restrict ρ G)

            Restricting a disjunction applies mkOr to the restricted arguments.

            source
            theorem Cslib.Circuits.Formula.restrict_input_of_eq_none {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) {i : Fin n} (h : ρ i = none) :
            restrict ρ (input i) = input i
            source
            theorem Cslib.Circuits.Formula.restrict_input_of_eq_some {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) {i : Fin n} {b : Bool} (h : ρ i = some b) :
            restrict ρ (input i) = const b
            source
            @[simp]
            theorem Cslib.Circuits.Formula.eval_restrict {n : ℕ} (x : BitString n) (ρ : BitString.PartialAssignment (Fin n)) (F : Formula Boolean.signature n) :
            (restrict ρ F).eval Boolean.interpretation x = F.eval Boolean.interpretation (ρ.fill x)

            A restriction computes the restricted function: it reads the fixed inputs from ρ.

            source
            theorem Cslib.Circuits.Formula.leafSize_restrict_le {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (F : Formula Boolean.signature n) :
            (restrict ρ F).leafSize ≤ leafSizeIn ρ.free F

            A restriction keeps only the leaves of the free inputs.

            source
            theorem Cslib.Circuits.Formula.leafSize_restrict_update_le {n : ℕ} (F : Formula Boolean.signature n) (i : Fin n) (b : Bool) :
            (restrict (Function.update BitString.PartialAssignment.empty i (some b)) F).leafSize + leafSizeIn {i} F ≤ F.leafSize

            Restricting by an assignment of a single input removes its leaves.

            Simplified formulas #

            source
            inductive Cslib.Circuits.Formula.IsSimplified {n : ℕ} :
            Formula Boolean.signature n → Prop

            A De Morgan formula is simplified when it has no constants and no double negations: it is built from inputs by conjunctions and disjunctions, and negations of inputs, conjunctions and disjunctions.

            Instances For
              source
              theorem Cslib.Circuits.Formula.IsSimplified.constValue?_eq_none {n : ℕ} {F : Formula Boolean.signature n} (hF : F.IsSimplified) :
              F.constValue? = none

              A simplified formula is not a constant (constValue? = none).

              source
              theorem Cslib.Circuits.Formula.IsSimplified.one_le_leafSize {n : ℕ} {F : Formula Boolean.signature n} (hF : F.IsSimplified) :
              1 ≤ F.leafSize

              A simplified formula has a leaf.

              source
              theorem Cslib.Circuits.Formula.IsSimplified.size_add_two_le {n : ℕ} {F : Formula Boolean.signature n} (hF : F.IsSimplified) :
              F.size + 2 ≤ 3 * F.leafSize

              A simplified formula with L leaves has at most 3 L - 2 operation nodes.

              source
              theorem Cslib.Circuits.Formula.restrict_eq_const_or_isSimplified {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) (F : Formula Boolean.signature n) :
              (∃ (b : Bool), restrict ρ F = const b) ∨ (restrict ρ F).IsSimplified

              A restriction is a constant or a simplified formula.

              source
              theorem Cslib.Circuits.Formula.exists_restrict_eq_const {n : ℕ} (ρ : BitString.PartialAssignment (Fin n)) {F : Formula Boolean.signature n} (h : (restrict ρ F).leafSize = 0) :
              ∃ (b : Bool), restrict ρ F = const b

              A restriction without leaves is a constant.

              Formula size #

              source
              noncomputable def Cslib.Circuits.Boolean.formulaSize {n : ℕ} (f : BooleanFunction n) :
              ℕ

              The formula size of a Boolean function: the least leaf size of a De Morgan formula computing it, Jukna's L(f) Jukna, Chapter 6. Every function has a formula (Formula.exists_computes), so the least leaf size exists.

              Instances For
                source
                theorem Cslib.Circuits.Boolean.formulaSize_le {n : ℕ} {f : BooleanFunction n} {F : Formula signature n} (hF : F.Computes interpretation f) :
                formulaSize f ≤ F.leafSize

                The formula size is at most the leaf size of every formula computing the function.

                source
                theorem Cslib.Circuits.Boolean.exists_computes_leafSize_eq {n : ℕ} (f : BooleanFunction n) :
                ∃ (F : Formula signature n), F.Computes interpretation f ∧ F.leafSize = formulaSize f

                Some formula computing the function has the least leaf size.

                source
                theorem Cslib.Circuits.Boolean.le_formulaSize_iff {n : ℕ} {f : BooleanFunction n} {k : ℕ} :
                k ≤ formulaSize f ↔ ∀ (F : Formula signature n), F.Computes interpretation f → k ≤ F.leafSize

                Lower bounds on the formula size are lower bounds on the leaf size of every formula.

                source
                @[simp]
                theorem Cslib.Circuits.Boolean.formulaSize_const {n : ℕ} (b : Bool) :
                (formulaSize fun (x : BitString n) => b) = 0

                A constant function has formula size zero.

                source
                theorem Cslib.Circuits.Boolean.formulaSize_eq_zero_of_dependsOn_empty {n : ℕ} {f : BooleanFunction n} (hf : DependsOn f ∅) :
                formulaSize f = 0

                A function of no inputs has formula size zero.

                source
                theorem Cslib.Circuits.Boolean.formulaSize_comp_fill_le_leafSizeIn {n : ℕ} {f : BooleanFunction n} {F : Formula signature n} (hF : F.Computes interpretation f) (ρ : BitString.PartialAssignment (Fin n)) :
                formulaSize (f ∘ ρ.fill) ≤ Formula.leafSizeIn ρ.free F

                A restriction of a formula computing f computes the restriction of f, with only the leaves of the free inputs.

                source
                theorem Cslib.Circuits.Boolean.formulaSize_comp_fill_le {n : ℕ} (f : BooleanFunction n) (ρ : BitString.PartialAssignment (Fin n)) :
                formulaSize (f ∘ ρ.fill) ≤ formulaSize f

                Restricting a Boolean function by a partial assignment does not increase its formula size.

                source
                theorem Cslib.Circuits.Boolean.leafSizeIn_eq_leafSize_of_dependsOn {n : ℕ} {f : BooleanFunction n} {S : Finset (Fin n)} (hf : DependsOn f ↑S) {F : Formula signature n} (hF : F.Computes interpretation f) (hmin : F.leafSize = formulaSize f) :
                Formula.leafSizeIn S F = F.leafSize

                A formula of least leaf size for a function depending only on the inputs in S has all its leaves in S.

                source
                theorem Cslib.Circuits.Boolean.exists_computes_size_le {n : ℕ} (f : BooleanFunction n) :
                ∃ (F : Formula signature n), F.Computes interpretation f ∧ F.leafSize = formulaSize f ∧ ((∃ (b : Bool), F = Formula.const b) ∨ F.size + 2 ≤ 3 * formulaSize f)

                Every function has a formula of least leaf size that is a constant or has at most 3 L - 2 operation nodes for L leaves.