not_isSome_eq_isNone'
plain-language theorem explainer
The lemma asserts that negating the isSome check on an Option equals checking isNone, for any type. SAT backpropagation proofs cite this identity when simplifying conditions on partial assignments during XOR constraint handling. The proof is a one-line wrapper that cases on the Option and closes by reflexivity.
Claim. For any type $α$ and option $o : Option α$, $¬(o.isSome) = o.isNone$.
background
PartialAssignment is defined as a function Var n → Option Bool, with none marking unknown values and some b marking determined booleans. The module develops backward propagation over CNF formulas that include XOR constraints, using these partial assignments to track determined literals. This lemma supplies a basic Option identity employed in state updates and correctness checks.
proof idea
The proof is a one-line wrapper that applies the cases tactic to the Option o and closes both branches by reflexivity.
why it matters
It feeds the proved theorem xorMissing_correct, which establishes that xorMissing recovers the correct value for the missing variable when an assignment satisfies the XOR constraint. The result strengthens the semantic correctness argument for backpropagation in the SAT complexity module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.