parityOf

formal source

  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
  46
  47/-- XOR cancellation: (a ⊕ b) ⊕ b = a -/
  48@[simp] lemma Bool.xor_xor_cancel_right (a b : Bool) : Bool.xor (Bool.xor a b) b = a := by