list_singleton_of_length_one'
plain-language theorem explainer
Any list of length exactly one equals the singleton containing its element at index zero. This helper supports extraction of the unique unknown variable inside xorMissing for XOR constraints under partial assignments. The proof proceeds by exhaustive case analysis on list constructors, with the length hypothesis eliminating the empty and longer cases via simplification.
Claim. Let $l$ be a list over a type $A$ such that the length of $l$ equals 1. Then $l$ equals the singleton list whose sole element is the entry of $l$ at position zero.
background
The module treats partial assignments in which none marks an unknown variable and some b marks a determined Boolean value. In xorMissing, the variables of an XOR constraint are filtered to those whose values remain unknown under the partial assignment; the resulting list of unknowns is checked for length one before indexing. This lemma supplies the equality needed to equate that filtered list with its singleton form for safe extraction via get. Upstream, the xorMissing definition itself performs the length-one check and the initial indexing step that this lemma justifies. Module-level imports of unrelated list constants (plot families, kinship systems, ore classes) do not affect the list lemma.
proof idea
The term proof matches on the structure of the input list. The empty-list case yields a contradiction with the length hypothesis after simplification. The singleton case reduces directly to the required equality. The two-or-more-elements case again contradicts the length hypothesis after simplification.
why it matters
The lemma is invoked inside the proof of xorMissing_correct, which establishes that the Boolean returned by xorMissing equals the value under any satisfying assignment. It therefore closes the indexing step required for the backpropagation procedure on XOR constraints. Within the Recognition framework the result contributes to the complexity module by guaranteeing deterministic extraction when exactly one variable remains undetermined, consistent with the uniqueness steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.