SeedCertificates.lean

1 import PaperX.SeedConsequences
2 
3 /-!
4 Finite reachability certificates. A bounded walk search is accepted as complete
5 only after its closure under the original edges is proved. There is no claim that
6 an arbitrary cutoff is sufficient, and no external solver output is trusted.
7 -/
8 set_option autoImplicit false
9 namespace PaperX.SeedCertificates
10 
11 open PaperX.DirectedSeeds
12 universe u v
13 variable {V : Type u} [Fintype V] [DecidableEq V]
14 variable (E : V → V → Prop) [DecidableRel E]
15 
16 def neighbors (a : V) : Finset V := Finset.univ.filter (E a)
17 
18 def reachableWithin : ℕ → V → Finset V
19   | 0, a => {a}
20   | n+1, a => reachableWithin n a ∪ (reachableWithin n a).biUnion (neighbors E)
21 
22 theorem reachableWithin_self (n : ℕ) (a : V) : a ∈ reachableWithin E n a := by
23   induction n with
24   | zero => simp [reachableWithin]
25   | succ n ih => exact Finset.mem_union_left _ ih
26 
27 theorem reachableWithin_sound {n : ℕ} {a b : V} (h : b ∈ reachableWithin E n a) :
28     Reach E a b := by
29   induction n generalizing b with
30   | zero =>
31     have heq : b = a := Finset.mem_singleton.mp h
32     subst b
33     exact .refl
34   | succ n ih =>
35     rcases Finset.mem_union.mp h with h | h
36     · exact ih h
37     · obtain ⟨c, hc, hcb⟩ := Finset.mem_biUnion.mp h
38       exact (ih hc).tail (Finset.mem_filter.mp hcb).2
39 
40 def ClosedAt (n : ℕ) : Prop :=
41   ∀ a b, b ∈ reachableWithin E n a → ∀ c, E b c → c ∈ reachableWithin E n a
42 
43 instance closedAtDecidable (n : ℕ) : Decidable (ClosedAt E n) :=
44   inferInstanceAs (Decidable (∀ a b, b ∈ reachableWithin E n a →
45     ∀ c, E b c → c ∈ reachableWithin E n a))
46 
47 theorem reach_iff_certificate (n : ℕ) (hclosed : ClosedAt E n) (a b : V) :
48     Reach E a b ↔ b ∈ reachableWithin E n a := by
49   constructor
50   · intro h
51     induction h with
52     | refl => exact reachableWithin_self E n a
53     | @tail b c _ hbc ih => exact hclosed a b ih c hbc
54   · exact reachableWithin_sound E
55 
56 def certifiedCover (n : ℕ) (S : Finset V) : Prop :=
57   ∀ v, ∃ s ∈ S, v ∈ reachableWithin E n s
58 
59 instance certifiedCoverDecidable (n : ℕ) (S : Finset V) :
60     Decidable (certifiedCover E n S) :=
61   inferInstanceAs (Decidable (∀ v, ∃ s ∈ S, v ∈ reachableWithin E n s))
62 
63 theorem certifiedCover_iff (n : ℕ) (hclosed : ClosedAt E n) (S : Finset V) :
64     certifiedCover E n S ↔ Covers E S := by
65   simp only [certifiedCover, Covers, reach_iff_certificate E n hclosed]
66 
67 /-- A certified complete component labeling is equivalent to the actual SCC quotient. -/
68 noncomputable def componentEquivOfLabels {K : Type v}
69     (label : V → K) (rep : K → V) (sectionLaw : ∀ k, label (rep k) = k)
70     (labelLaw : ∀ a b, label a = label b ↔ Reach E a b ∧ Reach E b a) :
71     Component E ≃ K where
72   toFun := Quotient.lift label (fun a b hab => (labelLaw a b).2 hab)
73   invFun := fun k => component E (rep k)
74   left_inv := by
75     intro c
76     induction c using Quotient.inductionOn with
77     | h a =>
78       apply (component_eq_iff E _ _).2
79       exact (labelLaw _ _).1 (sectionLaw (label a))
80   right_inv := sectionLaw
81 
82 end PaperX.SeedCertificates

Back to source controls