Markov's principle implies Post's theorem, constructively.

MPimpliesPost.v

(* Post's theorem in computability theory states that a subset S ⊆ ℕ is
   decidable if both S and its complement ℕ \ S are semidecidable.
   Just how much classical logic is needed to prove the theorem, though?
   In this note we show that Markov's principle suffices.

   Rather than working with subsets of ℕ we work synthetically, with
   semidecidable and decidable truth values. (This is more general than
   the traditional Post's theorem.)
*)

Require Import Arith.

(* We first define decidable and semidecidable truth values. *)

Definition is_decidable (p : Prop) := p \/ ~ p.

Structure Bool := { Bval :> Prop ; Bdec : is_decidable Bval }.

Definition is_semidecidable (p : Prop) := exists f : nat -> Bool , (p <-> exists n, f n).

(* The statement of Markov's principle. *)

Definition MP :=
  forall p, is_semidecidable p -> ~ ~ p -> p.

(* The statement of Post's theorem. *)
Definition Post :=
  forall p, is_semidecidable p -> is_semidecidable (~ p) -> is_decidable p.

(* We need to know that a disjunction of semidecidable truth values
   is semidecidable. For this purpose we define the interleaving of
   two maps. *)

Definition interleave {A : Type} (f g : nat -> A) (n : nat) : A :=
  match Nat.EvenT_OddT_dec n with
  | inl (exist _ k _) => f k (* in even positions we use f *)
  | inr (exist _ k _) => g k (* in odd positions we use g *)
  end.

(* Interleaving does what it think it does. Is there a shorter proof? *)

Lemma interleave_even {A : Type} (f g : nat -> A) (n : nat) :
  interleave f g (2 * n) = f n.
Proof.
  unfold interleave.
  destruct (Nat.EvenT_OddT_dec (2 * n)) as [[k e] | [k e]].
  - f_equal.
    now apply (Nat.mul_cancel_l _ _ 2).
  - absurd (Nat.even 1 = true).
    + discriminate.
    + rewrite <- (Nat.even_add_mul_2 1 k).
      rewrite Nat.add_comm, <- e.
      apply Nat.EvenT_even.
      now exists n.
Defined.

Lemma interleave_odd {A : Type} (f g : nat -> A) (n : nat) :
  interleave f g (2 * n + 1) = g n.
Proof.
  unfold interleave.
  destruct (Nat.EvenT_OddT_dec (2 * n + 1)) as [[k e] | [k e]].
  - absurd (Nat.even 1 = true).
    + discriminate.
    + rewrite <- (Nat.even_add_mul_2 1 n).
      rewrite Nat.add_comm, e.
      apply Nat.EvenT_even.
      now exists k.
  - f_equal.
    apply (Nat.mul_cancel_l k n 2).
    + auto.
    + now apply (Nat.add_cancel_r _ _ 1).
Defined.

(* We are ready to prove the main theorem. *)

Theorem MP_implies_Post : MP -> Post.
Proof.
  intros mp p [f p_iff_f] [g np_iff_g].
  (* At this point we have a semidecidable proposition p
     and we're asked to decide it, i.e., prove p ∨ ¬p.
     We do so by applying Markov principle, reducing
     the problem to two subgoals. *)
  apply mp.
  - (* Subgoal #1: p ∨ ¬p is semidecidable *)
    (* We claim that p ∨ ¬p ⇔ ∃ n . interleave f g n = true *)
    exists (interleave f g ).
    split.
    + (* p ∨ ¬p ⇒ ∃ n . interleave f g n = true *)
      intros [H|H].
      * destruct (proj1 p_iff_f H) as [n ?].
        exists (2 * n).
        now rewrite interleave_even.
      * destruct (proj1 np_iff_g H) as [n ?].
        exists (2 * n + 1).
        now rewrite interleave_odd.
    + (* (∃ n . interleave f g n = true) ⇒ p ∨ ¬p *)
      intros [n I].
      destruct (Nat.EvenT_OddT_dec n) as [[k eq]|[k eq]] ; rewrite eq in I.
      * left.
        apply p_iff_f.
        exists k.
        now rewrite <- (interleave_even f g k).
      * right.
        apply np_iff_g.
        exists k.
        now rewrite <- (interleave_odd f g k).
  - (* Subgoal #2: ¬¬ (p ∨ ¬p) -- this one is just an intuitionistic tautology. *)
    unfold is_decidable ; tauto.
Qed.