show that there is an oracle B such that P^B != NP^B, formalized in Coq

np.v

Require Import Arith Bool Combinators FinFun Lia List.
Import ListNotations.
Open Scope list_scope.
Open Scope nat.
Scheme Equality for list.

(* helpers missing in the standard library *)

Lemma NoDup_app {A : Type} (a b : list A) : NoDup a -> NoDup b -> (forall x, In x a -> ~(In x b)) -> NoDup (a ++ b).
Proof.
  revert b.
  induction a.
	- intros. simpl. assumption.
	- intros. inversion H. subst. rewrite <-app_comm_cons. apply NoDup_cons.
	  -- unfold not. intros. apply in_app_or in H2. destruct H2. auto. apply (H1 a). apply in_eq. assumption.
	  -- apply (IHa b H5 H0). intros. apply (H1 x). simpl. auto.
Qed.

Lemma NoDup_prod {A B : Type} (a : list A) (b : list B) : NoDup a -> NoDup b -> NoDup (list_prod a b).
Proof.
  revert b.
  induction a; intros; simpl.
  - apply NoDup_nil.
  - remember (map (fun y => (a, y)) b).
	assert (NoDup l). rewrite Heql. apply Injective_map_NoDup. unfold Injective. intros. inversion H1. auto. auto.
	apply NoDup_app. auto. apply (IHa b). inversion H. auto. auto.
	intros. rewrite Heql in H2. destruct x. apply in_map_iff in H2. destruct H2. destruct H2. inversion H2. subst. clear H2.
	rewrite in_prod_iff. unfold not. intros. destruct H2. inversion H. contradiction.
Qed.

(* define computation model *)
Definition word := list bool.
Definition instructions := list word.
Definition algorithm := nat -> instructions.
Definition oracle := word -> bool.
Definition problem := oracle -> nat -> Prop.
Definition run := @find word.
Definition polynomial (algo : algorithm) := exists deg, forall n, length (algo n) <= n ^ deg + deg.
Definition decides (algo : algorithm) (prob : problem) := forall b n, (exists w, run b (algo n) = Some w) <-> prob b n.
Notation "x 'decides y" := (decides x y) (at level 75, right associativity).

(* helpers for word equality *)
Definition word_eq_dec := (list_eq_dec bool eqb (fun a b => proj1 (eqb_true_iff a b)) (fun a b => proj2 (eqb_true_iff a b))).
Definition word_beq := (list_beq bool eqb).

(* define our problem *)
(* given a set B and an oracle that decides it, determine if B contains any words of a given length n *)
Definition length_problem : problem := fun b n => exists w : word, length w = n /\ b w = true.

(* introduce an algorithm that decides the problem *)
Fixpoint solver (n : nat) : instructions := match n with
  | O => nil :: nil
  | S n => map (uncurry cons) (list_prod [true; false] (solver n))
end.

(* prove some properties of our algorithm *)

Lemma solver_cardinality (n : nat) : length (solver n) = 2 ^ n.
Proof.
  induction n.
	- auto.
	- simpl. rewrite map_length, app_length, app_nil_r. repeat rewrite map_length. rewrite IHn. auto.
Qed.

Lemma solver_nodup (n : nat) : NoDup (solver n).
Proof.
  induction n.
	- simpl. apply NoDup_cons_iff. split. auto. apply NoDup_nil.
	- unfold solver. fold solver.
	  apply Injective_map_NoDup. unfold Injective. intros. destruct x, y. inversion H. auto.
	  apply NoDup_prod.
	  repeat apply NoDup_cons; unfold not; intros; try inversion H; try discriminate; try inversion H0.
	  apply NoDup_nil. auto.
Qed.

Lemma in_solver_iff (n : nat) : forall w : word, length w = n <-> In w (solver n).
Proof.
  induction n.
	- split; intros.
	  -- destruct w. simpl. auto. inversion H.
	  -- inversion H. subst. auto. pose proof (in_nil H0). contradiction H1.
	- simpl. rewrite app_nil_r. split.
	  -- intros. simpl. destruct w. inversion H. replace (b :: w) with (uncurry cons (b, w)). 2: auto. apply in_map.
		 apply in_app_iff. destruct b; [left | right]; apply in_map, (IHn w); auto.
	  -- revert w. apply Forall_forall, Forall_map, Forall_app.
		 split; apply Forall_map, Forall_forall; intros; destruct (IHn x); specialize (H1 H); simpl; auto.
Qed.

(* various lemmas developing the central argument *)

(* a list that includes all binary words of length n contains at least 2^n entries *)
Lemma length_words_cardinality (n : nat) (l : list word) : (forall w, length w = n -> In w l) -> length l >= 2 ^ n.
Proof.
  intros.
  assert (incl (solver n) l). unfold incl. intros. apply (H a), in_solver_iff, H0.
  apply NoDup_incl_length in H0. rewrite (solver_cardinality n) in H0. auto.
  apply solver_nodup.
Qed.

(* an algorithm solves the problem iff it tests all words of length n only *)
Lemma solves_length_problem_iff (algo : algorithm) : (forall n w, length w = n <-> In w (algo n)) <-> algo 'decides length_problem.
Proof.
  unfold decides, length_problem, run.
  split.
  - split; intros; destruct H0.
	-- exists x. apply find_some in H0. destruct (H n x), H0. split; auto.
	-- case_eq (find b (algo n)). intros. exists w. reflexivity.
	   intros. exfalso. destruct (H n x), H0. pose proof (find_none _ _ H1 x (H2 H0)). destruct (b x); discriminate.
  - intros. remember (word_beq w) as b. specialize (H b n). destruct H.
	assert (forall x, w = x <-> b x = true).
	  split; rewrite Heqb; [apply internal_list_dec_lb | apply internal_list_dec_bl]; apply eqb_true_iff.
	assert (forall x, find b (algo n) = Some x -> w = x /\ In w (algo n)).
	  intros. apply find_some in H2. destruct H2. rewrite (proj2 (H1 x) H3). auto.
	split; intros.
	-- destruct (in_dec word_eq_dec w (algo n)). auto. exfalso.
	   assert (exists w, length w = n /\ b w = true). exists w. split. auto. apply (H1 w). auto.
	   destruct (H0 H4). destruct (H2 x H5). contradiction.
	-- case_eq (find b (algo n)). intros. destruct (H2 l H4). subst l.
	   assert (exists w : word, find b (algo n) = Some w). exists w. auto.
	   destruct (H H5). destruct H7. rewrite (proj2 (H1 x) H8). auto.
	   intros. pose proof (find_none _ _ H4 w H3). pose proof (proj1 (H1 w) (eq_refl w)). destruct (b w); discriminate.
Qed.

(* exponential runtime is not polynomial *)
Lemma exp_beats_poly : forall x, exists n, 2 ^ n > n ^ x + x.
Proof.
  intros.
  exists (2 ^ (x + 5)).
  unfold gt.
  transitivity (2 ^ S (2 ^ (x + 4))).
  2: { apply Nat.pow_lt_mono_r. lia. replace (x + 5) with (S (x + 4)). simpl Nat.pow at 2. rewrite Nat.add_0_r.
       rewrite <-Nat.add_1_l. apply Nat.add_lt_mono_r. replace 1 with (2 ^ 0) at 1. apply Nat.pow_lt_mono_r. 1-4: simpl; lia. }
  simpl Nat.pow. apply Nat.add_lt_le_mono. rewrite <-Nat.pow_mul_r. apply Nat.pow_lt_mono_r. lia. rewrite Nat.mul_add_distr_r.
  induction x. simpl. lia.
    simpl Nat.pow. replace (S x * S x + 5 * S x) with ((x * x + 5 * x) + (2 * x + 6)). 2: lia.
    rewrite Nat.add_0_r. apply Nat.add_lt_le_mono. apply IHx. clear IHx.
  induction x. simpl. lia.
    simpl Nat.pow. replace (2 * S x + 6) with ((2 * x + 6) + 2). 2: lia.
    rewrite Nat.add_0_r. apply Nat.add_le_mono. apply IHx. clear IHx.
  replace 2 with (2 ^ 1) at 1. 2: auto. apply Nat.pow_le_mono; lia.
  transitivity (2 ^ (x + 4)). transitivity (2 ^ x). apply Nat.lt_le_incl, Nat.pow_gt_lin_r. lia. apply Nat.pow_le_mono; lia.
  rewrite Nat.add_0_r. apply Nat.pow_le_mono; try lia. apply Nat.lt_le_incl, Nat.pow_gt_lin_r. lia.
Qed.

(* show that our problem lies in NP, but not in P (with respect to the oracle) *)

(* witnesses produced by the solver can be verified using a single instruction (checking if the witness is in the set) *)
(* since the verifiability of results in polynomial time is so trivial for this problem, we don't formalize it *)
(* to show that the algorithm lies in NP, we only demonstrate that the solver solves the problem *)
Theorem length_problem_in_NP : exists algo : algorithm, algo 'decides length_problem.
Proof.
  exists solver. apply solves_length_problem_iff, in_solver_iff.
Qed.

Theorem length_problem_not_in_P : ~exists algo : algorithm, polynomial algo /\ algo 'decides length_problem.
Proof.
  unfold not. intros. do 3 destruct H.
  destruct (exp_beats_poly x0) as (n,Hn).
  assert (forall w : word, length w = n -> In w (x n)). apply solves_length_problem_iff. auto.
  pose proof (length_words_cardinality n (x n) H1). specialize (H n).
  assert (2 ^ n <= n ^ x0 + x0). transitivity (length (x n)); auto.
  apply Arith_prebase.le_not_gt_stt in H3. contradiction.
Qed.