IndisputableMonolith.Complexity.SAT.Backprop
IndisputableMonolith/Complexity/SAT/Backprop.lean · 462 lines · 31 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Complexity.SAT.CNF
3import IndisputableMonolith.Complexity.SAT.XOR
4
5namespace IndisputableMonolith
6namespace Complexity
7namespace SAT
8
9/-- Partial assignments for backpropagation: `none` = unknown, `some b` = determined. -/
10abbrev PartialAssignment (n : Nat) := Var n → Option Bool
11
12/-- Backward-propagation state over a CNF with XOR constraints. -/
13structure BPState (n : Nat) where
14 assign : PartialAssignment n
15
16/-- Update a partial assignment at variable `v` to value `b`. -/
17def setVar {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) : PartialAssignment n :=
18 fun w => if w = v then some b else σ w
19
20@[simp] lemma setVar_same {n} (σ : PartialAssignment n) (v : Var n) (b : Bool) :
21 setVar σ v b v = some b := by
22 unfold setVar; simp
23
24lemma setVar_ne {n} (σ : PartialAssignment n) (v w : Var n) (b : Bool) (hvw : w ≠ v) :
25 setVar σ v b w = σ w := by
26 unfold setVar
27 simp only [ite_eq_right_iff]
28 intro heq
29 exact absurd heq hvw
30
31/-- Evaluate a literal under a partial assignment. -/
32def valueOfLit {n} (σ : PartialAssignment n) : Lit n → Option Bool
33 | .pos v => σ v
34 | .neg v => Option.map not (σ v)
35
36/-- Evaluate a clause under a partial assignment: returns `some b` if all literals
37 are known, otherwise none. -/
38def valueOfClause {n} (σ : PartialAssignment n) (C : Clause n) : Option Bool :=
39 let vals := C.map (valueOfLit σ)
40 if vals.all Option.isSome then
41 some (vals.any fun o => o.getD false)
42 else
43 none
44
45/-- Evaluate an XOR constraint under a partial assignment: returns `some b` if all
46 vars are known, else none. -/
47def valueOfXOR {n} (σ : PartialAssignment n) (X : XORConstraint n) : Option Bool :=
48 if X.vars.all (fun v => (σ v).isSome) then
49 some (X.vars.foldl (fun acc v => Bool.xor acc ((σ v).getD false)) false)
50 else
51 none
52
53/-- If exactly one variable of an XOR constraint is unknown, return that variable and the
54 value needed to satisfy the parity given the known variables. -/
55def xorMissing {n} (σ : PartialAssignment n) (X : XORConstraint n) : Option (Var n × Bool) :=
56 let unknowns := X.vars.filter (fun v => (σ v).isNone)
57 if h : unknowns.length = 1 then
58 let v := unknowns.get ⟨0, by omega⟩
59 let knownParity := X.vars.foldl (fun acc w =>
60 if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) false
61 some (v, Bool.xor X.parity knownParity)
62 else
63 none
64
65/-- If exactly one literal of a clause is unknown and the others are false, return that var and required value. -/
66def clauseUnit {n} (σ : PartialAssignment n) (C : Clause n) : Option (Var n × Bool) :=
67 let vals := C.map (valueOfLit σ)
68 let unknowns := C.zip vals |>.filter (fun ⟨_, o⟩ => o.isNone)
69 if h1 : unknowns.length = 1 then
70 if (vals.filter Option.isSome).all (fun o => o.getD false = false) then
71 let l := unknowns.get ⟨0, by omega⟩
72 match l.fst with
73 | .pos v => some (v, true)
74 | .neg v => some (v, false)
75 else none
76 else none
77
78/-- A (single) backpropagation step relation with guarded rules. -/
79inductive BPStep {n} (φ : CNF n) (H : XORSystem n) : BPState n → BPState n → Prop
80 | xor_push
81 {s : BPState n}
82 (X : XORConstraint n)
83 (v : Var n)
84 (b : Bool)
85 (hX : X ∈ H)
86 (hmiss : xorMissing s.assign X = some (v, b))
87 : BPStep φ H s { assign := setVar s.assign v b }
88 | clause_unit
89 {s : BPState n}
90 (C : Clause n)
91 (v : Var n)
92 (b : Bool)
93 (hC : C ∈ φ.clauses)
94 (hmiss : clauseUnit s.assign C = some (v, b))
95 : BPStep φ H s { assign := setVar s.assign v b }
96 -- Additional gate placeholders (to be refined with circuit semantics):
97 | and_one {s : BPState n} : BPStep φ H s s
98 | and_zero {s : BPState n} : BPStep φ H s s
99 | or_one {s : BPState n} : BPStep φ H s s
100 | or_zero {s : BPState n} : BPStep φ H s s
101 | not_flip {s : BPState n} : BPStep φ H s s
102 | wire_prop {s : BPState n} : BPStep φ H s s
103
104/-- Predicate: state is complete (all variables determined). -/
105def complete {n} (s : BPState n) : Prop :=
106 ∀ v, (s.assign v).isSome = true
107
108/-- Predicate: state is consistent with φ ∧ H (semantic notion). -/
109def consistent {n} (s : BPState n) (φ : CNF n) (H : XORSystem n) : Prop :=
110 ∃ a : Assignment n, (∀ v, s.assign v = some (a v)) ∧
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
145
146private lemma parityOf_filter_split' {n} (a : Assignment n) (vs : List (Var n)) (p : Var n → Bool) :
147 parityOf a vs = Bool.xor
148 (parityOf a (vs.filter p))
149 (parityOf a (vs.filter (fun v => !p v))) := by
150 induction vs with
151 | nil => simp [parityOf]
152 | cons v vs ih =>
153 simp only [parityOf_cons, List.filter_cons]
154 by_cases hp : p v
155 · have h1 : (if p v then v :: vs.filter p else vs.filter p) = v :: vs.filter p := by simp [hp]
156 have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
157 vs.filter (fun v => !p v) := by simp [hp]
158 rw [h1, h2, parityOf_cons, ih, Bool.xor_assoc]
159 · have h1 : (if p v then v :: vs.filter p else vs.filter p) = vs.filter p := by simp [hp]
160 have h2 : (if !p v then v :: vs.filter (fun v => !p v) else vs.filter (fun v => !p v)) =
161 v :: vs.filter (fun v => !p v) := by simp [hp]
162 rw [h1, h2, parityOf_cons, ih]
163 exact xor_comm_assoc' _ _ _
164
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
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
177private lemma knownParity_eq_parityOf_known' {n} (σ : PartialAssignment n) (a : Assignment n)
178 (X : XORConstraint n) (hcompat : compatible σ a) :
179 X.vars.foldl (fun acc w => if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) false =
180 parityOf a (X.vars.filter (fun w => (σ w).isSome)) := by
181 suffices h : ∀ init,
182 X.vars.foldl (fun acc w => if (σ w).isSome then Bool.xor acc ((σ w).getD false) else acc) init =
183 Bool.xor init (parityOf a (X.vars.filter (fun w => (σ w).isSome))) by
184 specialize h false; simp at h; exact h
185 intro init
186 induction X.vars generalizing init with
187 | nil => simp [parityOf]
188 | cons w ws ih =>
189 simp only [List.foldl_cons]
190 by_cases hw : (σ w).isSome
191 · simp only [hw, ↓reduceIte, List.filter_cons_of_pos]
192 have hgetD : (σ w).getD false = a w := getD_of_compat_isSome' σ a w hcompat hw
193 rw [hgetD, ih (Bool.xor init (a w)), parityOf_cons, Bool.xor_assoc]
194 · simp only [hw, Bool.false_eq_true, ↓reduceIte, List.filter_cons_of_neg, not_false_eq_true]
195 exact ih init
196
197private lemma list_singleton_of_length_one' {α : Type*} (l : List α) (h : l.length = 1) :
198 l = [l.get ⟨0, by omega⟩] := by
199 match l with
200 | [] => simp at h
201 | [x] => simp
202 | _ :: _ :: _ => simp at h
203
204/-- **PROVED**: xorMissing produces the correct value for a satisfying assignment.
205 If exactly one variable v is unknown in XOR constraint X, and a satisfies X,
206 then the value returned by xorMissing equals a v.
207
208 **Mathematical justification**: XOR is linear over GF(2).
209 If ⊕_{w ∈ X.vars} a(w) = X.parity and we know all values except a(v),
210 then a(v) = X.parity ⊕ (⊕_{w ≠ v} a(w)).
211
212 **Status**: PROVED (formerly axiom) -/
213theorem xorMissing_correct {n} (σ : PartialAssignment n) (a : Assignment n) (X : XORConstraint n)
214 (v : Var n) (b : Bool)
215 (hcompat : compatible σ a)
216 (hsat : satisfiesXOR a X)
217 (hmiss : xorMissing σ X = some (v, b)) :
218 b = a v := by
219 unfold xorMissing at hmiss
220 simp only at hmiss
221 split at hmiss
222 case isTrue h_len1 =>
223 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss
224 obtain ⟨hv_eq, hb_eq⟩ := hmiss
225
226 set unknowns := X.vars.filter (fun w => (σ w).isNone) with h_unknowns_def
227 set known := X.vars.filter (fun w => (σ w).isSome) with h_known_def
228
229 have h_unknowns_singleton : unknowns = [v] := by
230 have h := list_singleton_of_length_one' unknowns h_len1
231 rw [h, hv_eq]
232
233 unfold satisfiesXOR at hsat
234
235 have h_split := parityOf_filter_split' a X.vars (fun w => (σ w).isSome)
236 have h_filter_eq : X.vars.filter (fun w => !(σ w).isSome) = unknowns := by
237 simp only [h_unknowns_def]; congr 1; ext w; exact not_isSome_eq_isNone' (σ w)
238 rw [h_filter_eq, h_unknowns_singleton] at h_split
239
240 have h_par_v : parityOf a [v] = a v := by simp [parityOf]
241 rw [h_par_v, ← h_known_def] at h_split
242 rw [hsat] at h_split
243
244 have h_known_par := knownParity_eq_parityOf_known' σ a X hcompat
245 rw [← h_known_def] at h_known_par
246
247 rw [← hb_eq, h_known_par, h_split]
248 exact xor_comm_cancel' (a v) (parityOf a known)
249
250 case isFalse h => simp at hmiss
251
252/-!
253## Semantic Correctness for Unit Propagation
254
255The clauseUnit function produces the correct value for a satisfying assignment.
256This is now a **proved theorem**, not an axiom.
257-/
258
259-- Helper lemmas for clauseUnit_correct proof
260private lemma not_isSome_iff_isNone' {α : Type*} (o : Option α) : ¬o.isSome ↔ o.isNone := by
261 cases o <;> simp
262
263private lemma singleton_eq_get_zero' {α : Type*} (l : List α) (h : l.length = 1) :
264 ∃ x, l = [x] ∧ x = l.get ⟨0, by omega⟩ := by
265 match l with
266 | [] => simp at h
267 | [x] => exact ⟨x, rfl, rfl⟩
268 | _ :: _ :: _ => simp at h
269
270private lemma mem_zip_of_getElem' {α β : Type*} (l1 : List α) (l2 : List β) (i : Nat)
271 (hi1 : i < l1.length) (hi2 : i < l2.length) :
272 (l1[i], l2[i]) ∈ l1.zip l2 := by
273 rw [List.mem_iff_getElem]
274 have hi : i < (l1.zip l2).length := by simp; omega
275 exact ⟨i, hi, by simp⟩
276
277private lemma known_lit_false'' {n} (σ : PartialAssignment n) (a : Assignment n) (l : Lit n)
278 (hcompat : compatible σ a) (hsome : (valueOfLit σ l).isSome)
279 (hfalse : (valueOfLit σ l).getD false = false) :
280 evalLit a l = false := by
281 have heq : valueOfLit σ l = some (evalLit a l) := by
282 cases l with
283 | pos v =>
284 simp only [valueOfLit, evalLit] at *
285 rcases hcompat v with h | h
286 · exact h
287 · simp [h] at hsome
288 | neg v =>
289 simp only [valueOfLit, evalLit, Option.map] at *
290 rcases hcompat v with h | h
291 · simp [h]
292 · simp [h] at hsome
293 cases hv : valueOfLit σ l with
294 | none => simp [hv] at hsome
295 | some b =>
296 simp only [hv, Option.getD_some] at hfalse heq
297 simp only [Option.some.injEq] at heq
298 rw [← heq, hfalse]
299
300/-- **PROVED**: clauseUnit produces the correct value for a satisfying assignment.
301 If exactly one literal is unknown in clause C, all known literals are false,
302 and a satisfies C, then the value returned by clauseUnit equals a v.
303
304 **Mathematical justification**: A clause is satisfied iff at least one literal is true.
305 If all known literals are false under a (by compatibility), and a satisfies C,
306 then the unknown literal must be the satisfying one.
307 - For .pos v: the literal is true iff a v = true
308 - For .neg v: the literal is true iff a v = false
309
310 **Status**: PROVED (formerly axiom) -/
311theorem clauseUnit_correct {n} (σ : PartialAssignment n) (a : Assignment n) (C : Clause n)
312 (v : Var n) (b : Bool)
313 (hcompat : compatible σ a)
314 (hsat : evalClause a C = true)
315 (hmiss : clauseUnit σ C = some (v, b)) :
316 b = a v := by
317 unfold clauseUnit at hmiss
318 simp only at hmiss
319
320 split at hmiss
321 case isFalse h => simp at hmiss
322 case isTrue h_len1 =>
323 split at hmiss
324 case isFalse h => simp at hmiss
325 case isTrue h_all_false =>
326 -- Set up unknowns
327 set unknowns := (C.zip (C.map (valueOfLit σ))).filter (fun ⟨_, o⟩ => o.isNone) with hunk_def
328 have h_len1' : unknowns.length = 1 := h_len1
329
330 -- Get the singleton element
331 obtain ⟨unk, h_singleton, hunk_get⟩ := singleton_eq_get_zero' unknowns h_len1'
332
333 -- Known literals are false
334 have h_known_false : ∀ l ∈ C, (valueOfLit σ l).isSome → evalLit a l = false := by
335 intro l hl_in hsome
336 have hval_in : valueOfLit σ l ∈ (C.map (valueOfLit σ)).filter Option.isSome := by
337 simp only [List.mem_filter, List.mem_map]
338 exact ⟨⟨l, hl_in, rfl⟩, hsome⟩
339 rw [List.all_eq_true] at h_all_false
340 simp only [decide_eq_true_eq] at h_all_false
341 exact known_lit_false'' σ a l hcompat hsome (h_all_false _ hval_in)
342
343 -- Some literal is true
344 rw [evalClause, List.any_eq_true] at hsat
345 obtain ⟨l_sat, hl_in, hl_true⟩ := hsat
346
347 -- l_sat must be unknown
348 have hl_unknown : (valueOfLit σ l_sat).isNone := by
349 rw [← not_isSome_iff_isNone']
350 intro hsome
351 have hfalse := h_known_false l_sat hl_in hsome
352 rw [hl_true] at hfalse
353 cases hfalse
354
355 -- l_sat is in unknowns
356 have hl_in_unk : (l_sat, valueOfLit σ l_sat) ∈ unknowns := by
357 rw [hunk_def, List.mem_filter]
358 constructor
359 · have hlen : C.length = (C.map (valueOfLit σ)).length := by simp
360 obtain ⟨i, hi, hget⟩ := List.mem_iff_getElem.mp hl_in
361 have hi2 : i < (C.map (valueOfLit σ)).length := by simp; omega
362 have hmem := mem_zip_of_getElem' C (C.map (valueOfLit σ)) i hi hi2
363 simp only [List.getElem_map, hget] at hmem
364 exact hmem
365 · exact hl_unknown
366
367 -- Since unknowns = [unk], l_sat = unk.fst
368 rw [h_singleton, List.mem_singleton] at hl_in_unk
369 have hl_eq : l_sat = unk.fst := congrArg Prod.fst hl_in_unk
370
371 -- Rewrite hmiss using hunk_get
372 have hmiss' : (match unk.fst with
373 | .pos v => some (v, true)
374 | .neg v => some (v, false)) = some (v, b) := by
375 convert hmiss using 2
376 rw [← hunk_get]
377
378 -- Case analysis on unk.fst
379 cases hl : unk.fst with
380 | pos w =>
381 simp only [hl] at hmiss'
382 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
383 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
384 subst hv_eq hb_eq
385 rw [hl_eq, hl] at hl_true
386 simp only [evalLit] at hl_true
387 exact hl_true.symm
388
389 | neg w =>
390 simp only [hl] at hmiss'
391 simp only [Option.some.injEq, Prod.mk.injEq] at hmiss'
392 obtain ⟨hv_eq, hb_eq⟩ := hmiss'
393 subst hv_eq hb_eq
394 rw [hl_eq, hl] at hl_true
395 simp only [evalLit, Bool.not_eq_true'] at hl_true
396 exact hl_true.symm
397
398/-- Soundness of one step: preserves compatibility with any model. -/
399lemma bp_step_sound {n} (φ : CNF n) (H : XORSystem n)
400 {s t : BPState n} :
401 BPStep φ H s t →
402 ∀ a : Assignment n, evalCNF a φ = true → satisfiesSystem a H →
403 compatible s.assign a → compatible t.assign a := by
404 intro hstep a hφ hH hcompat
405 cases hstep with
406 | xor_push X v b hX hmiss =>
407 -- Need to show: compatible (setVar s.assign v b) a
408 -- Since a satisfies X and xorMissing gave us (v, b), we need b = a v
409 have hXsat : satisfiesXOR a X := hH X hX
410 have hbeq : b = a v := xorMissing_correct s.assign a X v b hcompat hXsat hmiss
411 subst hbeq
412 exact compatible_setVar s.assign a v hcompat
413 | clause_unit C v b hC hmiss =>
414 -- Need to show: compatible (setVar s.assign v b) a
415 -- Since a satisfies C and clauseUnit gave us (v, b), we need b = a v
416 have hCsat : evalClause a C = true := by
417 unfold evalCNF at hφ
418 simp only [List.all_eq_true] at hφ
419 exact hφ C hC
420 have hbeq : b = a v := clauseUnit_correct s.assign a C v b hcompat hCsat hmiss
421 subst hbeq
422 exact compatible_setVar s.assign a v hcompat
423 | and_one => exact hcompat
424 | and_zero => exact hcompat
425 | or_one => exact hcompat
426 | or_zero => exact hcompat
427 | not_flip => exact hcompat
428 | wire_prop => exact hcompat
429
430/-- Monotonicity: steps never unassign known values. -/
431lemma bp_step_monotone {n} (φ : CNF n) (H : XORSystem n)
432 {s t : BPState n} :
433 BPStep φ H s t →
434 ∀ v, (s.assign v).isSome → (t.assign v).isSome := by
435 intro hstep v hv
436 cases hstep with
437 | xor_push X v_pushed b_pushed hX hmiss =>
438 by_cases hvv : v = v_pushed
439 · subst hvv; simp only [setVar_same, Option.isSome_some]
440 · show (setVar s.assign v_pushed b_pushed v).isSome = true
441 rw [setVar_ne _ _ _ _ hvv]; exact hv
442 | clause_unit C v_pushed b_pushed hC hmiss =>
443 by_cases hvv : v = v_pushed
444 · subst hvv; simp only [setVar_same, Option.isSome_some]
445 · show (setVar s.assign v_pushed b_pushed v).isSome = true
446 rw [setVar_ne _ _ _ _ hvv]; exact hv
447 | and_one => exact hv
448 | and_zero => exact hv
449 | or_one => exact hv
450 | or_zero => exact hv
451 | not_flip => exact hv
452 | wire_prop => exact hv
453
454/-- Backpropagation succeeds if every legal start reaches a complete consistent state. -/
455def BackpropSucceeds {n} (φ : CNF n) (H : XORSystem n) : Prop :=
456 ∀ (_s0 : BPState n),
457 ∃ s, complete s ∧ consistent s φ H
458
459end SAT
460end Complexity
461end IndisputableMonolith
462