Trace.lean

1 import ProofPath.Extension
2 import Mathlib.Data.List.Basic
3 
4 /-!
5 An executable finite trace checker refining the existing Field semantics.
6 Node identifiers are natural-number slots. Rule identifiers are list positions,
7 so even identical rule rows remain distinct addresses. Out-of-range addresses
8 are rejected rather than interpreted by the default row of the total Field.
9 -/
10 namespace ProofPath.Trace
11 
12 structure Rule where
13   premises : List Nat
14   conclusion : Nat
15   deriving DecidableEq, Repr
16 
17 structure Problem where
18   nodeCount : Nat
19   leaves : List Nat
20   rules : List Rule
21   positive : List Nat
22   negative : List Nat
23   deriving DecidableEq, Repr
24 
25 structure Witness where
26   target : Nat
27   trace : List Nat
28   deriving DecidableEq, Repr
29 
30 structure Certificate where
31   feasible : Bool
32   closure : List Nat
33   trace : List Nat
34   obstruction : Option Witness
35   deriving DecidableEq, Repr
36 
37 /-- Total finite lookup with an explicit failure value. -/
38 def lookup {α : Type*} : List α → Nat → Option α
39   | [], _ => none
40   | x :: _, 0 => some x
41   | _ :: xs, i+1 => lookup xs i
42 
43 theorem lookup_mem {α : Type*} {xs : List α} {i : Nat} {a : α}
44     (h : lookup xs i = some a) : a ∈ xs := by
45   induction xs generalizing i with
46   | nil => simp [lookup] at h
47   | cons x xs ih =>
48     cases i with
49     | zero => simp [lookup] at h; simp [h]
50     | succ i => exact List.mem_cons_of_mem _ (ih h)
51 
52 theorem mem_lookup {α : Type*} {xs : List α} {a : α} (h : a ∈ xs) :
53     ∃ i, lookup xs i = some a := by
54   induction xs with
55   | nil => simp at h
56   | cons x xs ih =>
57     rcases List.mem_cons.mp h with h | h
58     · exact ⟨0, by simp [lookup, h]⟩
59     · obtain ⟨i, hi⟩ := ih h
60       exact ⟨i+1, hi⟩
61 
62 def Problem.initial (p : Problem) : List Nat := p.leaves ++ p.positive
63 
64 def Problem.field (p : Problem) : Field Nat Nat where
65   leaf := {v | v ∈ p.leaves}
66   premises j := {v | v ∈ ((lookup p.rules j).getD ⟨[], 0⟩).premises}
67   conclusion j := ((lookup p.rules j).getD ⟨[], 0⟩).conclusion
68   certified j := (lookup p.rules j).isSome = true
69 
70 def Problem.seeds (p : Problem) : Set Nat := {v | v ∈ p.positive}
71 def Problem.forbidden (p : Problem) : Set Nat := {v | v ∈ p.negative}
72 def Problem.exactClosure (p : Problem) : Set Nat := p.field.closure p.seeds
73 
74 def enabled (r : Rule) (known : List Nat) : Bool :=
75   r.premises.all (fun v => known.contains v)
76 
77 theorem enabled_iff (r : Rule) (known : List Nat) :
78     enabled r known = true ↔ ∀ v, v ∈ r.premises → v ∈ known := by
79   simp [enabled]
80 
81 /-- Repeated conclusions are allowed for a causal witness, but not for a
82 strict complete-closure trace. The two modes have the same logical meaning. -/
83 def replay (p : Problem) (strict : Bool) : List Nat → List Nat → Option (List Nat)
84   | known, [] => some known
85   | known, j :: js =>
86     match lookup p.rules j with
87     | none => none
88     | some r =>
89       if enabled r known && (!strict || !(known.contains r.conclusion)) then
90         replay p strict (r.conclusion :: known) js
91       else none
92 
93 theorem initial_sound (p : Problem) :
94     ∀ v, v ∈ p.initial → v ∈ p.exactClosure := by
95   intro v hv
96   rcases List.mem_append.mp hv with hv | hv
97   · exact Field.Derives.leaf (Or.inl hv)
98   · exact p.field.closure_contains_seed p.seeds hv
99 
100 theorem rule_sound (p : Problem) {known : List Nat} {j : Nat} {r : Rule}
101     (hj : lookup p.rules j = some r) (he : enabled r known = true)
102     (hk : ∀ v, v ∈ known → v ∈ p.exactClosure) :
103     r.conclusion ∈ p.exactClosure := by
104   have hp := (enabled_iff r known).mp he
105   have hc : (p.field.seeded p.seeds).Derives (p.field.conclusion j) := by
106     apply Field.Derives.step j
107     · simp [Problem.field, Field.seeded, hj]
108     · intro v hv
109       apply hk v
110       apply hp v
111       simpa [Problem.field, Field.seeded, hj] using hv
112   simpa [Problem.exactClosure, Field.closure, Problem.field, hj] using hc
113 
114 /-- No execution step can insert a node without a declared derivation. -/
115 theorem replay_sound (p : Problem) (strict : Bool) {known trace out : List Nat}
116     (hk : ∀ v, v ∈ known → v ∈ p.exactClosure)
117     (h : replay p strict known trace = some out) :
118     ∀ v, v ∈ out → v ∈ p.exactClosure := by
119   induction trace generalizing known with
120   | nil =>
121     have he : known = out := Option.some.inj h
122     simpa [← he] using hk
123   | cons j js ih =>
124     cases hj : lookup p.rules j with
125     | none => simp [replay, hj] at h
126     | some r =>
127       simp only [replay, hj] at h
128       split at h
129       next ha =>
130         have he := (Bool.and_eq_true_iff.mp ha).1
131         apply ih ?_ h
132         intro v hv
133         rcases List.mem_cons.mp hv with hv | hv
134         · subst v
135           exact rule_sound p hj he hk
136         · exact hk v hv
137       next => simp at h
138 
139 /-- Replay preserves every initially known node. -/
140 theorem replay_extensive (p : Problem) (strict : Bool) {known trace out : List Nat}
141     (h : replay p strict known trace = some out) :
142     ∀ v, v ∈ known → v ∈ out := by
143   induction trace generalizing known with
144   | nil =>
145     have he : known = out := Option.some.inj h
146     exact fun v hv => he ▸ hv
147   | cons j js ih =>
148     cases hj : lookup p.rules j with
149     | none => simp [replay, hj] at h
150     | some r =>
151       simp only [replay, hj] at h
152       split at h
153       next => exact fun v hv => ih h v (List.mem_cons_of_mem _ hv)
154       next => simp at h
155 
156 /-- Execution composes by concatenation, including explicit failure propagation. -/
157 theorem replay_append (p : Problem) (strict : Bool) (known left right : List Nat) :
158     replay p strict known (left ++ right) =
159       (replay p strict known left).bind (fun middle => replay p strict middle right) := by
160   induction left generalizing known with
161   | nil => rfl
162   | cons j js ih =>
163     cases hj : lookup p.rules j with
164     | none => simp [replay, hj]
165     | some r =>
166       simp only [List.cons_append, replay, hj]
167       split
168       · exact ih _
169       · rfl
170 
171 /-- A list-coded model predicate, with all rule rows checked. -/
172 def closed (p : Problem) (known : List Nat) : Bool :=
173   p.leaves.all (fun v => known.contains v) &&
174     p.rules.all (fun r => !enabled r known || known.contains r.conclusion)
175 
176 theorem closed_iff_model (p : Problem) (known : List Nat) :
177     closed p known = true ↔ p.field.Model (fun v => v ∈ known) := by
178   constructor
179   · intro h
180     have hl := (Bool.and_eq_true_iff.mp h).1
181     have hr := (Bool.and_eq_true_iff.mp h).2
182     constructor
183     · intro v hv
184       exact (List.all_eq_true.mp hl v hv) |> (by simpa using ·)
185     · intro j hj hp
186       cases he : lookup p.rules j with
187       | none => simp [Problem.field, he] at hj
188       | some r =>
189         have hm := lookup_mem he
190         have hh := List.all_eq_true.mp hr r hm
191         have en : enabled r known = true := by
192           apply (enabled_iff r known).mpr
193           intro v hv
194           apply hp v
195           simpa [Problem.field, he] using hv
196         have hc : r.conclusion ∈ known := by simpa [en] using hh
197         simpa [Problem.field, he] using hc
198   · rintro ⟨hl, hr⟩
199     apply Bool.and_eq_true_iff.mpr
200     constructor
201     · apply List.all_eq_true.mpr
202       intro v hv
203       simpa using hl v hv
204     · apply List.all_eq_true.mpr
205       intro r hm
206       by_cases he : enabled r known = true
207       · obtain ⟨j, hj⟩ := mem_lookup hm
208         have hc : p.field.certified j := by simp [Problem.field, hj]
209         have hp : ∀ v, v ∈ p.field.premises j → v ∈ known := by
210           intro v hv
211           apply (enabled_iff r known).mp he v
212           simpa [Problem.field, hj] using hv
213         have hh := hr j hc hp
214         simpa [Problem.field, hj, he] using hh
215       · simp [he]
216 
217 def sameMembers (a b : List Nat) : Bool :=
218   a.all (fun v => b.contains v) && b.all (fun v => a.contains v)
219 
220 theorem sameMembers_iff (a b : List Nat) :
221     sameMembers a b = true ↔ ∀ v, v ∈ a ↔ v ∈ b := by
222   simp only [sameMembers, Bool.and_eq_true, List.all_eq_true, List.contains_iff_mem]
223   constructor
224   · rintro ⟨hab, hba⟩ v
225     exact ⟨hab v, hba v⟩
226   · intro h
227     exact ⟨fun v => (h v).mp, fun v => (h v).mpr⟩
228 
229 /-- Complete replay plus a model check establishes equality with the least closure. -/
230 def checkClosure (p : Problem) (trace known : List Nat) : Bool :=
231   match replay p true p.initial trace with
232   | none => false
233   | some out => sameMembers out known && closed p known
234 
235 theorem checkClosure_exact (p : Problem) (trace known : List Nat)
236     (h : checkClosure p trace known = true) :
237     ∀ v, v ∈ known ↔ v ∈ p.exactClosure := by
238   cases he : replay p true p.initial trace with
239   | none => simp [checkClosure, he] at h
240   | some out =>
241     have hh : sameMembers out known = true ∧ closed p known = true := by
242       simpa [checkClosure, he] using h
243     have hm := (sameMembers_iff out known).mp hh.1
244     have hs := replay_sound p true (initial_sound p) he
245     have hi := replay_extensive p true he
246     have hmodel := (closed_iff_model p known).mp hh.2
247     have seed : ∀ v, v ∈ p.seeds → v ∈ known := by
248       intro v hv
249       exact (hm v).mp (hi v (List.mem_append_right _ hv))
250     exact fun v => ⟨fun hv => hs v ((hm v).mpr hv),
251       p.field.closure_le_model p.seeds hmodel seed v⟩
252 
253 def checkWitness (p : Problem) (w : Witness) : Bool :=
254   match replay p false p.initial w.trace with
255   | none => false
256   | some out => out.contains w.target && p.negative.contains w.target
257 
258 theorem checkWitness_sound (p : Problem) (w : Witness)
259     (h : checkWitness p w = true) :
260     w.target ∈ p.forbidden ∧ w.target ∈ p.exactClosure := by
261   cases he : replay p false p.initial w.trace with
262   | none => simp [checkWitness, he] at h
263   | some out =>
264     have hh : w.target ∈ out ∧ w.target ∈ p.negative := by
265       simpa [checkWitness, he] using h
266     exact ⟨hh.2, replay_sound p false (initial_sound p) he _ hh.1⟩
267 
268 theorem checkWitness_refutes (p : Problem) (w : Witness)
269     (h : checkWitness p w = true) :
270     ¬ ∃ x, p.field.Extends p.seeds p.forbidden x := by
271   apply (p.field.infeasible_iff_forbidden_derivation p.seeds p.forbidden).mpr
272   exact ⟨w.target, checkWitness_sound p w h⟩
273 
274 /-- Complete positive and negative result verification. Both require the full
275 least-closure certificate; a bare negative witness has its own checker. -/
276 def checkCertificate (p : Problem) (c : Certificate) : Bool :=
277   checkClosure p c.trace c.closure &&
278     if c.feasible then
279       c.obstruction.isNone && !(c.closure.any (fun v => p.negative.contains v))
280     else
281       match c.obstruction with
282       | none => false
283       | some w => checkWitness p w
284 
285 theorem certificate_closure (p : Problem) (c : Certificate)
286     (h : checkCertificate p c = true) :
287     ∀ v, v ∈ c.closure ↔ v ∈ p.exactClosure :=
288   checkClosure_exact p c.trace c.closure (Bool.and_eq_true_iff.mp h).1
289 
290 theorem certificate_positive (p : Problem) (c : Certificate)
291     (h : checkCertificate p c = true) (hf : c.feasible = true) :
292     p.field.Extends p.seeds p.forbidden (fun v => v ∈ c.closure) := by
293   have he := certificate_closure p c h
294   have branch := (Bool.and_eq_true_iff.mp h).2
295   have hn : ∀ v, v ∈ c.closure → v ∉ p.negative := by
296     have hh : c.obstruction = none ∧ (∀ v, v ∈ c.closure → v ∉ p.negative) := by
297       simpa [hf] using branch
298     exact hh.2
299   refine ⟨?_, ?_, ?_⟩
300   · constructor
301     · intro v hv
302       apply (he v).mpr
303       exact Field.Derives.leaf (Or.inl hv)
304     · intro j hj hp
305       apply (he _).mpr
306       exact Field.Derives.step j hj (fun v hv => (he v).mp (hp v hv))
307   · exact fun v hv => (he v).mpr (p.field.closure_contains_seed p.seeds hv)
308   · exact fun v hv hc => hn v hc hv
309 
310 theorem certificate_negative (p : Problem) (c : Certificate)
311     (h : checkCertificate p c = true) (hf : c.feasible = false) :
312     ¬ ∃ x, p.field.Extends p.seeds p.forbidden x := by
313   have branch := (Bool.and_eq_true_iff.mp h).2
314   cases hw : c.obstruction with
315   | none => simp [hf, hw] at branch
316   | some w =>
317     apply checkWitness_refutes p w
318     simpa [hf, hw] using branch
319 
320 theorem certificate_decides_feasibility (p : Problem) (c : Certificate)
321     (h : checkCertificate p c = true) :
322     (c.feasible = true ↔ ∃ x, p.field.Extends p.seeds p.forbidden x) := by
323   constructor
324   · exact fun hf => ⟨_, certificate_positive p c h hf⟩
325   · intro hx
326     cases hf : c.feasible with
327     | true => rfl
328     | false => exact False.elim (certificate_negative p c h hf hx)
329 
330 /-- Semantic validity remains conditional on an interpretation and true seeds. -/
331 theorem accepted_meaning (p : Problem) (c : Certificate)
332     (h : checkCertificate p c = true) (meaning : Nat → Prop)
333     (hm : p.field.Model meaning) (hs : ∀ v, v ∈ p.seeds → meaning v)
334     {v : Nat} (hv : v ∈ c.closure) : meaning v :=
335   p.field.closure_le_model p.seeds hm hs v ((certificate_closure p c h v).mp hv)
336 
337 end ProofPath.Trace

Back to source controls