RevisionAdmission.lean

1 import MachineTheory.RevisionReplay
2 
3 /-! # Admission and the initial certificate boundary
4 
5 A positive local verdict without established parents does not constitute an old proof.
6 The constructor below derives old establishment in topological order. The finite gate
7 also checks every unchanged external premise before copying old certificates.
8 -/
9 namespace Komorebi.MachineTheory.Dependency
10 open Finset
11 variable {V I : Type*} [Fintype V] [DecidableEq V]
12 variable {A : I → Type*} [∀ i, DecidableEq (A i)] {W : V → Type*}
13 variable {G : Graph V I} (S : System G A W)
14 
15 omit [Fintype V] [DecidableEq V] [∀ i, DecidableEq (A i)] in
16 /-- Establishing an initial snapshot requires sound local rules and grounded parents. -/
17 theorem System.established_from_checks (rank : V → ℕ) (ordered : G.Ranked rank)
18     (a : ∀ i, A i) (old : ∀ v, W v)
19     (hc : ∀ v, S.check v (G.view a v) (old v) = true)
20     (he : ∀ v, S.external a v) : ∀ v, S.Established a v (old v) := by
21   have go : ∀ n v, rank v=n → S.claim a v := by
22     intro n
23     induction n using Nat.strong_induction_on with
24     | h n ih =>
25       intro v hn
26       apply S.sound a v (old v) (hc v) (he v)
27       intro u hu
28       exact ih (rank u) (by rw [← hn]; exact ordered v u hu) u rfl
29   intro v
30   exact ⟨hc v,he v,go (rank v) v rfl⟩
31 
32 def replayGuard (G : Graph V I) (a b : ∀ i, A i) (external : V → Bool) (rank : V → ℕ) : Bool :=
33   decide ((∀ v u, u ∈ G.parents v → rank u < rank v) ∧
34     (∀ v, v ∉ G.stale a b → external v = true))
35 
36 theorem replayGuard_iff (G : Graph V I) (a b : ∀ i, A i) (external : V → Bool) (rank : V → ℕ) :
37     replayGuard G a b external rank = true ↔
38       G.Ranked rank ∧ (∀ v, v ∉ G.stale a b → external v = true) := by
39   simp [replayGuard,Graph.Ranked]
40 
41 /-- An outer rejection is neither a false-claim verdict nor a completed proof search. -/
42 def System.checkedFinish (a b : ∀ i, A i) (old : ∀ v, W v)
43     (fresh : ∀ v, Option (W v)) (external : V → Bool) (rank : V → ℕ) :
44     Option (∀ v, Verdict (W v)) :=
45   if replayGuard G a b external rank then some (S.finish a b old fresh external rank) else none
46 
47 /-- Every certificate returned by an admitted partial replay has its revised meaning. -/
48 theorem System.admitted_reuse_and_restoration (complete : S.Complete)
49     (a b : ∀ i, A i) (old : ∀ v, W v) (fresh : ∀ v, Option (W v))
50     (external : V → Bool) (rank : V → ℕ)
51     (hold : ∀ v, S.Established a v (old v))
52     (he : ∀ v, external v = true → S.external b v)
53     (result : ∀ v, Verdict (W v))
54     (accepted : S.checkedFinish a b old fresh external rank = some result) :
55     S.SoundState b result := by
56   unfold checkedFinish at accepted
57   split at accepted
58   next hg =>
59     have heq := Option.some.inj accepted
60     subst result
61     obtain ⟨hr,hclean⟩ := (replayGuard_iff G a b external rank).mp hg
62     exact S.finish_sound complete rank hr a b old fresh external hold
63       (fun v hv => he v (hclean v hv)) he
64   next => contradiction
65 
66 omit [∀ i, DecidableEq (A i)] in
67 /-- A missing parent yields no local certificate even when the local check could pass. -/
68 theorem System.blocked_parent (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
69     (external : V → Bool) (s : ∀ v, Verdict (W v)) (v u : V)
70     (hu : u ∈ G.parents v) (hm : (s u).ready = false) :
71     S.evaluate b fresh external s v = .blockedParents := by
72   have hn : ¬ ∀ z ∈ G.parents v, (s z).ready = true := by
73     intro h
74     have hh := h u hu
75     rw [hm] at hh
76     contradiction
77   exact ite_eq_right hn
78 
79 omit [∀ i, DecidableEq (A i)] in
80 /-- Failure to find a witness is recorded separately from rejection of a supplied witness. -/
81 theorem System.missing_evidence (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
82     (external : V → Bool) (s : ∀ v, Verdict (W v)) (v : V)
83     (hp : ∀ u ∈ G.parents v, (s u).ready = true) (he : external v=true)
84     (hf : fresh v=none) : S.evaluate b fresh external s v = .missing := by
85   unfold evaluate
86   rw [ite_eq_left hp,ite_eq_left he,hf]
87 
88 omit [∀ i, DecidableEq (A i)] in
89 /-- A rejected local witness supplies no theorem that its intended claim is false. -/
90 theorem System.rejected_evidence (b : ∀ i, A i) (fresh : ∀ v, Option (W v))
91     (external : V → Bool) (s : ∀ v, Verdict (W v)) (v : V) (w : W v)
92     (hp : ∀ u ∈ G.parents v, (s u).ready = true) (he : external v=true)
93     (hf : fresh v=some w) (hc : S.check v (G.view b v) w = false) :
94     S.evaluate b fresh external s v = .rejected := by
95   unfold evaluate
96   rw [ite_eq_left hp,ite_eq_left he,hf]
97   simp only [hc,Bool.false_eq_true,ite_false]
98 
99 end Komorebi.MachineTheory.Dependency

Back to source controls