Theory NP

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

theory NP
  imports Elementary Composing Symbol_Ops
begin

text ‹
In 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
the complexity class $\NP$ and the concept of polynomial-time many-one
reduction. Moreover, although not required for the Cook-Levin theorem, it
introduces the class $\mathcal{P}$ and contains a proof of $\mathcal{P}
\subseteq \NP$ (see Section~\ref{s:TC-subseteq}). The chapter concludes with
some easy results about $\mathcal{P}$, $\NP$ and reducibility in
Section~\ref{s:TC-more}.
›


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

text ‹
Arora 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$,
this means that for a language $L$ to be in $\mathcal{P}$, the Turing machine
deciding $L$ must check the empty string in zero steps. For a Turing machine to
halt in zero steps, it must start in the halting state, which limits its
usefulness. Because of this technical issue we define $\mathrm{DTIME}(T(n))$ as
the set of all languages that can be decided with a running time in $O(T(n))$,
which seems a common enough alternative~\cite{lv-aikc,sipser2006,cz-dtime}.
›

text ‹
Languages are sets of strings, and deciding a language means computing its
characteristic 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" ("𝒫") where
  "𝒫  c{1..}. DTIME (λn. n ^ c)"

text ‹
A language $L$ is in $\NP$ if there is a polynomial $p$ and a polynomial-time
Turing 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.
\]
The string $u$ does not seem to have a name in general, but in case the verifier
outputs $\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" ("𝒩𝒫") where
  "𝒩𝒫  {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 ‹
The definition of $\NP$ is the one place where we need an actual polynomial
function, namely $p$, rather than a function that is merely bounded by a
polynomial. This raises the question as to the definition of a polynomial
function. Arora and Barak~\cite{ccama} do not seem to give a definition in the
context 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
a_i\cdot n^i$, as polynomials do.  We have filled in the gap in this definition
in Section~\ref{s:tm-basic-bigoh} by letting the coefficients $a_i$ be natural
numbers.

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

For the one direction, if a language is decided by a polynomial-time NTM then a
verifier TM can be constructed that simulates the NTM on input $x$ by using the
bits in the string $u$ for the nondeterministic choices. The strings $u$ have
the 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
natural coefficients exists with that property.

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

text ‹
A language $L_1$ is polynomial-time many-one reducible to a language $L_2$ if
there 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
  "L1 p L2  k G M T freduce.
    turing_machine k G M 
    big_oh_poly T 
    computes_in_time k M freduce T 
    (x. x  L1  freduce x  L2)"

abbreviation NP_hard :: "language  bool" where
  "NP_hard L  L'𝒩𝒫. L' p L"

definition NP_complete :: "language  bool" where
  "NP_complete L  L  𝒩𝒫  NP_hard L"

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

lemma in_P_iff: "L  𝒫  (c. L  DTIME (λn. n ^ c))"
proof
  assume "L  𝒫"
  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  𝒫"
    unfolding complexity_class_P_def by auto
qed


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

text ‹
The verifier Turing machine in the definition of $\NP$ can output any symbol
sequence. 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
easy to check if a symbol sequence differs from \textbf{1} and if so change it
to \textbf{0}, as we show below.

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

The next Turing machine checks if the symbol sequence on tape $j$ differs from
the one-symbol sequence \textbf{1} and if so turns it into \textbf{0}. It thus
ensures 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 = 𝟭 THEN
      tm_right j ;;
      IF λrs. rs ! j =  THEN
        []
      ELSE
        tm_set j [𝟬]
      ENDIF
    ELSE
      tm_set j [𝟬]
    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 [𝟬] ENDIF"
definition "tmT2  tmT1 ;; tmT12"
definition "tm12  IF λrs. rs ! j = 𝟭 THEN tmT2 ELSE tm_set j [𝟬] 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 ([𝟬], 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 [𝟬]) + 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 := ([𝟬], 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 = [𝟭] then (zs, 2) else ([𝟬], 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 = 𝟭  zs 1 = 𝟭"
    by simp
  show "read tps1 ! j  𝟭  tps2 = tps1[j := ([𝟬], 1)]"
    using * tps2_def tps1_def by auto
  show "tps2 = tpsT2" if "read tps1 ! j = 𝟭"
  proof (cases "zs = [𝟭]")
    case True
    then show ?thesis
      using * tps2_def tpsT2_def by simp
  next
    case False
    then have "zs 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 [𝟬]) + 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 = [𝟭] then (zs, 2) else ([𝟬], 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 ‹
This is the alternative definition of $\NP$, which restricts the verifier
to output only strings of length one:
›

lemma NP_output_len_1:
  "𝒩𝒫 = {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  𝒩𝒫"
    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 "𝒩𝒫  ?M"
  proof
    fix L assume "L  𝒩𝒫"
    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 = [𝟭] then (zs, 2) else ([𝟬], 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 = [𝟭] then tps ::: 1 else [𝟬])"
        using tps'_def len_tps zs(1) by simp
      also have "... = (if zs = [𝟭] then [𝟭] else [𝟬])"
        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 [𝟭] else [𝟬])"
        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 ‹
Let $L\in\mathcal{P}$ be a language and $M$ a Turing machine that decides $L$ in
polynomial time. To show $L\in\NP$ we could use a TM that extracts the first
element from the input $\langle x, u\rangle$ and runs $M$ on $x$. We do not have
to construct such a TM explicitly because we have shown that the extraction of
the first pair element is computable in polynomial time (lemma~@{thm [source]
tm_first_computes}), and by assumption the characteristic function of $L$ is
computable in polynomial time, too.  The composition of these two functions is
the verifier function required by the definition of $\NP$. And by lemma~@{thm
[source] computes_composed_poly} the composition of polynomial-time functions is
polynomial-time, too.

\null
›

theorem P_subseteq_NP: "𝒫  𝒩𝒫"
proof
  fix L :: language
  assume "L  𝒫"
  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  𝒩𝒫"
    using * complexity_class_NP_def by fast
qed


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

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

text ‹
A language can be reduced to itself by the identity function. Hence reducibility
is 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 ‹
Reducibility 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
show that $L_1 \leq_p L_3$. Again this is merely the composition of two
polynomial-time computable functions.
›

lemma reducible_trans:
  assumes "L1 p L2" and "L2 p L3"
  shows "L1 p L3"
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  L1  f1 x  L2)"
    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  L2  f2 x  L3)"
    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  L1  f2 (f1 x)  L3"
    using 1 2 by simp
  ultimately show ?thesis
    using reducible_def by fastforce
qed

text ‹
The usual way to show that a language is $\NP$-hard is to reduce another $\NP$-hard
language 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 ‹
The 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  𝒩𝒫" and "L' p L"
  shows "NP_complete L"
  using assms NP_complete_def reducible_trans by blast

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

lemma P_closed_reduction:
  assumes "L  𝒫" and "L' p L"
  shows "L'  𝒫"
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 ‹
The next lemmas are items~2 and~3 of Theorem~2.8 of the textbook~\cite{ccama}.
Item~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  𝒫"
  shows "𝒫 = 𝒩𝒫"
  using assms P_closed_reduction P_subseteq_NP by auto

lemma NP_complete_imp:
  assumes "NP_complete L"
  shows "L  𝒫  𝒫 = 𝒩𝒫"
  using assms NP_complete_def P_eq_NP by auto

end