singleton_eq_get_zero'
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply to lists whose length differs from one.
- Does not construct the element without the length hypothesis.
- Does not extend to arrays, trees, or other container types.
formal statement (Lean)
263private lemma singleton_eq_get_zero' {α : Type*} (l : List α) (h : l.length = 1) :
264 ∃ x, l = [x] ∧ x = l.get ⟨0, by omega⟩ := by
proof body
Term-mode proof.
265 match l with
266 | [] => simp at h
267 | [x] => exact ⟨x, rfl, rfl⟩
268 | _ :: _ :: _ => simp at h
269