Quelle  NP.thy

chapter ‹Time complexity\label{s:TC}›

theory NP
  imports Elementary Composing Symbol_Ops
begin

text ‹
  order to formulate the Cook-Levin theorem we need to formalize \SAT{} and
 \NP$-completeness. This chapter is devoted to the latter and hence introduces
  complexity class $\NP$ and the concept of polynomial-time many-one
 . Moreover, although not required for the Cook-Levin theorem, it
  the class $\mathcal{P}$ and contains a proof of $\mathcal{P}
 subseteq \NP$ (see Section~\ref{s:TC-subseteq}). The chapter concludes with
  easy results about $\mathcal{P}$, $\NP$ and reducibility in
 ~\ref{s:TC-more}.
 ›


section ‹The time complexity classes DTIME, $\mathcal{P}$, and $\NP$\label{s:TC-NP}›

text ‹
  and Barak~\cite[Definitions 1.12, 1.13]{ccama} define
 \mathrm{DTIME}(T(n))$ as the set of all languages that can be decided in time
 c \cdot T(n)$ for some $c > 0$ and $\mathcal{P} =
 bigcup_{c\geq1}\mathrm{DTIME}(n^c)$. However since $0^c = 0$ for $c\geq 1$,
  means that for a language $L$ to be in $\mathcal{P}$, the Turing machine
  $L$ must check the empty string in zero steps. For a Turing machine to
  in zero steps, it must start in the halting state, which limits its
 . Because of this technical issue we define $\mathrm{DTIME}(T(n))$ as
  set of all languages that can be decided with a running time in $O(T(n))$,
  seems a common enough alternative~\cite{lv-aikc,sipser2006,cz-dtime}.
 ›

text ‹
  are sets of strings, and deciding a language means computing its
  function.
 ›

type_synonym language = "string set"

definition characteristic :: "language ==> (string ==> string)" where
  "characteristic L ≡ (λx. [x ∈ L])"

definition DTIME :: "(nat ==> nat) ==> language set" where
  "DTIME T ≡ {L. ∃k G M T'.
    turing_machine k G M ∧
    big_oh T' T ∧
    computes_in_time k M (characteristic L) T'}"

definition complexity_class_P :: "language set" (‹P›) where
  "P ≡ ∪c∈{1..}. DTIME (λn. n ^ c)"

text ‹
  language $L$ is in $\NP$ if there is a polynomial $p$ and a polynomial-time
  machine, called the \emph{verifier}, such that for all strings
 x\in\bbOI^*$,
 [
 x\in L \longleftrightarrow
 \exists u\in\bbOI^{p(|x|)}: M(\langle x, u\rangle) = \bbbI.
 ]
  string $u$ does not seem to have a name in general, but in case the verifier
  $\bbbI$ on input $\langle x, u\rangle$ it is called a
 emph{certificate} for $x$~\cite[Definition~2.1]{ccama}.
 ›

definition complexity_class_NP :: "language set" (‹NP›) where
  "NP ≡ {L. ∃k G M p T fverify.
    turing_machine k G M ∧
    polynomial p ∧
    big_oh_poly T ∧
    computes_in_time k M fverify T ∧
    (∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀 ]))}"

text ‹
  definition of $\NP$ is the one place where we need an actual polynomial
 , namely $p$, rather than a function that is merely bounded by a
 . This raises the question as to the definition of a polynomial
 . Arora and Barak~\cite{ccama} do not seem to give a definition in the
  of $\NP$ but explicitly state that polynomial functions are mappings
 \nat \to \nat$. Presumably they also have the form $f(n) = \sum_{i=0}^d
 \cdot n^i$, as polynomials do. We have filled in the gap in this definition
  Section~\ref{s:tm-basic-bigoh} by letting the coefficients $a_i$ be natural
 .

  of whether this is the meaning intended by Arora and Barak, the
  is justified because with it the verifier-based definition of $\NP$ is
  to the original definition via nondeterministic Turing machines
 NTMs). In the usual equivalence proof (for example, Arora and
 ~\cite[Theorem~2.6]{ccama}) a verifier TM and an NTM are constructed.

  the one direction, if a language is decided by a polynomial-time NTM then a
  TM can be constructed that simulates the NTM on input $x$ by using the
  in the string $u$ for the nondeterministic choices. The strings $u$ have
  length $p(|x|)$. So for this construction to work, there must be a polynomial
 p$ that bounds the running time of the NTM. Clearly, a polynomial function with
  coefficients exists with that property.

  the other direction, assume a language has a verifier TM where $p$ is a
  function with natural coefficients. An NTM deciding this language
  $x$ as input, then ``guesses'' a string $u$ of length $p(|x|)$, and
  runs the verifier on the pair $\langle x, u\rangle$. For this NTM to run in
  time, $p$ must be computable in time polynomial in $|x|$. We have
  this to be the case in lemma @{thm [source] transforms_tm_polynomialI} in
 ~\ref{s:tm-arithmetic-poly}.
 ›

text ‹
  language $L_1$ is polynomial-time many-one reducible to a language $L_2$ if
  is a polynomial-time computable function $f_\mathit{reduce}$ such that for all
 x$, $x\in L_1$ iff.\ $f_\mathit{reduce}(x) \in L_2$.
 ›

definition reducible (infix ‹≤_p› 50) where
  "L₁ ≤_p L₂ ≡ ∃k G M T freduce.
    turing_machine k G M ∧
    big_oh_poly T ∧
    computes_in_time k M freduce T ∧
    (∀x. x ∈ L₁ ⟷ freduce x ∈ L₂)"

abbreviation NP_hard :: "language ==> bool" where
  "NP_hard L ≡ ∀L'∈NP. L' ≤_p L"

definition NP_complete :: "language ==> bool" where
  "NP_complete L ≡ L ∈ NP ∧ NP_hard L"

text ‹
  $c \geq 1$ in the definition of $\mathcal{P}$ is not essential:
 ›

lemma in_P_iff: "L ∈ P ⟷ (∃c. L ∈ DTIME (λn. n ^ c))"
proof
  assume "L ∈ P"
  then show "∃c. L ∈ DTIME (λn. n ^ c)"
    unfolding complexity_class_P_def using Suc_le_eq by auto
next
  assume "∃c. L ∈ DTIME (λn. n ^ c)"
  then obtain c where "L ∈ DTIME (λn. n ^ c)"
    by auto
  then obtain k G M T where M:
    "turing_machine k G M"
    "big_oh T (λn. n ^ c)"
    "computes_in_time k M (characteristic L) T"
    using DTIME_def by auto
  moreover have "big_oh T (λn. n ^ Suc c)"
  proof -
    obtain c0 n0 :: nat where c0n0: "∀n>n0. T n ≤ c0 * n ^ c"
      using M(2) big_oh_def by auto
    have "∀n>n0. T n ≤ c0 * n ^ Suc c"
    proof standard+
      fix n assume "n0 < n"
      then have "n ^ c ≤ n ^ Suc c"
        using pow_mono by simp
      then show "T n ≤ c0 * n ^ Suc c"
        using c0n0 by (metis ‹n0 < n› add.commute le_Suc_ex mult_le_mono2 trans_le_add2)
    qed
    then show ?thesis
      using big_oh_def by auto
  qed
  ultimately have "∃c>0. L ∈ DTIME (λn. n ^ c)"
    using DTIME_def by blast
  then show "L ∈ P"
    unfolding complexity_class_P_def by auto
qed


section ‹Restricting verifiers to one-bit output\label{s:np-alt}›

text ‹
  verifier Turing machine in the definition of $\NP$ can output any symbol
 . In this section we restrict it to outputting only the symbol sequence
 textbf{1} or \textbf{0}. This is equivalent to the definition because it is
  to check if a symbol sequence differs from \textbf{1} and if so change it
  \textbf{0}, as we show below.

  advantage of this restriction is that if we can make the TM halt with the
  tape head on cell number~1, the output tape symbol read in the final step
  the output of the TM. We will exploit this in Chapter~\ref{s:Reducing},
  we show how to reduce any language $L\in\NP$ to \SAT{}.

  next Turing machine checks if the symbol sequence on tape $j$ differs from
  one-symbol sequence \textbf{1} and if so turns it into \textbf{0}. It thus
  that the tape contains only one bit symbol.

 null
 ›

definition tm_make_bit :: "tapeidx ==> machine" where
  "tm_make_bit j ≡
    tm_cr j ;;
    IF λrs. rs ! j = 1 THEN
      tm_right j ;;
      IF λrs. rs ! j = ◻ THEN
        []
      ELSE
        tm_set j [0]
      ENDIF
    ELSE
      tm_set j [0]
    ENDIF"

lemma tm_make_bit_tm:
  assumes "G ≥ 4" and "0 < j" and "j < k"
  shows "turing_machine k G (tm_make_bit j)"
  unfolding tm_make_bit_def
  using assms tm_right_tm tm_set_tm tm_cr_tm Nil_tm turing_machine_branch_turing_machine
  by simp

locale turing_machine_make_bit =
  fixes j :: tapeidx
begin

definition "tm1 ≡ tm_cr j"
definition "tmT1 ≡ tm_right j"
definition "tmT12 ≡ IF λrs. rs ! j = ◻ THEN [] ELSE tm_set j [0] ENDIF"
definition "tmT2 ≡ tmT1 ;; tmT12"
definition "tm12 ≡ IF λrs. rs ! j = 1 THEN tmT2 ELSE tm_set j [0] ENDIF"
definition "tm2 ≡ tm1 ;; tm12"

lemma tm2_eq_tm_make_bit: "tm2 ≡ tm_make_bit j"
  unfolding tm_make_bit_def tm2_def tm12_def tmT2_def tmT12_def tmT1_def tm1_def by simp

context
  fixes tps0 :: "tape list" and zs :: "symbol list"
  assumes jk: "j < length tps0"
    and zs: "proper_symbols zs"
  assumes tps0: "tps0 ::: j = ⌊zs⌋"
begin

lemma clean: "clean_tape (tps0 ! j)"
  using zs tps0 contents_clean_tape' by simp

definition "tps1 ≡ tps0[j := (⌊zs⌋, 1)]"

lemma tm1 [transforms_intros]:
  assumes "ttt = tps0 :#: j + 2"
  shows "transforms tm1 tps0 ttt tps1"
  unfolding tm1_def by (tform tps: assms jk clean tps0 tps1_def)

definition "tpsT1 ≡ tps0[j := (⌊zs⌋, 2)]"

lemma tmT1 [transforms_intros]:
  assumes "ttt = 1"
  shows "transforms tmT1 tps1 ttt tpsT1"
  unfolding tmT1_def
proof (tform tps: assms tps1_def jk)
  show "tpsT1 = tps1[j := tps1 ! j |+| 1] "
    using tps1_def tpsT1_def jk
    by (metis Suc_1 fst_conv list_update_overwrite nth_list_update_eq plus_1_eq_Suc snd_conv)
qed

definition "tpsT2 ≡ tps0
  [j := if length zs ≤ 1 then (⌊zs⌋, 2) else (⌊[0]⌋, 1)]"

lemma tmT12 [transforms_intros]:
  assumes "ttt = 14 + 2 * length zs"
  shows "transforms tmT12 tpsT1 ttt tpsT2"
  unfolding tmT12_def
proof (tform tps: assms tpsT1_def tps0 jk zs)
  show "8 + tpsT1 :#: j + 2 * length zs + Suc (2 * length [0]) + 1 ≤ ttt"
    using tpsT1_def jk assms by simp
  have "read tpsT1 ! j = ⌊zs⌋ 2"
    using tpsT1_def jk tapes_at_read' by (metis fst_conv length_list_update nth_list_update_eq snd_conv)
  moreover have "⌊zs⌋ 2 = ◻ ⟷ length zs ≤ 1"
    using zs contents_def
    by (metis Suc_1 diff_Suc_1 less_imp_le_nat linorder_le_less_linear not_less_eq_eq zero_neq_numeral)
  ultimately have "read tpsT1 ! j = ◻ ⟷ length zs ≤ 1"
    by simp
  then show
      "read tpsT1 ! j ≠ ◻ ==> tpsT2 = tpsT1[j := (⌊[0]⌋, 1)]"
      "read tpsT1 ! j = ◻ ==> tpsT2 = tpsT1"
    using tpsT1_def tpsT2_def jk by simp_all
qed

lemma tmT2 [transforms_intros]:
  assumes "ttt = 15 + 2 * length zs"
  shows "transforms tmT2 tps1 ttt tpsT2"
  unfolding tmT2_def by (tform time: assms)

definition "tps2 ≡ tps0
  [j := if zs = [1] then (⌊zs⌋, 2) else (⌊[0]⌋, 1)]"

lemma tm12 [transforms_intros]:
  assumes "ttt = 17 + 2 * length zs"
  shows "transforms tm12 tps1 ttt tps2"
  unfolding tm12_def
proof (tform tps: assms tps0 jk zs tps1_def)
  have "read tps1 ! j = ⌊zs⌋ 1"
    using tps1_def jk tapes_at_read' by (metis fst_conv length_list_update nth_list_update_eq snd_conv)
  then have *: "read tps1 ! j = 1 ⟷ ⌊zs⌋ 1 = 1"
    by simp
  show "read tps1 ! j ≠ 1 ==> tps2 = tps1[j := (⌊[0]⌋, 1)]"
    using * tps2_def tps1_def by auto
  show "tps2 = tpsT2" if "read tps1 ! j = 1"
  proof (cases "zs = [1]")
    case True
    then show ?thesis
      using * tps2_def tpsT2_def by simp
  next
    case False
    then have "⌊zs⌋ 1 = 1"
      using * that by simp
    then have "length zs > 1"
      using False contents_def contents_outofbounds
      by (metis One_nat_def Suc_length_conv diff_Suc_1 length_0_conv linorder_neqE_nat nth_Cons_0 zero_neq_numeral)
    then show ?thesis
      using * tps2_def tpsT2_def by auto
  qed
  show "8 + tps1 :#: j + 2 * length zs + Suc (2 * length [0]) + 1 ≤ ttt"
    using tps1_def jk assms by simp
qed

lemma tm2:
  assumes "ttt = 19 + 2 * length zs + tps0 :#: j"
  shows "transforms tm2 tps0 ttt tps2"
  unfolding tm2_def by (tform tps: assms tps0 jk zs tps1_def)

end

end  (* locale *)

lemma transforms_tm_make_bitI [transforms_intros]:
  fixes j :: tapeidx 
  fixes tps tps' :: "tape list" and zs :: "symbol list" and ttt :: nat
  assumes "j < length tps" and "proper_symbols zs"
  assumes "tps ::: j = ⌊zs⌋"
  assumes "ttt = 19 + 2 * length zs + tps :#: j"
  assumes "tps' = tps
    [j := if zs = [1] then (⌊zs⌋, 2) else (⌊[0]⌋, 1)]"
  shows "transforms (tm_make_bit j) tps ttt tps'"
proof -
  interpret loc: turing_machine_make_bit j .
  show ?thesis
    using assms loc.tps2_def loc.tm2 loc.tm2_eq_tm_make_bit by simp
qed

lemma output_length_le_time:
  assumes "turing_machine k G M"
    and "tps ::: 1 = ⌊zs⌋"
    and "proper_symbols zs"
    and "transforms M (snd (start_config k xs)) t tps"
  shows "length zs ≤ t"
proof -
  have 1: "execute M (start_config k xs) t = (length M, tps)"
    using assms transforms_def transits_def
    by (metis (no_types, lifting) execute_after_halting_ge fst_conv start_config_def sndI)
  moreover have "k > 1"
    using assms(1) turing_machine_def by simp
  ultimately have "((execute M (start_config k xs) t) <:> 1) i = ◻" if "i > t" for i
    using assms blank_after_time that by (meson zero_less_one)
  then have "(tps ::: 1) i = ◻" if "i > t" for i
    using 1 that by simp
  then have *: "⌊zs⌋ i = ◻" if "i > t" for i
    using assms(2) that by simp
  show ?thesis
  proof (rule ccontr)
    assume "¬ length zs ≤ t"
    then have "length zs > t"
      by simp
    then have "⌊zs⌋ (Suc t) ≠ ◻"
      using contents_inbounds assms(3) contents_def proper_symbols_ne0 by simp
    then show False
      using * by simp
  qed
qed

text ‹
  is the alternative definition of $\NP$, which restricts the verifier
  output only strings of length one:
 ›

lemma NP_output_len_1:
  "NP = {L. ∃k G M p T fverify.
    turing_machine k G M ∧
    polynomial p ∧
    big_oh_poly T ∧
    computes_in_time k M fverify T ∧
    (∀y. length (fverify y) = 1) ∧
    (∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀 ]))}"
  (is "_ = ?M")
proof
  show "?M ⊆ NP"
    using complexity_class_NP_def by fast
  define Q where "Q = (λL k G M p T fverify.
    turing_machine k G M ∧
    polynomial p ∧
    big_oh_poly T ∧
    computes_in_time k M fverify T ∧
    (∀x. (x ∈ L) = (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀 ])))"
  have alt: "complexity_class_NP = {L::language. ∃k G M p T fverify. Q L k G M p T fverify}"
    unfolding complexity_class_NP_def Q_def by simp
  show "NP ⊆ ?M"
  proof
    fix L assume "L ∈ NP"
    then obtain k G M p T fverify where "Q L k G M p T fverify"
      using alt by blast
    then have ex:
      "turing_machine k G M ∧
       polynomial p ∧
       big_oh_poly T ∧
       computes_in_time k M fverify T ∧
       (∀x. (x ∈ L) = (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀 ]))"
      using Q_def by simp

    have "k ≥ 2" and "G ≥ 4"
      using ex turing_machine_def by simp_all

    define M' where "M' = M ;; tm_make_bit 1"
    define f' where "f' = (λy. if fverify y = [𝕀 ] then [𝕀 ] else [𝕆])"
    define T' where "T' = (λn. 19 + 4 * T n)"

    have "turing_machine k G M'"
      unfolding M'_def using ‹2 ≤ k› ‹4 ≤ G› ex tm_make_bit_tm by simp
    moreover have "polynomial p"
      using ex by simp
    moreover have "big_oh_poly T'"
      using T'_def ex big_oh_poly_const big_oh_poly_prod big_oh_poly_sum by simp
    moreover have "computes_in_time k M' f' T'"
    proof
      fix y
      let ?cfg = "start_config k (string_to_symbols y)"
      obtain tps where
        1: "tps ::: 1 = string_to_contents (fverify y)" and
        2: "transforms M (snd ?cfg) (T (length y)) tps"
        using ex computes_in_timeD by blast
      have len_tps: "length tps ≥ 2"
        by (smt (verit) "2" ‹2 ≤ k› ex execute_num_tapes start_config_length less_le_trans numeral_2_eq_2
          prod.sel(2) transforms_def transits_def zero_less_Suc)
      define zs where "zs = string_to_symbols (fverify y)"
      then have zs: "tps ::: 1 = ⌊zs⌋" "proper_symbols zs"
        using 1 by auto
      have transforms_MI [transforms_intros]: "transforms M (snd ?cfg) (T (length y)) tps"
        using 2 by simp
      define tps' where
        "tps' = tps[1 := if zs = [1] then (⌊zs⌋, 2) else (⌊[0]⌋, 1)]"

      have "transforms M' (snd ?cfg) (T (length y) + (19 + (tps :#: Suc 0 + 2 * length zs))) tps'"
        unfolding M'_def by (tform tps: zs len_tps tps'_def)
      moreover have "T (length y) + (19 + (tps :#: Suc 0 + 2 * length zs)) ≤ T' (length y)"
      proof -
        have "tps :#: Suc 0 ≤ T (length y)"
          using 2 transforms_def transits_def start_config_def ex head_pos_le_time `2 ≤ k`
          by (smt (verit, ccfv_threshold) One_nat_def Suc_1 Suc_le_lessD leD linorder_le_less_linear
            order_less_le_trans prod.sel(2))
        moreover have "length zs ≤ T (length y)"
          using zs 2 ex output_length_le_time by auto
        ultimately show ?thesis
          using T'_def 1 2 by simp
      qed
      ultimately have *: "transforms M' (snd ?cfg) (T' (length y)) tps'"
        using transforms_monotone by simp

      have "tps' ::: 1 = (if zs = [1] then tps ::: 1 else ⌊[0]⌋)"
        using tps'_def len_tps zs(1) by simp
      also have "... = (if zs = [1] then ⌊[1]⌋ else ⌊[0]⌋)"
        using zs(1) by simp
      also have "... = (if string_to_symbols (fverify y) = [3] then ⌊[3]⌋ else ⌊[2]⌋)"
        using zs_def by simp
      also have "... = (if fverify y = [𝕀 ] then ⌊[1]⌋ else ⌊[0]⌋)"
        by auto
      also have "... = (if fverify y = [𝕀 ] then string_to_contents [𝕀 ] else string_to_contents [𝕆])"
        by auto
      also have "... = string_to_contents (if fverify y = [𝕀 ] then [𝕀 ] else [𝕆])"
        by simp
      also have "... = string_to_contents (f' y)"
        using f'_def by auto
      finally have "tps' ::: 1 = string_to_contents (f' y)" .

      then show "∃tps'. tps' ::: 1 = string_to_contents (f' y) ∧
          transforms M' (snd ?cfg) (T' (length y)) tps'"
        using * by auto
    qed
    moreover have "∀y. length (f' y) = 1"
      using f'_def by simp
    moreover have "(∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ f' ⟨x, u⟩ = [𝕀 ]))"
      using ex f'_def by auto
    ultimately show "L ∈ ?M"
      by blast
  qed
qed



section ‹$\mathcal{P}$ is a subset of $\NP$\label{s:TC-subseteq}›

text ‹
  $L\in\mathcal{P}$ be a language and $M$ a Turing machine that decides $L$ in
  time. To show $L\in\NP$ we could use a TM that extracts the first
  from the input $\langle x, u\rangle$ and runs $M$ on $x$. We do not have
  construct such a TM explicitly because we have shown that the extraction of
  first pair element is computable in polynomial time (lemma~@{thm [source]
 }), and by assumption the characteristic function of $L$ is
  in polynomial time, too. The composition of these two functions is
  verifier function required by the definition of $\NP$. And by lemma~@{thm
 source] computes_composed_poly} the composition of polynomial-time functions is
 -time, too.

 null
 ›

theorem P_subseteq_NP: "P ⊆ NP"
proof
  fix L :: language
  assume "L ∈ P"
  then obtain c where c: "L ∈ DTIME (λn. n ^ c)"
    using complexity_class_P_def by auto
  then obtain k G M T' where M:
    "turing_machine k G M"
    "computes_in_time k M (characteristic L) T'"
    "big_oh T' (λn. n ^ c)"
    using DTIME_def by auto
  then have 4: "big_oh_poly T'"
    using big_oh_poly_def by auto

  define f where "f = (λx. symbols_to_string (first (bindecode (string_to_symbols x))))"
  define T :: "nat ==> nat" where "T = (λn. 9 + 4 * n)"
  have 1: "turing_machine 3 6 tm_first"
    by (simp add: tm_first_tm)
  have 2: "computes_in_time 3 tm_first f T"
    using f_def T_def tm_first_computes by simp
  have 3: "big_oh_poly T"
  proof -
    have "big_oh_poly (λn. 9)"
      using big_oh_poly_const by simp
    moreover have "big_oh_poly (λn. 4 * n)"
      using big_oh_poly_const big_oh_poly_prod big_oh_poly_poly[of 1] by simp
    ultimately show ?thesis
      using big_oh_poly_sum T_def by simp
  qed

  define fverify where "fverify = characteristic L ∘ f"
  then have *: "∃T k G M. big_oh_poly T ∧ turing_machine k G M ∧ computes_in_time k M fverify T"
    using M 1 2 3 4 computes_composed_poly by simp

  then have fverify: "fverify ⟨x, u⟩ = [x ∈ L]" for x u
    using f_def first_pair symbols_to_string_to_symbols fverify_def characteristic_def
    by simp

  define p :: "nat ==> nat" where "p = (λ_. 0)"
  then have "polynomial p"
    using const_polynomial by simp
  moreover have "∀x. x ∈ L ⟷ (∃u. length u = p (length x) ∧ fverify ⟨x, u⟩ = [𝕀 ])"
    using fverify p_def by simp
  ultimately show "L ∈ NP"
    using * complexity_class_NP_def by fast
qed


section ‹More about $\mathcal{P}$, $\NP$, and reducibility\label{s:TC-more}›

text ‹
  prove some low-hanging fruits about the concepts introduced in this chapter.
  of the results are needed to show the Cook-Levin theorem.
 ›

text ‹
  language can be reduced to itself by the identity function. Hence reducibility
  a reflexive relation.

 null
 ›

lemma reducible_refl: "L ≤_p L"
proof -
  let ?M = "tm_id"
  let ?T = "λn. Suc (Suc n)"
  have "turing_machine 2 4 ?M"
    using tm_id_tm by simp
  moreover have "big_oh_poly ?T"
  proof -
    have "big_oh_poly (λn. n + 2)"
      using big_oh_poly_const big_oh_poly_id big_oh_poly_sum by blast
    then show ?thesis
      by simp
  qed
  moreover have "computes_in_time 2 ?M id ?T"
    using computes_id by simp
  moreover have "∀x. x ∈ L ⟷ id x ∈ L"
    by simp
  ultimately show "L ≤_p L"
    using reducible_def by metis
qed

text ‹
  is also transitive. If $L_1 \leq_p L_2$ by a TM $M_1$ and $L_2
 leq_p L_3$ by a TM $M_2$ we merely have to run $M_2$ on the output of $M_1$ to
  that $L_1 \leq_p L_3$. Again this is merely the composition of two
 -time computable functions.
 ›

lemma reducible_trans:
  assumes "L₁ ≤_p L₂" and "L₂ ≤_p L₃"
  shows "L₁ ≤_p L₃"
proof -
  obtain k1 G1 M1 T1 f1 where 1:
     "turing_machine k1 G1 M1 ∧
      big_oh_poly T1 ∧
      computes_in_time k1 M1 f1 T1 ∧
      (∀x. x ∈ L₁ ⟷ f1 x ∈ L₂)"
    using assms(1) reducible_def by metis
  moreover obtain k2 G2 M2 T2 f2 where 2:
     "turing_machine k2 G2 M2 ∧
      big_oh_poly T2 ∧
      computes_in_time k2 M2 f2 T2 ∧
      (∀x. x ∈ L₂ ⟷ f2 x ∈ L₃)"
    using assms(2) reducible_def by metis
  ultimately obtain T k G M where
      "big_oh_poly T ∧ turing_machine k G M ∧ computes_in_time k M (f2 ∘ f1) T"
    using computes_composed_poly by metis
  moreover have "∀x. x ∈ L₁ ⟷ f2 (f1 x) ∈ L₃"
    using 1 2 by simp
  ultimately show ?thesis
    using reducible_def by fastforce
qed

text ‹
  usual way to show that a language is $\NP$-hard is to reduce another $\NP$-hard
  to it.
 ›

lemma ex_reducible_imp_NP_hard:
  assumes "NP_hard L'" and "L' ≤_p L"
  shows "NP_hard L"
  using reducible_trans assms by auto

text ‹
  converse is also true because reducibility is a reflexive relation.
 ›

lemma NP_hard_iff_reducible: "NP_hard L ⟷ (∃L'. NP_hard L' ∧ L' ≤_p L)"
proof
  show "NP_hard L ==> ∃L'. NP_hard L' ∧ L' ≤_p L"
    using reducible_refl by auto
  show "∃L'. NP_hard L' ∧ L' ≤_p L ==> NP_hard L"
    using ex_reducible_imp_NP_hard by blast
qed

lemma NP_complete_reducible:
  assumes "NP_complete L'" and "L ∈ NP" and "L' ≤_p L"
  shows "NP_complete L"
  using assms NP_complete_def reducible_trans by blast

text ‹
  a sense the complexity class $\mathcal{P}$ is closed under reduction.
 ›

lemma P_closed_reduction:
  assumes "L ∈ P" and "L' ≤_p L"
  shows "L' ∈ P"
proof -
  obtain c where c: "L ∈ DTIME (λn. n ^ c)"
    using assms(1) complexity_class_P_def by auto
  then obtain k G M T where M:
    "turing_machine k G M"
    "computes_in_time k M (characteristic L) T"
    "big_oh T (λn. n ^ c)"
    using DTIME_def by auto
  then have T: "big_oh_poly T"
    using big_oh_poly_def by auto

  obtain k' G' M' T' freduce where M':
    "turing_machine k' G' M'"
    "big_oh_poly T'"
    "computes_in_time k' M' freduce T'"
    "(∀x. x ∈ L' ⟷ freduce x ∈ L)"
    using reducible_def assms(2) by auto

  obtain T2 k2 G2 M2 where M2:
    "big_oh_poly T2"
    "turing_machine k2 G2 M2"
    "computes_in_time k2 M2 (characteristic L ∘ freduce) T2"
    using M T M' computes_composed_poly by metis

  obtain d where d: "big_oh T2 (λn. n ^ d)"
    using big_oh_poly_def M2(1) by auto

  have "characteristic L ∘ freduce = characteristic L'"
    using characteristic_def M'(4) by auto
  then have "∃k G M T'. turing_machine k G M ∧ big_oh T' (λn. n ^ d) ∧ computes_in_time k M (characteristic L') T'"
    using M2 d by auto
  then have "L' ∈ DTIME (λn. n ^ d)"
    using DTIME_def by simp
  then show ?thesis
    using in_P_iff by auto
qed

text ‹
  next lemmas are items~2 and~3 of Theorem~2.8 of the textbook~\cite{ccama}.
 ~1 is the transitivity of the reduction, already proved in lemma @{thm
 source] reducible_trans}.
 ›

lemma P_eq_NP:
  assumes "NP_hard L" and "L ∈ P"
  shows "P = NP"
  using assms P_closed_reduction P_subseteq_NP by auto

lemma NP_complete_imp:
  assumes "NP_complete L"
  shows "L ∈ P ⟷ P = NP"
  using assms NP_complete_def P_eq_NP by auto

end