getD_of_compat_isSome'

formal source

 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
 177private lemma knownParity_eq_parityOf_known' {n} (σ : PartialAssignment n) (a : Assignment n)
 178    (X : XORConstraint n) (hcompat : compatible σ a) :
 179    X.vars.foldl (fun acc w => if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) false =
 180    parityOf a (X.vars.filter (fun w => (σ w).isSome)) := by
 181  suffices h : ∀ init,
 182    X.vars.foldl (fun acc w => if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) init =
 183    Bool.xor init (parityOf a (X.vars.filter (fun w => (σ w).isSome))) by
 184    specialize h false; simp at h; exact h
 185  intro init
 186  induction X.vars generalizing init with
 187  | nil => simp [parityOf]
 188  | cons w ws ih =>
 189    simp only [List.foldl_cons]
 190    by_cases hw : (σ w).isSome
 191    · simp only [hw, ↓reduceIte, List.filter_cons_of_pos]
 192      have hgetD : (σ w).getD false = a w := getD_of_compat_isSome' σ a w hcompat hw
 193      rw [hgetD, ih (Bool.xor init (a w)), parityOf_cons, Bool.xor_assoc]
 194    · simp only [hw, Bool.false_eq_true, ↓reduceIte, List.filter_cons_of_neg, not_false_eq_true]
 195      exact ih init