CLRS-Lean
Chapter 34. NP-Completeness
34.4. NP-Completeness Proofs
34.4. General CLIQUE — GeneralClique
34.4. General CLIQUE — VerifierMachine
34.4. General CLIQUE — TargetBound facade
34.4. General CLIQUE — Canonical

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.VerifierMachine.TargetBound.Runtime
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.VerifierMachine.TargetBound.Specification
import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.Encoding.RoundTrip

General CLIQUE verifier: canonical target-bound semantics

              namespace CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBoundprivate theorem targetResult_prepend (targetSize : Nat)
    (rest : List CliqueSym) (vertexCount : Nat) :
    targetResult vertexCount
        (prependCliqueTicks targetSize (.fieldSep :: rest)) =
      decide (targetSize ≤ vertexCount) := by
  induction targetSize generalizing vertexCount with
  | zero => simp [prependCliqueTicks, targetResult]
  | succ targetSize ih =>
      cases vertexCount with
      | zero => simp [prependCliqueTicks, targetResult]
      | succ vertexCount =>
          simp [prependCliqueTicks, targetResult, ih]

private theorem vertexResult_prepend (vertexTicks count : Nat)
    (rest : List CliqueSym) :
    vertexResult count
        (prependCliqueTicks vertexTicks (.fieldSep :: rest)) =
      targetResult (count + vertexTicks) rest := by
  induction vertexTicks generalizing count with
  | zero => simp [prependCliqueTicks, vertexResult]
  | succ vertexTicks ih =>
      simp [prependCliqueTicks, vertexResult, ih, This simp argument is unused:
  Nat.add_assoc

Hint: Omit it from the simp argument list.
  simp [prependCliqueTicks, vertexResult, ih, N̵a̵t̵.̵a̵d̵d̵_̵a̵s̵s̵o̵c̵,̵Nat.add_comm, Nat.add_left_comm]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`Nat.add_assoc,
        Nat.add_comm, Nat.add_left_comm]

On a canonical graph serialization, the concrete pass is exactly the typed target-size bound, independently of the certificate.


theorem targetBoundPass_encode_iff (certificate : List CliqueSym)
    (I : CliqueInstance) :
    targetBoundPass certificate (encodeCliqueInstance I) = true ↔
      I.targetSize ≤ I.vertexCount := by
  simp only [targetBoundPass, encodeCliqueInstance]
  rw [vertexResult_prepend]
  simp only [Nat.zero_add]
  rw [targetResult_prepend]
  simp

end CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBound