(** * Post's Theorem and Markov's Principle *)

Require Export DecidableEnumerable.
Require Import ConstructiveEpsilon.

Definition stable P := ~~ P -> P.

Definition MP := forall f : nat -> bool, stable (exists n, f n = true).

Definition mu (p : nat -> Prop) :
  (forall x, dec (p x)) -> ex p -> sig p.
Proof.
(* Goal: forall (_ : forall x : nat, dec (p x)) (_ : @ex nat p), @sig nat p *)
  apply constructive_indefinite_ground_description_nat_Acc.
Defined.

Local Notation R p :=
  (fun x y : nat => x = S y /\ ~ p y).

Lemma Acc_ind_dep (A : Type) (R : A -> A -> Prop) (P : forall a, Acc R a -> Prop) :
  (forall x (F : (forall y, R y x -> Acc R y)), (forall y (Hy : R y x), P y (F y Hy)) -> P x (Acc_intro x F))
  -> forall x (h : Acc R x), P x h.
Proof.
(* Goal: forall (_ : forall (x : A) (F : forall (y : A) (_ : R y x), @Acc A R y) (_ : forall (y : A) (Hy : R y x), P y (F y Hy)), P x (@Acc_intro A R x F)) (x : A) (h : @Acc A R x), P x h *)
  refine (fix f H x h := match h with Acc_intro _ F => _ end).
(* Goal: P x (@Acc_intro A R x F) *)
  apply H. intros y Hy. apply f, H.
Qed.

Notation mu' d H := (proj1_sig (mu d H)).

Lemma mu_least (p : nat -> Prop) (d : forall x, dec (p x)) (H : ex p) :
  forall n, p n -> mu' d H <= n.
Proof.
(* Goal: forall (n : nat) (_ : p n), le (@proj1_sig nat p (@mu p d H)) n *)
  intros n H'. unfold mu, constructive_indefinite_ground_description_nat_Acc.
(* Goal: le (@proj1_sig nat p (acc_implies_P_eventually p d (P_eventually_implies_acc_ex p H))) n *)
  unfold acc_implies_P_eventually. assert (Hn : 0 <= n) by omega. revert n H' Hn.
(* Goal: forall (n : nat) (_ : p n) (_ : le O n), le (@proj1_sig nat p (@Fix_F nat (fun x y : nat => and (@eq nat x (S y)) (not (p y))) (fun _ : nat => @sig nat (fun n1 : nat => p n1)) (fun (x : nat) (IH : forall (y : nat) (_ : and (@eq nat y (S x)) (not (p x))), @sig nat (fun n0 : nat => p n0)) => match d x with | left Px => @exist nat (fun n0 : nat => p n0) x Px | right not_Px => let (n0, Hn0) := IH (S x) (@conj (@eq nat (S x) (S x)) (not (p x)) (@eq_refl nat (S x)) not_Px) in @exist nat (fun n1 : nat => p n1) n0 Hn0 end) O (P_eventually_implies_acc_ex p H))) n *)
  generalize 0, (P_eventually_implies_acc_ex p H). clear H.
(* Goal: forall (n : nat) (a : @Acc nat (fun x y : nat => and (@eq nat x (S y)) (not (p y))) n) (n0 : nat) (_ : p n0) (_ : le n n0), le (@proj1_sig nat p (@Fix_F nat (fun x y : nat => and (@eq nat x (S y)) (not (p y))) (fun _ : nat => @sig nat (fun n2 : nat => p n2)) (fun (x : nat) (IH : forall (y : nat) (_ : and (@eq nat y (S x)) (not (p x))), @sig nat (fun n1 : nat => p n1)) => match d x with | left Px => @exist nat (fun n1 : nat => p n1) x Px | right not_Px => let (n1, Hn0) := IH (S x) (@conj (@eq nat (S x) (S x)) (not (p x)) (@eq_refl nat (S x)) not_Px) in @exist nat (fun n2 : nat => p n2) n1 Hn0 end) n a)) n0 *)
  intros k H. pattern k, H. apply (@Acc_ind_dep nat (R p)). clear k H.
(* Goal: forall (x : nat) (F : forall (y : nat) (_ : and (@eq nat y (S x)) (not (p x))), @Acc nat (fun x0 y0 : nat => and (@eq nat x0 (S y0)) (not (p y0))) y) (_ : forall (y : nat) (Hy : and (@eq nat y (S x)) (not (p x))) (n : nat) (_ : p n) (_ : le y n), le (@proj1_sig nat p (@Fix_F nat (fun x0 y0 : nat => and (@eq nat x0 (S y0)) (not (p y0))) (fun _ : nat => @sig nat (fun n1 : nat => p n1)) (fun (x0 : nat) (IH : forall (y0 : nat) (_ : and (@eq nat y0 (S x0)) (not (p x0))), @sig nat (fun n0 : nat => p n0)) => match d x0 with | left Px => @exist nat (fun n0 : nat => p n0) x0 Px | right not_Px => let (n0, Hn0) := IH (S x0) (@conj (@eq nat (S x0) (S x0)) (not (p x0)) (@eq_refl nat (S x0)) not_Px) in @exist nat (fun n1 : nat => p n1) n0 Hn0 end) y (F y Hy))) n) (n : nat) (_ : p n) (_ : le x n), le (@proj1_sig nat p (@Fix_F nat (fun x0 y : nat => and (@eq nat x0 (S y)) (not (p y))) (fun _ : nat => @sig nat (fun n1 : nat => p n1)) (fun (x0 : nat) (IH : forall (y : nat) (_ : and (@eq nat y (S x0)) (not (p x0))), @sig nat (fun n0 : nat => p n0)) => match d x0 with | left Px => @exist nat (fun n0 : nat => p n0) x0 Px | right not_Px => let (n0, Hn0) := IH (S x0) (@conj (@eq nat (S x0) (S x0)) (not (p x0)) (@eq_refl nat (S x0)) not_Px) in @exist nat (fun n1 : nat => p n1) n0 Hn0 end) x (@Acc_intro nat (fun x0 y : nat => and (@eq nat x0 (S y)) (not (p y))) x F))) n *)
  intros k F IH n H1 H2. cbn. destruct (d k) as [H|H]; trivial.
(* Goal: le (@proj1_sig nat p (let (n, Hn) := @Fix_F nat (fun x y : nat => and (@eq nat x (S y)) (not (p y))) (fun _ : nat => @sig nat (fun n0 : nat => p n0)) (fun (x : nat) (IH : forall (y : nat) (_ : and (@eq nat y (S x)) (not (p x))), @sig nat (fun n : nat => p n)) => match d x with | left Px => @exist nat (fun n : nat => p n) x Px | right not_Px => let (n, Hn) := IH (S x) (@conj (@eq nat (S x) (S x)) (not (p x)) (@eq_refl nat (S x)) not_Px) in @exist nat (fun n0 : nat => p n0) n Hn end) (S k) (F (S k) (@conj (@eq nat (S k) (S k)) (not (p k)) (@eq_refl nat (S k)) H)) in @exist nat (fun n0 : nat => p n0) n Hn)) n *)
  destruct Fix_F eqn : E. rewrite <- E. apply IH; trivial. clear E.
(* Goal: le (S k) n *)
  apply le_lt_eq_dec in H2 as [H2|H2]; subst; tauto.
Qed.

Definition ldecidable X (p : X -> Prop) :=
  forall x, p x \/ ~ p x.

Lemma weakPost X (p : X -> Prop) : discrete X ->
  ldecidable p -> enumerable p -> enumerable (compl p) -> decidable p.
Proof.
(* Goal: forall (_ : discrete X) (_ : @ldecidable X p) (_ : @enumerable X p) (_ : @enumerable X (@compl X p)), @decidable X p *)
  intros [E] % discrete_iff Hl [f Hf] [g Hg].
(* Goal: @decidable X p *)
  eapply decidable_iff. econstructor. intros x.
(* Goal: dec (p x) *)
  assert (exists n, f n = Some x \/ g n = Some x) by (destruct (Hl x); firstorder).
(* Goal: dec (p x) *)
  destruct (mu (p := fun n => f n = Some x \/ g n = Some x)) as [n HN]; trivial.
  - intros n. exact _.
  - decide (f n = Some x); decide (g n = Some x); firstorder.
Qed.

Lemma MP_to_decMP :
  MP -> (forall p : nat -> Prop, decidable p -> stable (exists n, p n)).
Proof.
(* Goal: forall (_ : MP) (p : forall _ : nat, Prop) (_ : @decidable nat p), stable (@ex nat (fun n : nat => p n)) *)
  intros H p [d Hd] ?.
(* Goal: @ex nat (fun n : nat => p n) *)
  specialize (H (fun x => if d x then true else false)).
(* Goal: @ex nat (fun n : nat => p n) *)
  destruct H.
(* Goal: P x (@Acc_intro A R x F) *)
  - intros ?. eapply H0. intros [n]. eapply H. exists n. now eapply Hd in H1 as ->.
  - specialize (Hd x). destruct (d x); try congruence. exists x. now eapply Hd.
Qed.

Lemma decMP_to_eMP :
  (forall p : nat -> Prop, decidable p -> stable (exists n, p n)) -> (forall X (p : X -> Prop), enumerable p -> stable (exists n, p n)).
Proof.
(* Goal: forall (_ : forall (p : forall _ : nat, Prop) (_ : @decidable nat p), stable (@ex nat (fun n : nat => p n))) (X : Type) (p : forall _ : X, Prop) (_ : @enumerable X p), stable (@ex X (fun n : X => p n)) *)
  intros dMP X p [e He] ?. destruct (dMP (fun n => e n <> None)).
  - exists (fun n => match e n with Some _ => true | _ => false end). intros; destruct (e x); firstorder congruence.
(* Goal: P x (@Acc_intro A R x F) *)
  - intros ?. eapply H. intros [x]. eapply H0. eapply He in H1 as [n].
(* Goal: @ex nat (fun n : nat => not (@eq (option X) (e n) (@None X))) *)
    exists n. congruence.
  - destruct (e x) eqn:E; try congruence. exists x0. eapply He. now exists x. 
Qed.

Lemma eMP_to_MP :
  (forall X (p : X -> Prop), enumerable p -> stable (exists n, p n)) -> MP.
Proof.
(* Goal: forall _ : forall (X : Type) (p : forall _ : X, Prop) (_ : @enumerable X p), stable (@ex X (fun n : X => p n)), MP *)
  intros eMP f ?. destruct (eMP nat (fun n => f n = true)).
  - eapply dec_count_enum. now exists f. exists Some. eauto.
  - firstorder. 
  - eauto.
Qed.

Lemma MP_enum_stable X (p : X -> Prop) :
  MP -> enumerable p -> discrete X -> forall x, stable (p x).
Proof.
(* Goal: forall (_ : MP) (_ : @enumerable X p) (_ : discrete X) (x : X), stable (p x) *)
  intros MP [f Hf] [d Hd] x. eapply MP_to_decMP with (p := fun n => f n = Some x) in MP.
  - intros H. rewrite Hf in *. now eapply MP.
  - exists (fun n => match f n with Some x' => d (x, x') | _ => false end).
    intros x0. destruct (f x0). rewrite <- (Hd (x,x1)). split. inversion 1. eauto. intros ->. eauto.
(* Goal: forall _ : @eq (option X) (@Some X x1) (@Some X x), @eq X x x1 *)
(* Goal: forall _ : @eq X x x1, @eq (option X) (@Some X x1) (@Some X x) *)
(* Goal: iff (@eq (option X) (@None X) (@Some X x)) (@eq bool false true) *)
    split; inversion 1.
Qed.

Definition POST' :=
  forall X (p : X -> Prop), discrete X -> enumerable p -> enumerable (fun x => ~ p x) -> ldecidable p.

Theorem MP_Post :
  MP -> POST'.
Proof.
(* Goal: forall _ : MP, POST' *)
  intros mp X p HX [f Hf] [g Hg].
(* Goal: @ldecidable X p *)
  cut (forall x, exists n, f n = Some x \/ g n = Some x).
  - intros H x. destruct (H x); firstorder.
(* Goal: forall x : nat, iff (not (@ex nat (fun n : nat => p n))) (@ex nat (fun _ : nat => @eq (option nat) (@None nat) (@Some nat x))) *)
  - intros x. apply (MP_to_decMP mp).
    + apply discrete_iff in HX as [H]. apply decidable_iff.
(* Goal: forall x0 : nat, dec (or (@eq (option X) (f x0) (@Some X x)) (@eq (option X) (g x0) (@Some X x))) *)
      constructor. intros n. exact _.
(* Goal: False *)
    + intros H. assert (H1 : ~ ~ (p x \/ ~ p x)) by tauto. firstorder.
Qed.

Lemma Post_to' :
   POST' -> MP.
Proof.
(* Goal: forall _ : POST', MP *)
  intros HP. apply eMP_to_MP. apply decMP_to_eMP.
(* Goal: forall (p : forall _ : nat, Prop) (_ : @decidable nat p), stable (@ex nat (fun n : nat => p n)) *)
  intros p [Hp] % decidable_iff H. destruct (HP nat (fun _ => exists n, p n)) with (x:=0); trivial.
(* Goal: inhabited (forall x y : nat, dec (@eq nat x y)) *)
  - eapply discrete_iff. econstructor. exact _.
  - change (enumerable (fun m => exists n, (fun (x : nat * nat) => p (snd x)) (m,n))).
(* Goal: @enumerable nat (fun m : nat => @ex nat (fun n : nat => (fun x : prod nat nat => p (@snd nat nat x)) (@pair nat nat m n))) *)
    apply projection. eapply dec_count_enum; try apply enumerable_nat_nat.
(* Goal: dec (p (@snd nat nat (@pair nat nat n m))) *)
    apply decidable_iff. constructor. intros [n m]. exact _.
(* Goal: forall x : nat, iff (not (@ex nat (fun n : nat => p n))) (@ex nat (fun _ : nat => @eq (option nat) (@None nat) (@Some nat x))) *)
  - exists (fun _ => None). intros x. firstorder congruence.
  - contradiction.
Qed.

Definition POST :=
  forall X (p : X -> Prop), discrete X -> enumerable p -> enumerable (fun x => ~ p x) -> decidable p.

Lemma Post_MP :
  POST <-> MP.
Proof.
(* Goal: iff POST MP *)
  split; intros.
  - intros ?. eapply Post_to'.
(* Goal: POST' *)
    intros ? ? ? ? ? ?. destruct (H X p H0 H1 H2) as [g].
(* Goal: not (@eq (option X) (e n) (@None X)) *)
    specialize (H3 x). destruct (g x); firstorder congruence.
  - intros ? ? ? ? ?. eapply weakPost; eauto.
(* Goal: @eq (option X) (@Some X x1) (@Some X x1) *)
(* Goal: iff (@eq (option X) (@None X) (@Some X x)) (@eq bool false true) *)
    eapply MP_Post; eauto.
Qed.

  
