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

Imports

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

General CLIQUE verifier: polynomial runtime of the target bound

              noncomputable sectionopen Computability StateTransitionnamespace CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBoundopen PolyBuilderopen _root_.TuringUsed `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

private theorem targetSteps_le (count : Nat) (input : List CliqueSym) :
    targetSteps count input ≤ 2 * input.length + count + 4 := by
  induction input generalizing count with
  | nil => simp [targetSteps]
  | cons symbol input ih =>
      have hsame := ih count
      cases symbol <;> try simp [targetSteps] Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`<;> try omega
      case tick =>
        cases count with
        | zero => simp [targetSteps]; omega
        | succ count =>
            have h := ih count
            simp [targetSteps]
            omegaUsed `tac1 <;> tac2` where `(tac1; tac2)` would suffice

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

private theorem vertexSteps_le (count : Nat) (input : List CliqueSym) :
    vertexSteps count input ≤ 3 * input.length + count + 4 := by
  induction input generalizing count with
  | nil => simp [vertexSteps]
  | cons symbol input ih =>
      have hsame := ih count
      cases symbol <;> try simp [vertexSteps] Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`<;> try omega
      case tick =>
        have h := ih (count + 1)
        simp [This simp argument is unused:
  vertexSteps

Hint: Omit it from the simp argument list.
  simp ̵[̵v̵e̵r̵t̵e̵x̵S̵t̵e̵p̵s̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`vertexSteps]
        omega
      case fieldSep =>
        have h := targetSteps_le count input
        simp [This simp argument is unused:
  vertexSteps

Hint: Omit it from the simp argument list.
  simp ̵[̵v̵e̵r̵t̵e̵x̵S̵t̵e̵p̵s̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`vertexSteps]
        omegaprivate theorem instanceSteps_le (input : List CliqueSym) :
    instanceSteps input ≤ 3 * input.length + 4 := by
  cases input with
  | nil => simp [instanceSteps]
  | cons symbol input =>
      have h := vertexSteps_le 0 input
      simp [instanceSteps]
      omega

Total step budget of the exact target-bound run.

def targetBoundSteps (certificate input : List CliqueSym) : Nat :=
  certificate.length + 1 + instanceSteps input

The controller is linear in the separator-based pair encoding.

theorem targetBoundSteps_le (certificate input : List CliqueSym) :
    targetBoundSteps certificate input ≤
      3 * (pairEncoding certificate input).length + 4 := by
  have h := instanceSteps_le input
  simp only [targetBoundSteps, pairEncoding, List.length_append,
    List.length_map, List.length_cons, List.length_nil]
  omega

The compiled controller emits its singleton Boolean result inside the displayed linear budget.

Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
def targetBound_outputs_in_time (certificate input : List CliqueSym) :
    TM2OutputsInTime (compile program) (pairEncoding certificate input)
      (some (boolEncoding (targetBoundPass certificate input)))
      (3 * (pairEncoding certificate input).length + 4) := by
  have builderRun := targetBound_run certificate input
  have compiledRun := compile_evalsToInTime program builderRun
  change EvalsToInTime (compile program).step
      (initList (compile program) (pairEncoding certificate input))
      (some (haltList (compile program)
        [targetBoundPass certificate input]))
      (3 * (pairEncoding certificate input).length + 4)
  refine ⟨⟨compiledRun.steps, ?_⟩, compiledRun.steps_le_m.trans
    (targetBoundSteps_le certificate input)⟩
  convert compiledRun.evals_in_steps using 1 <;>
    simp only [encodeCfg_initialCfg, encodeCfg_haltCfg] Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`<;> rfl

Polynomial-time computability of the concrete target-bound component on raw certificate/instance pairs.

noncomputable def targetBoundPassComputableInPolyTime :
    TM2ComputableInPolyTime
      (fun pr : List CliqueSym × List CliqueSym => pairEncoding pr.1 pr.2)
      boolEncoding (fun pr => targetBoundPass pr.1 pr.2) where
  tm := compile program
  inputAlphabet := Equiv.refl _
  outputAlphabet := Equiv.refl _
  time := 3 * Polynomial.X + 4
  outputsFun := fun pr => by
    rcases pr with ⟨certificate, input⟩
    have run := targetBound_outputs_in_time certificate input
    convert run using 1 <;>
      simp [Polynomial.eval_add, Polynomial.eval_mul, Polynomial.eval_X,
        Polynomial.eval_ofNat]
    all_goals
      change List.map id _ = _
      exact List.map_id _

end CLRS.Chapter34.Turing.GeneralCliqueVerifier.TargetBound