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 — Specification

Imports

import CLRSLean.Chapter_34.Section_34_4_NP_Completeness_Proofs.GeneralClique.VerifierMachine.TargetBound.Basic

General CLIQUE verifier: raw target-bound specification

The controller's recursive Boolean semantics agrees with an explicit scan of the first two unary fields on every raw input, not only on encoder output.

              namespace CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBound

private theorem targetResult_eq_scan (count : Nat) (input : List CliqueSym) :
    targetResult count input =
      match ticksThroughSeparator input with
      | none => false
      | some (targetSize, _) => decide (targetSize ≤ count) := by
  induction input generalizing count with
  | nil => simp [targetResult, ticksThroughSeparator]
  | cons symbol input ih =>
      cases symbol <;>
        try simp [targetResult, ticksThroughSeparator, ih]
      case tick =>
        cases count with
        | zero =>
            cases hscan : ticksThroughSeparator input with
            | none => simp [targetResult, This simp argument is unused:
  ticksThroughSeparator

Hint: Omit it from the simp argument list.
  simp [targetResult, t̵i̵c̵k̵s̵T̵h̵r̵o̵u̵g̵h̵S̵e̵p̵a̵r̵a̵t̵o̵r̵,̵ ̵hscan]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`ticksThroughSeparator, This simp argument is unused:
  hscan

Hint: Omit it from the simp argument list.
  simp [targetResult, ticksThroughSeparator,̵ ̵h̵s̵c̵a̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hscan]
            | some result =>
                rcases result with ⟨targetSize, rest⟩
                simp [targetResult, This simp argument is unused:
  ticksThroughSeparator

Hint: Omit it from the simp argument list.
  simp [targetResult, t̵i̵c̵k̵s̵T̵h̵r̵o̵u̵g̵h̵S̵e̵p̵a̵r̵a̵t̵o̵r̵,̵ ̵hscan]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`ticksThroughSeparator, This simp argument is unused:
  hscan

Hint: Omit it from the simp argument list.
  simp [targetResult, ticksThroughSeparator,̵ ̵h̵s̵c̵a̵n̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hscan]
        | succ count =>
            cases hscan : ticksThroughSeparator input with
            | none =>
                simpa [targetResult, ticksThroughSeparator, hscan] using
                  ih count
            | some result =>
                rcases result with ⟨targetSize, rest⟩
                simpa [targetResult, ticksThroughSeparator, hscan] using
                  ih counttry 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`

private theorem vertexResult_eq_scan (count : Nat) (input : List CliqueSym) :
    vertexResult count input =
      match ticksThroughSeparator input with
      | none => false
      | some (vertexTicks, targetField) =>
          targetResult (count + vertexTicks) targetField := by
  induction input generalizing count with
  | nil => simp [vertexResult, ticksThroughSeparator]
  | cons symbol input ih =>
      cases symbol <;>
        try simp [vertexResult, ticksThroughSeparator, ih]
      case tick =>
        cases hscan : ticksThroughSeparator input with
        | none =>
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [vertexResult, ticksThroughSeparator, hscan] using
              ih (count + 1)
        | some result =>
            rcases result with ⟨vertexTicks, targetField⟩
            try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`simpa [vertexResult, ticksThroughSeparator, hscan,
              Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
              ih (count + 1)

Exact raw-string characterization of the Boolean computed by the fixed target-bound machine.


theorem targetBoundPass_eq_scan (certificate input : List CliqueSym) :
    targetBoundPass certificate input =
      match input with
      | [] => false
      | _ :: fields =>
          match ticksThroughSeparator fields with
          | none => false
          | some (vertexCount, targetField) =>
              match ticksThroughSeparator targetField with
              | none => false
              | some (targetSize, _) => decide (targetSize ≤ vertexCount) := by
  cases input with
  | nil => rfl
  | cons marker fields =>
      simp only [targetBoundPass]
      rw [vertexResult_eq_scan]
      cases hvertices : ticksThroughSeparator fields with
      | none => simp [This simp argument is unused:
  hvertices

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵v̵e̵r̵t̵i̵c̵e̵s̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hvertices]
      | some result =>
          rcases result with ⟨vertexCount, targetField⟩
          simp only [This simp argument is unused:
  hvertices

Hint: Omit it from the simp argument list.
  simp only [h̵v̵e̵r̵t̵i̵c̵e̵s̵,̵ ̵Nat.zero_add]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`hvertices, Nat.zero_add]
          rw [targetResult_eq_scan]

end CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBound