`XORSystem`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.XOR
domain: Complexity
line: 15 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Complexity.SAT.XOR on GitHub at line 15.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  12deriving Repr
  13
  14/-- A system of XOR constraints. -/
  15abbrev XORSystem (n : Nat) := List (XORConstraint n)
  16
  17/-- Compute the XOR (parity) of selected variables of assignment `a`. -/
  18def parityOf {n} (a : Assignment n) (S : List (Var n)) : Bool :=
  19  S.foldl (fun acc v => Bool.xor acc (a v)) false
  20
  21/-- A single XOR constraint is satisfied by `a` iff the parity matches. -/
  22def satisfiesXOR {n} (a : Assignment n) (c : XORConstraint n) : Prop :=
  23  parityOf a c.vars = c.parity
  24
  25/-- An assignment satisfies an XOR system when all constraints hold. -/
  26def satisfiesSystem {n} (a : Assignment n) (H : XORSystem n) : Prop :=
  27  ∀ c ∈ H, satisfiesXOR a c
  28
  29/-! ## XOR Parity Lemmas -/
  30
  31/-- XOR is self-inverse: a ⊕ a = false -/
  32@[simp] lemma Bool.xor_self (a : Bool) : Bool.xor a a = false := by cases a <;> rfl
  33
  34/-- XOR with false is identity -/
  35@[simp] lemma Bool.xor_false' (a : Bool) : Bool.xor a false = a := by cases a <;> rfl
  36
  37/-- false XOR a = a -/
  38@[simp] lemma Bool.false_xor (a : Bool) : Bool.xor false a = a := by cases a <;> rfl
  39
  40/-- XOR is commutative -/
  41lemma Bool.xor_comm (a b : Bool) : Bool.xor a b = Bool.xor b a := by cases a <;> cases b <;> rfl
  42
  43/-- XOR is associative -/
  44lemma Bool.xor_assoc (a b c : Bool) : Bool.xor (Bool.xor a b) c = Bool.xor a (Bool.xor b c) := by
  45  cases a <;> cases b <;> cases c <;> rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.