Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Boolean functions as an m-semiring

Lax392996.BooleanFunctions · concepts/Lax392996/BooleanFunctions.lean · lax-392996

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    The m-semiring B[X]\mathcal{B}[X] of Boolean functions over a set XX of Boolean variables: elements are the functions (X→{⊥,⊤})→{⊥,⊤}(X \to \{\bot, \top\}) \to \{\bot, \top\}, with pointwise ∨\lor as ⊕\oplus, pointwise ∧\land as ⊗\otimes, the constant functions ⊥\bot and ⊤\top as 0\mathbb{0} and 1\mathbb{1}, pointwise implication as the natural order and (a,b)↦a∧¬b(a, b) \mapsto a \land \lnot b as ⊖\ominus; δ\delta is the identity. Equality of two Boolean functions is decidable classically, which is what the annotated semantics requires of an annotation type.

    Concept map
    2 concepts; 5 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 4 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Algebra.Ring.Defs
    2import Mathlib.Order.Basic
    3import Lax392996.SemiringsWithMonus
    4
    5/-!
    6---
    7title: Boolean functions as an m-semiring
    8type: definition
    9---
    10The m-semiring B[X]\mathcal{B}[X] of Boolean functions over a set XX of
    11Boolean variables: elements are the functions (X→{⊥,⊤})→{⊥,⊤}(X \to \{\bot, \top\}) \to \{\bot, \top\}
    12, with pointwise ∨\lor as ⊕\oplus, pointwise ∧\land as
    13⊗\otimes, the constant functions ⊥\bot and ⊤\top as 0\mathbb{0} and
    141\mathbb{1}, pointwise implication as the natural order and (a,b)↦a∧¬b(a, b) \mapsto a \land \lnot b
    15 as ⊖\ominus; δ\delta is the identity. Equality of two
    16Boolean functions is decidable classically, which is what the annotated
    17semantics requires of an annotation type.
    18-/
    19
    20namespace Lax392996.BooleanFunctions
    21
    22open Lax392996.SemiringsWithMonus
    23
    24variable {X : Type}
    25
    26/-- The type of Boolean functions over Boolean assignments to `X`:
    27`(X → Bool) → Bool` with pointwise operations. -/
    28def BoolFunc (X : Type) := (X → Bool) → Bool
    29
    30instance instZeroBoolFunc : Zero (BoolFunc X) := ⟨λ _ ↦ False⟩
    31
    32instance instAddBoolFunc : Add (BoolFunc X) := ⟨λ f₁ f₂ ν ↦ (f₁ ν) || (f₂ ν)⟩
    33
    34instance instOneBoolFunc : One (BoolFunc X) := ⟨λ _ ↦ True⟩
    35
    36instance instMulBoolFunc : Mul (BoolFunc X) := ⟨λ f₁ f₂ ν ↦ (f₁ ν) && (f₂ ν)⟩
    37
    38instance instLEBoolFunc : LE (BoolFunc X) := ⟨λ f₁ f₂ ↦ ∀ ν : X → Bool, (f₁ ν) ≤ (f₂ ν)⟩
    39
    40instance instSubBoolFunc : Sub (BoolFunc X) := ⟨λ f₁ f₂ ν ↦ (f₁ ν) && !(f₂ ν)⟩
    41
    42instance instCommSemiringBoolFunc : CommSemiring (BoolFunc X) where
    43 add_assoc := by
    44 intro a b c
    45 simp[(· + ·),Add.add]
    46 apply funext
    47 intro x
    48 exact Bool.or_assoc _ _ _
    49
    50 add_comm := by
    51 intro a b
    52 simp[(· + ·),Add.add]
    53 apply funext
    54 intro x
    55 exact Bool.or_comm _ _
    56
    57 zero_add := by tauto
    58
    59 add_zero := by
    60 simp[(· + ·),Add.add]
    61 intro a
    62 apply funext
    63 simp
    64 tauto
    65
    66 nsmul := nsmulRec
    67
    68 left_distrib := by
    69 simp[(· + ·),Add.add,(· * ·),Mul.mul]
    70 intro a b c
    71 apply funext
    72 intro x
    73 exact Bool.and_or_distrib_left _ _ _
    74
    75 right_distrib := by
    76 simp[(· + ·),Add.add,(· * ·),Mul.mul]
    77 intro a b c
    78 apply funext
    79 intro x
    80 exact Bool.and_or_distrib_right _ _ _
    81
    82 zero_mul := by tauto
    83
    84 mul_zero := by
    85 simp[(· * ·),Mul.mul]
    86 intro a
    87 apply funext
    88 simp
    89 tauto
    90
    91 mul_assoc := by
    92 intro a b c
    93 simp[(· * ·),Mul.mul]
    94 apply funext
    95 intro x
    96 exact Bool.and_assoc _ _ _
    97
    98 mul_comm := by
    99 intro a b
    100 simp[(· * ·),Mul.mul]
    101 apply funext
    102 intro x
    103 exact Bool.and_comm _ _
    104
    105 one_mul := by tauto
    106
    107 mul_one := by
    108 simp[(· * ·),Mul.mul]
    109 intro a
    110 apply funext
    111 simp
    112 tauto
    113
    114/-- `BoolFunc X` is a commutative m-semiring with pointwise `||` as addition,
    115pointwise `&&` as multiplication, and pointwise implication as natural order. -/
    116instance instSemiringWithMonusBoolFunc : SemiringWithMonus (BoolFunc X) where
    117 le_refl := by tauto
    118
    119 le_trans := by tauto
    120
    121 le_antisymm := by
    122 simp[(· ≤ ·)]
    123 intro a b hab hba
    124 apply funext
    125 intro ν
    126 exact Bool.le_antisymm (hab ν) (hba ν)
    127
    128 le_self_add := by
    129 simp[(· + ·),Add.add,(· ≤ ·)]
    130 tauto
    131
    132 le_add_self := by
    133 simp[(· + ·),Add.add,(· ≤ ·)]
    134 tauto
    135
    136 add_le_add_left := by
    137 simp[(· + ·),Add.add,(· ≤ ·)]
    138 tauto
    139
    140 exists_add_of_le := by
    141 simp[(· + ·),Add.add,(· ≤ ·)]
    142 intro a b h
    143 use b
    144 apply funext
    145 intro x
    146 cases ha : a x
    147 . tauto
    148 . apply (h x) ha
    149
    150 monus_spec := by
    151 intro a b c
    152 simp[(· + ·),Add.add,(· ≤ ·),(· - ·),Sub.sub]
    153 apply Iff.intro
    154 . intro h ν ha
    155 cases hb : b ν <;> simp
    156 . exact h ν ha hb
    157 . intro h ν ha hb
    158 have h' : b ν = true ∨ c ν = true := h ν ha
    159 simp[hb] at h'
    160 exact h'
    161
    162 delta := id
    163 delta_zero := rfl
    164 delta_natCast_pos := by
    165 have hidem : ∀ a : BoolFunc X, a + a = a := fun a => funext fun ν => by
    166 show (a ν || a ν) = a ν
    167 simp
    168 have hcast : ∀ {n : ℕ}, 0 < n → (n : BoolFunc X) = 1 := by
    169 intro n hn
    170 induction n with
    171 | zero => omega
    172 | succ m ih =>
    173 rcases Nat.eq_zero_or_pos m with hm | hm
    174 · rw [hm]; simp
    175 · rw [Nat.cast_succ, ih hm, hidem 1]
    176 intro n hn
    177 exact hcast hn
    178 delta_absorb := fun a b => funext fun ν => by
    179 show (a ν && (a ν || b ν)) = a ν
    180 cases a ν <;> cases b ν <;> rfl
    181
    182/-- For finite `X`, equality of Boolean functions `(X → Bool) → Bool` is
    183decidable in principle, the function space being finite. The classical
    184decidability instance is what the annotated semantics, which requires
    185`[DecidableEq K]`, is invoked with for `K = BoolFunc X`. -/
    186noncomputable instance instDecidableEqBoolFunc : DecidableEq (BoolFunc X) :=
    187 Classical.decEq _
    188
    189end Lax392996.BooleanFunctions
    190
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…