getD_of_compat_isSome'
Known values in a partial assignment compatible with a total assignment must match the total assignment on those variables. Researchers deriving parity equalities for known bits under XOR constraints during SAT backpropagation cite this step. The proof uses case analysis on the option at the target variable, with compatibility forcing equality after ruling out the unknown case.
claimLet $n$ be a natural number, $σ : Var(n) → Option(Bool)$ a partial assignment, $a : Var(n) → Bool$ a total assignment, and $w : Var(n)$ a variable. If $σ$ is compatible with $a$ (i.e., $∀ v, σ(v) = some(a(v)) ∨ σ(v) = none$) and $σ(w)$ is defined, then getD($σ(w)$, false) = $a(w)$.
background
In this module partial assignments are functions from variables to Option Bool, where none marks an unknown bit and some b marks a determined value. Compatibility of $σ$ with a total assignment $a$ is the proposition that $σ$ agrees with $a$ wherever $σ$ is defined: for every variable $v$, either $σ(v) = some(a(v))$ or $σ(v) = none$. The module treats these objects as the state for backward propagation over CNF formulas that also contain XOR constraints. The lemma depends on the upstream definitions of compatible, the two Assignment types (Fin n → Bool), and Var as Fin n.
proof idea
The term proof begins with cases on the hypothesis $h : σ w$. The none branch yields an immediate contradiction with the isSome hypothesis after simp. The some b branch invokes compatibility at $w$, producing either an equality $b = a w$ or a none; the none disjunct is eliminated by simp, leaving the equality. Option.getD on some b then returns $b$, which equals $a w$ by the equality obtained from Option.some.injEq.
why it matters in Recognition Science
The lemma supplies the value-extraction step required by the downstream knownParity_eq_parityOf_known' lemma, which equates the fold of known bits under XOR to the parity of the filtered known variables. It therefore supports the entire backpropagation machinery for SAT instances that mix clauses and parity constraints. No direct link exists to the T0-T8 forcing chain or the Recognition Composition Law; the result remains internal to the complexity encoding layer.
scope and limits
- Does not prove preservation of compatibility after a setVar update.
- Does not apply when the variable remains unknown in the partial assignment.
- Does not propagate values across clauses or XOR constraints.
- Does not guarantee existence or uniqueness of a compatible total assignment.
formal statement (Lean)
165private lemma getD_of_compat_isSome' {n} (σ : PartialAssignment n) (a : Assignment n) (w : Var n)
166 (hcompat : compatible σ a) (hsome : (σ w).isSome = true) :
167 (σ w).getD false = a w := by
proof body
Term-mode proof.
168 cases h : σ w with
169 | none => simp [h] at hsome
170 | some b =>
171 simp only [Option.getD_some]
172 have := hcompat w; rw [h] at this
173 rcases this with heq | hn
174 · exact Option.some.injEq b (a w) |>.mp heq
175 · simp at hn
176