`compatible`

definition

show as: view math explainer →

module: IndisputableMonolith.Complexity.SAT.Backprop
domain: Complexity
line: 114 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Complexity.SAT.Backprop on GitHub at line 114.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 111    evalCNF a φ = true ∧ satisfiesSystem a H
 112
 113/-- Compatibility: a partial assignment agrees with a total assignment on known bits. -/
 114def compatible {n} (σ : PartialAssignment n) (a : Assignment n) : Prop :=
 115  ∀ v, σ v = some (a v) ∨ σ v = none
 116
 117/-- If σ is compatible with a and we set v to (a v), the result is still compatible. -/
 118lemma compatible_setVar {n} (σ : PartialAssignment n) (a : Assignment n) (v : Var n)
 119    (hcompat : compatible σ a) :
 120    compatible (setVar σ v (a v)) a := by
 121  intro w
 122  by_cases hwv : w = v
 123  · subst hwv
 124    left
 125    simp [setVar_same]
 126  · rw [setVar_ne σ v w (a v) hwv]
 127    exact hcompat w
 128
 129/-!
 130## Semantic Correctness for XOR Propagation
 131
 132The xorMissing function produces the correct value for a satisfying assignment.
 133This is now a **proved theorem**, not an axiom.
 134-/
 135
 136-- Helper lemmas for xorMissing_correct proof
 137private lemma not_isSome_eq_isNone' {α : Type*} (o : Option α) : (!o.isSome) = o.isNone := by
 138  cases o <;> rfl
 139
 140private lemma xor_comm_assoc' (a b c : Bool) : Bool.xor a (Bool.xor b c) = Bool.xor b (Bool.xor a c) := by
 141  cases a <;> cases b <;> cases c <;> rfl
 142
 143private lemma xor_comm_cancel' (a b : Bool) : Bool.xor (Bool.xor b a) b = a := by
 144  cases a <;> cases b <;> rfl

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.