When Prop is classical while allowing subsingleton elimination, Markov Principle is for free.

MP.lean

section Acc_from_Coq

  variable {P : Nat → Prop}

  inductive Proof : Prop → Type where
  | proof : Q -> Proof Q

  variable {P_dec : ∀ n, (Proof (P n)) ⊕ (Proof (¬ (P n)))}

  abbrev R (x y : Nat) : Prop := x = y + 1 ∧ ¬ P y

  instance wfRel {r : α → α → Prop} : WellFoundedRelation { val // Acc r val } where
    rel := InvImage r (·.1)
    wf  := ⟨fun ac => InvImage.accessible _ ac.2⟩

  /-- A computable version of `Acc.rec`. Workaround until Lean has native support for this. -/
  def recC {motive : (a : α) → Acc r a → Sort v}
      (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) →
      ((y : α) → (hr : r y x) → motive y (h y hr)) → motive x (Acc.intro x h))
      {a : α} (t : Acc r a) : motive a t :=
    intro a (fun _ h => t.inv h) (fun _ hr => recC intro (t.inv hr))
  termination_by Subtype.mk a t

  theorem P_implies_acc : ∀ x, P x -> Acc (@R P) x :=
  by
    intro x H
    constructor
    intro y ⟨_, not_Px⟩
    contradiction

  theorem P_eventually_implies_acc : ∀ x n, P (n + x) -> Acc (@R P) x :=
  by
    intro x n
    revert x
    induction n with
    | zero =>
      simp
      apply P_implies_acc
    | succ n IH =>
      intro x H
      constructor
      intro y ⟨fxy, _⟩
      apply IH
      rewrite [fxy]
      rw [Nat.add_assoc] at H
      rw [Nat.add_comm 1 x] at H
      assumption

  theorem P_eventually_implies_acc_ex : (∃ n, P n) -> Acc (@R P) 0 :=
  by
    intro ⟨x, Px⟩
    apply P_eventually_implies_acc 0 x
    assumption

  def acc_implies_P_eventually : ∀ n, Acc (@R P) n -> Σ n, Proof (P n) :=
  by
    apply recC
    intro x IH f
    cases P_dec x with
    | inl Px =>
      exact ⟨x, Px⟩
    | inr not_Px =>
      let y := x + 1
      cases not_Px with
      | proof not_Px =>
      have Ryx : R y x := ⟨rfl, not_Px⟩
      have ⟨n, Hn⟩ := f y Ryx
      exact ⟨n, Hn⟩

  def constructive_indefinite_ground_description_nat_Acc :
    (∃ n, P n) -> Σ n, Proof (P n) :=
  by
    intro H
    apply acc_implies_P_eventually
    assumption
    apply P_eventually_implies_acc_ex
    assumption

  notation " ¬ " P => P → Empty

  def MarkovPrinciple :
    (¬¬ Σ n, Proof (P n)) -> Σ n, Proof (P n) :=
  by
    intro H
    apply constructive_indefinite_ground_description_nat_Acc
    assumption
    rw [← Classical.not_forall_not]
    intro h
    have f : Empty := by
    {
      apply H
      intro ⟨n, p⟩
      cases p with
      | proof p =>
        induction (h n p)
    }
    induction f

end Acc_from_Coq

def is_zero b := bif b then Unit else Empty

def bool_fun_to_pred (f : Nat → Bool) := λ n => Nonempty (is_zero (f n))

def bool_fun_to_pred_decidable (f : Nat → Bool) : ∀ n, Proof (bool_fun_to_pred f n) ⊕ Proof (¬ bool_fun_to_pred f n) :=
by
{
  intro n
  unfold bool_fun_to_pred is_zero
  cases (f n)
  {
    simp
    right
    constructor
    intro h
    cases h with
    | intro h =>
      contradiction
  }
  {
    simp
    left
    constructor
    constructor
    constructor
  }
}

def MarkovPrinciple2 : ∀ f : Nat → Bool, (¬¬ Σ n, is_zero (f n)) → (Σ n, is_zero (f n)) :=
by
  intro f H
  have j : ¬¬(n : Nat) × Proof (bool_fun_to_pred f n) :=
  by
    intro h
    apply H
    intro ⟨n, p⟩
    apply h
    exists n
    constructor
    unfold bool_fun_to_pred is_zero
    unfold is_zero at p
    revert p
    cases (f n)
    {
      simp
      intro h
      constructor
      assumption
    }
    {
      simp
      repeat constructor
    }
  have ⟨n, h⟩ := (@MarkovPrinciple _ (bool_fun_to_pred_decidable f) j)
  exists n
  revert h; unfold bool_fun_to_pred is_zero
  cases (f n)
  {
    simp
    intro h
    cases h with
    | proof h =>
      have j : False := by
        cases h with
        | intro h =>
          induction h
      induction j
  }
  {
    simp
    intro
    repeat constructor
  }