EdgeCovered

formal source

  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