IndisputableMonolith.Complexity.SAT.XOR

   1import Mathlib
   2import IndisputableMonolith.Complexity.SAT.CNF
   3
   4namespace IndisputableMonolith
   5namespace Complexity
   6namespace SAT
   7
   8/-- An XOR constraint over `n` variables: parity of a variable subset equals `parity`. -/
   9structure XORConstraint (n : Nat) where
  10  vars   : List (Var n)
  11  parity : Bool
  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
  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
  49  cases a <;> cases b <;> rfl
  50
  51/-- Parity of empty list is false -/
  52@[simp] lemma parityOf_nil {n} (a : Assignment n) : parityOf a [] = false := rfl
  53
  54/-- Parity of singleton is the variable value -/
  55@[simp] lemma parityOf_singleton {n} (a : Assignment n) (v : Var n) :
  56    parityOf a [v] = a v := by
  57  simp [parityOf, List.foldl]
  58
  59/-- Helper: foldl with xor starting from init -/
  60lemma foldl_xor_init {n} (a : Assignment n) (init : Bool) (vs : List (Var n)) :
  61    vs.foldl (fun acc v => Bool.xor acc (a v)) init =
  62    Bool.xor init (vs.foldl (fun acc v => Bool.xor acc (a v)) false) := by
  63  induction vs generalizing init with
  64  | nil => simp
  65  | cons v vs ih =>
  66    simp only [List.foldl_cons]
  67    rw [ih (Bool.xor init (a v)), ih (Bool.xor false (a v))]
  68    simp only [Bool.false_xor]
  69    rw [Bool.xor_assoc]
  70
  71/-- Parity of cons: XOR of head and tail parity -/
  72lemma parityOf_cons {n} (a : Assignment n) (v : Var n) (vs : List (Var n)) :
  73    parityOf a (v :: vs) = Bool.xor (a v) (parityOf a vs) := by
  74  unfold parityOf
  75  simp only [List.foldl_cons]
  76  rw [foldl_xor_init]
  77  rw [Bool.false_xor, Bool.xor_comm]
  78
  79/-- If parityOf a (v :: vs) = p and parityOf a vs = q, then a v = p ⊕ q -/
  80lemma xor_recover_value {n} (a : Assignment n) (v : Var n) (vs : List (Var n))
  81    (p q : Bool) (hp : parityOf a (v :: vs) = p) (hq : parityOf a vs = q) :
  82    a v = Bool.xor p q := by
  83  rw [parityOf_cons] at hp
  84  -- hp: (a v) ^^ (parityOf a vs) = p
  85  -- hq: parityOf a vs = q
  86  -- Goal: a v = p ^^ q
  87  subst hq
  88  -- hp: (a v) ^^ (parityOf a vs) = p
  89  -- Need: a v = p ^^ (parityOf a vs)
  90  -- From hp: a v = (a v ^^ (parityOf a vs)) ^^ (parityOf a vs) = p ^^ (parityOf a vs)
  91  calc a v = Bool.xor (Bool.xor (a v) (parityOf a vs)) (parityOf a vs) := by simp
  92    _ = Bool.xor p (parityOf a vs) := by rw [hp]
  93
  94/-- CNF "under XOR constraints": we don't rewrite into CNF; we pair them semantically. -/
  95structure CNFWithXOR (n : Nat) where
  96  φ : CNF n
  97  H : XORSystem n
  98
  99/-- Satisfiable under XOR constraints. -/
 100def SatisfiableXOR {n} (ψ : CNFWithXOR n) : Prop :=
 101  ∃ a : Assignment n, evalCNF a ψ.φ = true ∧ satisfiesSystem a ψ.H
 102
 103/-- Unique solution under XOR constraints. -/
 104def UniqueSolutionXOR {n} (ψ : CNFWithXOR n) : Prop :=
 105  ∃! a : Assignment n, evalCNF a ψ.φ = true ∧ satisfiesSystem a ψ.H
 106
 107end SAT
 108end Complexity
 109end IndisputableMonolith
 110