xorMissing_correct

formal source

 210    then a(v) = X.parity ⊕ (⊕_{w ≠ v} a(w)).
 211
 212    **Status**: PROVED (formerly axiom) -/
 213theorem xorMissing_correct {n} (σ : PartialAssignment n) (a : Assignment n) (X : XORConstraint n)
 214    (v : Var n) (b : Bool)
 215    (hcompat : compatible σ a)
 216    (hsat : satisfiesXOR a X)
 217    (hmiss : xorMissing σ X = some (v, b)) :
 218    b = a v := by
 219  unfold xorMissing at hmiss
 220  simp only at hmiss
 221  split at hmiss
 222  case isTrue h_len1 =>
 223    simp only [Option.some.injEq, Prod.mk.injEq] at hmiss
 224    obtain ⟨hv_eq, hb_eq⟩ := hmiss
 225
 226    set unknowns := X.vars.filter (fun w => (σ w).isNone) with h_unknowns_def
 227    set known := X.vars.filter (fun w => (σ w).isSome) with h_known_def
 228
 229    have h_unknowns_singleton : unknowns = [v] := by
 230      have h := list_singleton_of_length_one' unknowns h_len1
 231      rw [h, hv_eq]
 232
 233    unfold satisfiesXOR at hsat
 234
 235    have h_split := parityOf_filter_split' a X.vars (fun w => (σ w).isSome)
 236    have h_filter_eq : X.vars.filter (fun w => !(σ w).isSome) = unknowns := by
 237      simp only [h_unknowns_def]; congr 1; ext w; exact not_isSome_eq_isNone' (σ w)
 238    rw [h_filter_eq, h_unknowns_singleton] at h_split
 239
 240    have h_par_v : parityOf a [v] = a v := by simp [parityOf]
 241    rw [h_par_v, ← h_known_def] at h_split
 242    rw [hsat] at h_split
 243