parityOf_filter_split'

formal source

 143private lemma xor_comm_cancel' (a b : Bool) : Bool.xor (Bool.xor b a) b = a := by
 144  cases a <;> cases b <;> rfl
 145
 146private lemma parityOf_filter_split' {n} (a : Assignment n) (vs : List (Var n)) (p : Var n → Bool) :
 147    parityOf a vs = Bool.xor
 148      (parityOf a (vs.filter p))
 149      (parityOf a (vs.filter (fun v => !p v))) := by
 150  induction vs with
 151  | nil => simp [parityOf]
 152  | cons v vs ih =>
 153    simp only [parityOf_cons, List.filter_cons]
 154    by_cases hp : p v
 155    · have h1 : (if p v then v :: vs.filter p else vs.filter p) = v :: vs.filter p := by simp [hp]
 156      have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
 157                vs.filter (fun v => !p v) := by simp [hp]
 158      rw [h1, h2, parityOf_cons, ih, Bool.xor_assoc]
 159    · have h1 : (if p v then v :: vs.filter p else vs.filter p) = vs.filter p := by simp [hp]
 160      have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
 161                v :: vs.filter (fun v => !p v) := by simp [hp]
 162      rw [h1, h2, parityOf_cons, ih]
 163      exact xor_comm_assoc' _ _ _
 164
 165private lemma getD_of_compat_isSome' {n} (σ : PartialAssignment n) (a : Assignment n) (w : Var n)
 166    (hcompat : compatible σ a) (hsome : (σ w).isSome = true) :
 167    (σ w).getD false = a w := by
 168  cases h : σ w with
 169  | none => simp [h] at hsome
 170  | some b =>
 171    simp only [Option.getD_some]
 172    have := hcompat w; rw [h] at this
 173    rcases this with heq | hn
 174    · exact Option.some.injEq b (a w) |>.mp heq
 175    · simp at hn
 176