IndisputableMonolith.Complexity.VertexCover

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Complexity
   5
   6/-- Complexity pair (functions of input size). -/
   7structure ComplexityPair where
   8  Tc : ℕ → ℕ
   9  Tr : ℕ → ℕ
  10
  11namespace VertexCover
  12
  13/-- Vertex Cover instance over `Nat` vertices. -/
  14structure Instance where
  15  vertices : List Nat
  16  edges    : List (Nat × Nat)
  17  k        : Nat
  18  deriving Repr
  19
  20/-- A set `S` covers an edge `(u,v)` if it contains `u` or `v`. -/
  21def InCover (S : List Nat) (v : Nat) : Prop := v ∈ S
  22
  23def EdgeCovered (S : List Nat) (e : Nat × Nat) : Prop :=
  24  InCover S e.fst ∨ InCover S e.snd
  25
  26/-- `S` covers all edges of instance `I`. -/
  27def Covers (S : List Nat) (I : Instance) : Prop :=
  28  ∀ e, e ∈ I.edges → EdgeCovered S e
  29
  30/-- There exists a vertex cover of size ≤ k. -/
  31def HasCover (I : Instance) : Prop :=
  32  ∃ S : List Nat, S.length ≤ I.k ∧ Covers S I
  33
  34/-- A trivial example with no edges is always covered by the empty set. -/
  35@[simp] def trivialInstance : Instance := { vertices := [1], edges := [], k := 0 }
  36
  37lemma trivial_hasCover : HasCover trivialInstance := by
  38  refine ⟨[], by decide, ?_⟩
  39  intro e he
  40  simpa using he
  41
  42@[simp] lemma InCover_cons {x : Nat} {xs : List Nat} : InCover (x :: xs) x := by
  43  simp [InCover]
  44
  45@[simp] lemma InCover_of_mem {S : List Nat} {v : Nat} (h : v ∈ S) : InCover S v := by
  46  simpa [InCover] using h
  47
  48lemma EdgeCovered_comm (S : List Nat) (u v : Nat) :
  49  EdgeCovered S (u, v) ↔ EdgeCovered S (v, u) := by
  50  simp [EdgeCovered, Or.comm]
  51
  52lemma Covers_nil_edges (S : List Nat) (I : Instance) (h_edges : I.edges = []) : Covers S I := by
  53  intro e he
  54  simpa [Covers, h_edges] using he
  55
  56lemma hasCover_of_nil_edges (I : Instance) (h_edges : I.edges = []) : HasCover I := by
  57  refine ⟨[], by simp, ?_⟩
  58  intro e he
  59  simpa [Covers, h_edges] using he
  60
  61end VertexCover
  62
  63end Complexity
  64
  65end IndisputableMonolith
  66