parityOf_cons

formal source

  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