singleton_eq_get_zero'
plain-language theorem explainer
Any list of length exactly one equals the singleton list containing its zeroth element. It is invoked inside the correctness proof for unit-clause propagation in SAT backpropagation. The argument proceeds by structural case analysis on the list, with length contradictions eliminating the empty and longer cases.
Claim. Let $l$ be a list over type $α$ with $|l|=1$. Then there exists $x$ such that $l=[x]$ and $x$ equals the element of $l$ at index zero.
background
The module treats partial assignments for SAT backpropagation, where none denotes an unknown variable and some b a determined Boolean value. The lemma extracts the unique element from a length-one list, a situation that occurs when a clause has exactly one unknown literal. It depends on the vantage projection that selects the inside, act, or outside component of a value triple.
proof idea
The proof matches on the list structure. The empty-list case contradicts the length hypothesis by simp. The singleton case directly supplies the witness with reflexivity. The two-or-more case again contradicts the length hypothesis by simp.
why it matters
The lemma supports clauseUnit_correct, which proves that unit propagation returns the correct Boolean value for the unknown literal when the assignment satisfies the clause. It supplies a technical extraction step inside the backpropagation correctness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.