list_singleton_of_length_one'

formal source

 194    · simp only [hw, Bool.false_eq_true, ↓reduceIte, List.filter_cons_of_neg, not_false_eq_true]
 195      exact ih init
 196
 197private lemma list_singleton_of_length_one' {α : Type*} (l : List α) (h : l.length = 1) :
 198    l = [l.get ⟨0, by omega⟩] := by
 199  match l with
 200  | [] => simp at h
 201  | [x] => simp
 202  | _ :: _ :: _ => simp at h
 203
 204/-- **PROVED**: xorMissing produces the correct value for a satisfying assignment.
 205    If exactly one variable v is unknown in XOR constraint X, and a satisfies X,
 206    then the value returned by xorMissing equals a v.
 207
 208    **Mathematical justification**: XOR is linear over GF(2).
 209    If ⊕_{w ∈ X.vars} a(w) = X.parity and we know all values except a(v),
 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