ComplexityPair

formal source

   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