TraceCompleteness.lean

1 import ProofPath.Trace
2 
3 /-!
4 Causal witnesses can be reused under stronger known information. Because each
5 rule has finitely many premises, every inductive derivation has a finite replay
6 trace. This is completeness of witness certificates, not verification of the
7 Python search procedure or a bound on shortest proofs.
8 -/
9 namespace ProofPath.Trace
10 
11 theorem enabled_mono (r : Rule) {a b : List Nat}
12     (hab : ∀ v, v ∈ a → v ∈ b) (h : enabled r a = true) :
13     enabled r b = true :=
14   (enabled_iff r b).mpr (fun v hv => hab v ((enabled_iff r a).mp h v hv))
15 
16 /-- Nonstrict traces remain valid if more nodes are already known. -/
17 theorem replay_weaken (p : Problem) {a b trace out : List Nat}
18     (hab : ∀ v, v ∈ a → v ∈ b) (h : replay p false a trace = some out) :
19     ∃ result, replay p false b trace = some result ∧
20       ∀ v, v ∈ out → v ∈ result := by
21   induction trace generalizing a b with
22   | nil =>
23     have he : a = out := Option.some.inj h
24     exact ⟨b, rfl, fun v hv => hab v (he.symm ▸ hv)⟩
25   | cons j js ih =>
26     cases hj : lookup p.rules j with
27     | none => simp [replay, hj] at h
28     | some r =>
29       simp only [replay, hj] at h
30       split at h
31       next ha =>
32         have he : enabled r a = true := by simpa using ha
33         have he' := enabled_mono r hab he
34         have hab' : ∀ v, v ∈ r.conclusion :: a → v ∈ r.conclusion :: b := by
35           intro v hv
36           rcases List.mem_cons.mp hv with hv | hv
37           · exact List.mem_cons.mpr (Or.inl hv)
38           · exact List.mem_cons.mpr (Or.inr (hab v hv))
39         obtain ⟨result, hr, hc⟩ := ih hab' h
40         exact ⟨result, by simp [replay, hj, he', hr], hc⟩
41       next => simp at h
42 
43 /-- A strict execution is also a valid causal-witness execution. -/
44 theorem strict_replay_is_causal (p : Problem) {known trace out : List Nat}
45     (h : replay p true known trace = some out) :
46     replay p false known trace = some out := by
47   induction trace generalizing known with
48   | nil => exact h
49   | cons j js ih =>
50     cases hj : lookup p.rules j with
51     | none => simp [replay, hj] at h
52     | some r =>
53       simp only [replay, hj] at h
54       split at h
55       next ha =>
56         have he := (Bool.and_eq_true_iff.mp ha).1
57         simpa [replay, hj, he] using ih h
58       next => simp at h
59 
60 /-- Concatenate finitely many existing causal traces, retaining all targets. -/
61 theorem gather_traces (p : Problem) (targets : List Nat)
62     (hw : ∀ v, v ∈ targets → ∃ tr out,
63       replay p false p.initial tr = some out ∧ v ∈ out)
64     {known : List Nat} (hk : ∀ v, v ∈ p.initial → v ∈ known) :
65     ∃ tr out, replay p false known tr = some out ∧
66       ∀ v, v ∈ targets → v ∈ out := by
67   induction targets generalizing known with
68   | nil => exact ⟨[], known, rfl, by simp⟩
69   | cons v vs ih =>
70     obtain ⟨first, out, hf, hv⟩ := hw v (by simp)
71     obtain ⟨middle, hm, hsub⟩ := replay_weaken p hk hf
72     have hnext : ∀ w, w ∈ p.initial → w ∈ middle := by
73       intro w hw
74       exact replay_extensive p false hm w (hk w hw)
75     obtain ⟨rest, last, hr, hvs⟩ := ih
76       (fun w hwv => hw w (List.mem_cons_of_mem _ hwv)) hnext
77     refine ⟨first ++ rest, last, ?_, ?_⟩
78     · simp [replay_append, hm, hr]
79     · intro w hmem
80       rcases List.mem_cons.mp hmem with hmem | hmem
81       · subst w
82         exact replay_extensive p false hr v (hsub v hv)
83       · exact hvs w hmem
84 
85 /-- Finite rule premises make every inductive derivation serially replayable. -/
86 theorem derivation_has_trace (p : Problem) {v : Nat} (hv : v ∈ p.exactClosure) :
87     ∃ tr out, replay p false p.initial tr = some out ∧ v ∈ out := by
88   induction hv with
89   | leaf hv =>
90     refine ⟨[], p.initial, rfl, ?_⟩
91     rcases hv with hv | hv
92     · exact List.mem_append_left _ hv
93     · exact List.mem_append_right _ hv
94   | step j hj _ ih =>
95     cases he : lookup p.rules j with
96     | none => simp [Problem.field, Field.seeded, he] at hj
97     | some r =>
98       have targets : ∀ w, w ∈ r.premises → ∃ tr out,
99           replay p false p.initial tr = some out ∧ w ∈ out := by
100         intro w hw
101         apply ih w
102         simpa [Problem.field, Field.seeded, he] using hw
103       obtain ⟨tr, out, ht, hp⟩ := gather_traces p r.premises targets (fun _ h => h)
104       have hen : enabled r out = true := (enabled_iff r out).mpr hp
105       refine ⟨tr ++ [j], r.conclusion :: out, ?_, ?_⟩
106       · simp [replay_append, ht, replay, he, hen]
107       · simp [Problem.field, Field.seeded, he]
108 
109 /-- An obstruction always has some finite causal witness in this declared field. -/
110 theorem witness_complete (p : Problem) {v : Nat}
111     (hn : v ∈ p.forbidden) (hv : v ∈ p.exactClosure) :
112     ∃ w, w.target = v ∧ checkWitness p w = true := by
113   obtain ⟨tr, out, ht, hvout⟩ := derivation_has_trace p hv
114   exact ⟨⟨v, tr⟩, rfl, by simpa [checkWitness, ht, hvout, Problem.forbidden] using hn⟩
115 
116 theorem witness_exists_iff_infeasible (p : Problem) :
117     (∃ w, checkWitness p w = true) ↔
118       ¬ ∃ x, p.field.Extends p.seeds p.forbidden x := by
119   constructor
120   · rintro ⟨w, hw⟩
121     exact checkWitness_refutes p w hw
122   · intro h
123     obtain ⟨v, hn, hv⟩ :=
124       (p.field.infeasible_iff_forbidden_derivation p.seeds p.forbidden).mp h
125     obtain ⟨w, _, hw⟩ := witness_complete p hn hv
126     exact ⟨w, hw⟩
127 
128 end ProofPath.Trace

Back to source controls