parityOf_singleton

formal source

  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