From Coq.Logic Require Import ConstructiveEpsilon.
Require Import Lia Nat.
From stdpp Require Import numbers list list_numbers.
From SyntheticComputability Require Import SemiDecidabilityFacts DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts reductions Axioms.Equivalence halting FinChoice Dec.

Lemma decidable_AC X :
  forall R : X -> nat -> Prop, decidable (uncurry R) -> (forall x, exists n, R x n) -> exists f, forall x, R x (f x).
Proof.
  intros R [f Hf] Htot.
  destruct (decider_AC _ f R) as [g Hg]; eauto.
Qed.

Lemma semi_decidable_AC X :
  forall R : X -> nat -> Prop, semi_decidable (uncurry R) -> (forall x, exists n, R x n) -> exists f, forall x, R x (f x).
Proof.
  intros R [f Hf] Htot.
  destruct (semi_decider_AC _ f R) as [g Hg]; eauto.
Qed.

Lemma sdec_compute_lor {X} {p q : X -> Prop} :
  semi_decidable p -> semi_decidable q -> (forall x, p x \/ q x) -> exists f : X -> bool, forall x, if f x then p x else q x.
Proof.
  intros Hp Hq Hpq.
  edestruct (semi_decidable_AC X (fun x n => if n is 0 then p x else q x)) as [f Hf].
  - destruct Hp as [f1 H1], Hq as [f2 H2]. red in H1, H2.
    exists (fun '(x,n) m => if n is 0 then f1 x m else f2 x m).
    now intros (x,[]); cbn; rewrite ?H1, ?H2.
  - intros x. destruct (Hpq x). now exists 0. now exists 1.
  - exists (fun x => if f x is 0 then true else false). intros x.
    specialize (Hf x). destruct (f x); firstorder.
Qed.

Lemma inspect_opt {X} (o : option X) :
  {x | o = Some x} + {o = None}.
Proof.
  destruct o; eauto.
Qed.

Lemma enumerable_AC :
  forall X, discrete X -> forall Y, forall R : X -> Y -> Prop, enumerable (uncurry R) -> (forall x, exists n, R x n) -> exists f, forall x, R x (f x).
Proof.
  intros X [d Hd] Y R [f Hf] Htot.
  destruct (enumerator_AC _ _ f d _ Hd Hf Htot) as [g Hg].
  now exists g.
Qed.

Lemma finite_AC :
  forall X, discrete X -> finiteᵗ X -> forall Y,
    forall R : X -> Y -> Prop, (forall x, exists y, R x y) -> exists f : X -> Y, forall x, R x (f x).
Proof.
  intros X [D] % discrete_iff Hfin Y R Htot.
  eapply finite_choice; auto.
Qed.

Definition Fext := forall X Y (f g : X -> Y), (forall x, f x = g x) -> f = g.
Definition Pext := forall P Q : Prop, P <-> Q -> P = Q.
Definition hProp (P : Prop) := forall x1 x2 : P, x1 = x2.
Definition PI := forall P : Prop, hProp P.

Lemma Pext_to_PI :
  Pext -> PI.
Proof.
  intros pext P x1 x2.
  assert (P = True) as -> by firstorder.
  now destruct x1, x2.
Qed.

Lemma hProp_disj P Q :
  hProp P -> hProp Q -> ~ (P /\ Q) -> hProp (P \/ Q).
Proof.
  unfold hProp.
  intros hP hQ H [H1 | H1] [H2 | H2]; f_equal; firstorder; exfalso; tauto.
Qed.

Lemma Fext_hProp_neg P :
  Fext -> hProp (~ P).
Proof.
  intros fext H1 H2.
  eapply fext. intros x. exfalso. tauto.
Qed.

Lemma Fext_hProp_disj P :
  Fext -> hProp P -> hProp (P \/ ~ P).
Proof.
  intros. now eapply hProp_disj; [ | eapply Fext_hProp_neg | ].
Qed.

Lemma Fext_hProp_wdisj P :
  Fext -> hProp (~ P \/ ~~ P).
Proof.
  intros. now eapply Fext_hProp_disj; [ | eapply Fext_hProp_neg].
Qed.

Section CT_wrong.

  Context {Part : partiality}.

  Variable ϕ : nat -> nat -> nat -> option nat.
  Variable Hϕ : forall c x, monotonic (ϕ c x).

  Definition CT_Sigma := forall f : nat -> nat, {c : nat | forall x, exists n, ϕ c x n = Some (f x) }.

  Lemma CT_Sigma_wrong : CT_Sigma -> Fext -> False.
  Proof.
    intros CT fext.
    eapply K_nat_undec. {
      right. exists ϕ. split; try eassumption.
      intros f. unshelve eexists.
      + intros x. destruct (CT (f x)) as [c]. exact c.
      + intros x y. cbn. destruct (CT (f x)) as [c Hc]; eauto.
    }
    exists (fun f => Nat.eqb (proj1_sig (CT f)) (proj1_sig (CT (fun _ => 0)))).
    intros f.
    destruct (PeanoNat.Nat.eqb_spec (` (CT f)) (` (CT (fun _ : nat => 0)))).
    - unfold reflects. intuition.
      destruct (CT f) as [cf Hf].
      destruct (CT (fun _ => 0)) as [cc Hc]. cbn in *. subst.
      destruct (Hf n), (Hc n).
      eapply monotonic_agnostic; eauto.
    - unfold reflects. intuition try congruence.
      assert (f = fun x => 0) as -> by now apply fext.
      congruence.
  Qed.

End CT_wrong.

Definition LEM := forall P, P \/ ~ P.
Definition DNE := forall P, ~~P -> P.
Definition DGP := forall P Q : Prop, (P -> Q) \/ (Q -> P).
Definition WLEM := forall P, ~~P \/ ~ P.

Definition IP := forall (P : Prop), forall p : nat -> Prop, (P -> exists n, p n) -> exists n, P -> p n.

Lemma LEM_to_DGP :
  LEM -> DGP.
Proof.
  intros H P Q.
  destruct (H P), (H Q); tauto.
Qed.

Lemma DGP_to_WLEM :
  DGP -> WLEM.
Proof.
  intros H P.
  destruct (H P (~ P)); tauto.
Qed.

Lemma LEM_to_IP : LEM -> IP.
Proof.
  intros H P p.
  destruct (H P) as [H0 | H0].
  - intros [n H1] % (fun H1 => H1 H0). eauto.
  - exists 0. tauto.
Qed.

(*

    LEM --> DGP --> WLEM  
     |               |
     |               |
     v               v
    LPO     -->    WLPO   -->   LLPO
     ^               ^
     |               |
     v               v
  MP /\ WLPO     PFP /\ LLPO

     ^
     |
     
  MP /\ IP

 *)

Definition LPO := forall f : nat -> bool, (exists n, f n = true) \/ ~ (exists n, f n = true).
Definition WLPO := forall f : nat -> bool, (forall n, f n = false) \/ ~ (forall n, f n = false).

Lemma forall_neg_exists_iff (f : nat -> bool) :
  (forall n, f n = false) <-> ~ exists n, f n = true.
Proof.
  split.
  - intros H [n Hn]. rewrite H in Hn. congruence.
  - intros H n. destruct (f n) eqn:E; try reflexivity.
    destruct H. eauto.
Qed.

Lemma LEM_to_LPO : LEM -> LPO.
Proof.
  cbv. intuition.
Qed.

Lemma WLEM_to_WLPO : WLEM -> WLPO.
Proof.
  intros H f. rewrite forall_neg_exists_iff.
  edestruct H; eauto.
Qed.

Lemma LPO_to_WLPO : LPO -> WLPO.
Proof.
  intros H f. rewrite forall_neg_exists_iff.
  edestruct H; eauto.
Qed.

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

Lemma LPO_semidecidable_iff :
  LPO <-> LPO_semidecidable.
Proof.
  split.
  - intros H X p [f Hf] x. red in Hf.
    rewrite Hf. eapply H.
  - intros H f.
    eapply (H unit (fun _ => exists n, f n = true)).
    exists (fun _ => f). cbv. intuition. econstructor.
Qed.

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

Lemma WLPO_semidecidable_iff :
  WLPO <-> WLPO_semidecidable.
Proof.
  split.
  - intros H X p [f Hf] x. red in Hf.
    rewrite Hf. rewrite <- forall_neg_exists_iff.
    eapply H.
  - intros H f.
    rewrite forall_neg_exists_iff.
    eapply (H unit (fun _ => exists n, f n = true)).
    exists (fun _ => f). cbv. intuition. econstructor.
Qed.

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

Lemma WLPO_cosemidecidable_iff :
  WLPO_cosemidecidable <-> WLPO_semidecidable.
Proof.
  split.
  - intros H X p [f Hf] x. red in Hf.
    rewrite Hf. rewrite <- forall_neg_exists_iff.
    eapply (H _ (fun x => forall n, f x n = false)).
    exists f. red. reflexivity.
  - intros H X p [f Hf] x. red in Hf.
    rewrite Hf. rewrite forall_neg_exists_iff.
    eapply (H _ (fun x => exists n, f x n = true)).
    exists f. intros x'. reflexivity.
Qed.

Definition CODING :=
  exists F : (nat -> bool) -> nat, forall f, F f = F (fun _ => false) <-> forall n, f n = false.

Lemma no_CODING :
  CODING -> decidable (compl K_nat_bool).
Proof.
  intros [F HF].
  exists (fun f => Nat.eqb (F f) (F (fun _ => false))).
  intros f. unfold compl, K_nat_bool. red. rewrite <- forall_neg_exists_iff.
  destruct (Nat.eqb_spec (F f) (F (fun _ => false))); rewrite <- HF.
  all: firstorder congruence.
Qed.

Definition LLPO := forall f g : nat -> bool, ((exists n, f n = true) -> (exists n, g n = true)) \/ ((exists n, g n = true) -> (exists n, f n = true)).
Definition DM_Sigma_0_1 := forall f g : nat -> bool, ~ ((exists n, f n = true) /\ (exists n, g n = true)) -> ~ (exists n, f n = true) \/ ~ (exists n, g n = true).
Definition DGP_sdec := forall X (p : X -> Prop), semi_decidable p -> forall x y, (p x -> p y) \/ (p y -> p x).
Definition DM_sdec := forall X (p q : X -> Prop), semi_decidable p -> semi_decidable q -> forall x, ~ (p x /\ q x) -> ~ p x \/ ~ q x.
Definition LLPO_split := forall f : nat -> bool, (forall n m, f n = true -> f m = true -> n = m) -> (forall n, f (2 * n) = false) \/ (forall n, f (1 + 2 * n) = false).

Lemma LLPO_to_DM_Sigma_0_1 :
  LLPO -> DM_Sigma_0_1.
Proof.
  intros H f g Hfg.
  destruct (H f g); tauto.
Qed.

Lemma LLPO_iff_DGP_sdec :
  LLPO <-> DGP_sdec.
Proof.
  split.
  - intros H X p [f Hf] x y.
    unfold semi_decider in *.
    rewrite !Hf. eapply H.
  - intros H f g.
    unshelve eapply (H bool (fun b => if b then exists n, f n = true else exists n, g n = true) _ true false).
    + exists (fun b : bool => if b then f else g). red. intros []; reflexivity.
Qed.

Lemma DM_Sigma_0_1_iff_DM_sdec :
  DM_Sigma_0_1 <-> DM_sdec.
Proof.
  split.
  - intros H X p q [f Hf] [g Hg] x.
    unfold semi_decider in *.
    rewrite Hf, Hg. eapply H.
  - intros H f g Hfg.
    eapply (H unit (fun _ => exists n, f n = true) (fun _ => exists n, g n = true)).
    + exists (fun _ => f). red. reflexivity.
    + exists (fun _ => g). red. reflexivity.
    + econstructor.
    + eassumption.
Qed.

Lemma neg_neg_XM P :
  ~~ (P \/ ~ P).
Proof.
  tauto.
Qed.

Lemma DM_Sigma_0_1_iff_totality :
  DM_Sigma_0_1 <-> (forall X (R : X -> bool -> Prop), co_semi_decidable (uncurry R) -> forall n, ~~ (exists b, R n b) -> exists b, R n b).
Proof.
  split.
  - intros H X R [f Hf'] n.
    assert (Hf : forall n b, R n b <-> forall m, f (n, b) m = false) by (intros; eapply (Hf' (_, b))).
    setoid_rewrite Hf. clear - H. intros Hb.
    destruct (H (f (n, true)) (f (n, false))) as [H1 | H1].
    + intros [ [n1 ?] [n2 ?]]. eapply Hb. intros [[] ?]; congruence.
    + exists true. now eapply forall_neg_exists_iff.
    + exists false. now eapply forall_neg_exists_iff.
  - intros H f g Hfg.
    edestruct (H nat (fun _ b => if b then forall n, f n = false else forall n, g n = false)) with (n := 0) as [[] H1].
    + exists (fun '(n,b) => if b : bool then f else g). now intros (n, []).
    + intros H0. eapply (neg_neg_XM (exists n, f n = true)). intros [H1 | H1].
      * eapply (neg_neg_XM (exists n, g n = true)). intros [H2 | H2].
        -- eauto.
        -- eapply H0. exists false. now eapply forall_neg_exists_iff.
      * eapply H0. exists true. now eapply forall_neg_exists_iff.
    + left. now eapply forall_neg_exists_iff.
    + right. now eapply forall_neg_exists_iff.
Qed.

Lemma DM_Sigma_0_1_to_LLPO_split :
  DM_Sigma_0_1 -> LLPO_split.
Proof.
  intros H f Huni.
  destruct (H (fun n => f (2 * n)) (fun n => (f (1 + 2 * n)))).
  - intros [[n Hn] [m Hm]].
    eapply Huni in Hn; eauto. lia.
  - left. now rewrite forall_neg_exists_iff.
  - right. now rewrite forall_neg_exists_iff.
Qed.

Lemma dec_bounded_quant P n :
  (forall m, m <= n -> P m \/ ~ P m) -> (forall m, m <= n -> ~ P m) \/ exists m, m <= n /\ P m.
Proof.
  intros H.
  induction n.
  - destruct (H 0 (Nat.le_refl 0)).
    + right. exists 0. split. lia. eauto.
    + left. intros m Hm. enough (m = 0) by now subst. lia.
  - destruct IHn as [H1 | [m [Hle Hm]]].
    + intros. eapply H. lia.
    + destruct (H (S n) (Nat.le_refl _)).
      * right. eauto.
      * left. intros m [Hle | ->] % le_lt_or_eq; eauto.
        eapply H1. lia.
    + right. exists m. split. lia. eassumption.
Qed.

Lemma least_ex (P : nat -> Prop) n : P n -> (forall m, m < n -> P m \/~ P m) -> exists n, P n /\ forall m, P m -> m >= n.
Proof.
  induction n using lt_wf_rec.
  intros Hn Hlt.
  destruct n.
  - exists 0. split. eauto. intros. lia.
  - edestruct dec_bounded_quant with (n := n).
    + intros. eapply (Hlt m). lia.
    + exists (S n). split. eauto. intros.
      destruct (le_lt_dec (S n) m); eauto. eapply H0 in H1; lia.
    + destruct H0 as (m & Hle & Hm).
      eapply (H m).
      * lia.
      * eassumption.
      * intros. eapply Hlt. lia.
Qed.

Lemma LLPO_split_to_LLPO :
  LLPO_split -> LLPO.
Proof.
  intros H f g.
  pose (alpha := (fun n => if n `mod` 2 =? 0 then f (n `div` 2) else g (n `div` 2))).
  pose (alpha' n := alpha n && forallb negb (map alpha (seq 0 n))).
  destruct (H alpha') as [H0 | H0].
  - intros n m [Ha1 Ha2] % andb_true_iff [Ha3 Ha4] % andb_true_iff.
    destruct (lt_eq_lt_dec n m) as [ [Hl | ] | Hl]; eauto.
    + rewrite forallb_forall in Ha4.
      setoid_rewrite in_map_iff in Ha4.
      setoid_rewrite in_seq in Ha4.
      enough (false = true) by congruence.
      eapply (Ha4 true). cbn. exists n. repeat split; eauto with arith.
    + rewrite forallb_forall in Ha2.
      setoid_rewrite in_map_iff in Ha2.
      setoid_rewrite in_seq in Ha2.
      enough (false = true) by congruence.
      eapply (Ha2 true). cbn. exists m. repeat split; eauto with arith.
  - left. intros [m Hm].
    destruct (least_ex (fun n => f n = true) _ Hm) as [n [Hn Hle]].
    { intros x. destruct (f x); firstorder congruence. }
    clear m Hm.
    assert (alpha (n * 2) = true). {
      unfold alpha. rewrite Nat.mod_mul. rewrite Nat.eqb_refl.
      rewrite Nat.div_mul. eauto. lia. lia.
    }
    destruct (dec_bounded_quant (fun n => g n = true) n).
    + intros m ?; destruct (g m); firstorder congruence.
    + exfalso. enough (alpha' (2 * n) = true). rewrite H0 in H3. congruence.
      rewrite mult_comm. unfold alpha'.
      eapply andb_true_iff. split. eauto.
      eapply forallb_forall.
      intros b. rewrite in_map_iff. setoid_rewrite in_seq.
      intros [k [H3 [_ H4] ]]. destruct b; try reflexivity.
      unfold alpha in H3.
      exfalso. destruct (k `mod` 2) eqn:Em.
      * cbn [Nat.eqb] in H3. eapply Hle in H3. cbn in H4.
        pose proof (Nat.div_lt_upper_bound k 2 n).
        lia.
      * cbn [Nat.eqb] in H3. eapply H2 in H3. lia.
        eapply Nat.div_le_upper_bound. lia. lia.
    + firstorder.
  - right. intros [m Hm].
    destruct (least_ex (fun n => g n = true) _ Hm) as [n [Hn Hle]].
    { intros x. destruct (g x); firstorder congruence. }
    clear m Hm.
    assert (alpha (1 + n * 2) = true). {
      unfold alpha. rewrite Nat.mod_add; try lia.
      change (1 `mod` 2 =? 0) with false. hnf.
      rewrite Nat.div_add. cbn. eauto. lia.
    }
    destruct (dec_bounded_quant (fun n => f n = true) (S n)).
    + intros m ?; destruct (f m); firstorder congruence.
    + exfalso. enough (H3 : alpha' (1 + 2 * n) = true). rewrite H0 in H3. congruence.
      rewrite mult_comm. unfold alpha'.
      eapply andb_true_iff. split. eauto.
      eapply forallb_forall.
      intros b. rewrite in_map_iff. setoid_rewrite in_seq.
      intros [k [H3 [_ H4] ]]. destruct b; try reflexivity.
      unfold alpha in H3.
      exfalso. destruct (k `mod` 2) eqn:Em.
      * cbn [Nat.eqb] in H3. eapply H2 in H3. cbn in H4. eauto.
        eapply Nat.div_le_upper_bound. lia. lia.
      * cbn [Nat.eqb] in H3. eapply Hle in H3. cbn in H4.
        rewrite Nat.mod_eq in Em; lia.
    + firstorder.
Qed.

Definition PFP := forall f : nat -> bool, exists g : nat -> bool, (forall n, f n = false) <-> exists n, g n = true.

Lemma WLPO_PFP_LLPO_iff :
  WLPO <-> PFP /\ LLPO.
Proof.
  split.
  - intros H. split.
    + intros f. destruct (H f).
      * exists (fun _ => true).
        split.
        -- now exists 0.
        -- eauto.
      * exists (fun _ => false).
        split.
        -- tauto.
        -- intros [? [=]].
    + eapply LLPO_split_to_LLPO, DM_Sigma_0_1_to_LLPO_split.
      intros f g Hfg.
      destruct (H f).
      * left. firstorder congruence.
      * destruct (H g).
        -- right. firstorder congruence.
        -- left. intros Hf.
           assert (H2 : ~~ ((exists n, g n = true) \/ ~ (exists n, g n = true))) by tauto.
           eapply H2. intros [Hg | Hg].
           now eapply Hfg. now rewrite <- forall_neg_exists_iff in Hg.
  - intros [PFP LLPO % LLPO_to_DM_Sigma_0_1] f.
    destruct (PFP f) as [g Hg].
    destruct (LLPO f g).
    + rewrite <- Hg. intros [[n Hn] H]. rewrite H in Hn. congruence.
    + left. now rewrite forall_neg_exists_iff.
    + right. now rewrite <- Hg in H.
Qed.

Definition KS := forall P, exists f : nat -> bool, P <-> exists n, f n = true.

Lemma LEM_to_KS :
  LEM -> KS.
Proof.
  intros xm P.
  destruct (xm P) as [H | H].
  - exists (fun _ => true). firstorder. econstructor.
  - exists (fun _ => false). firstorder congruence.
Qed.

Lemma KS_LPO_to_LEM :
  KS -> LPO -> LEM.
Proof.
  intros ks lpo P.
  destruct (ks P) as [f ->].
  eapply lpo.
Qed.

Lemma KS_WLPO_to_WLEM :
  KS -> LPO -> LEM.
Proof.
  intros ks lpo P.
  destruct (ks P) as [f ->].
  eapply lpo.
Qed.

Lemma KS_LLPO_to_DGP :
  KS -> LLPO -> DGP.
Proof.
  intros ks lpo P Q.
  destruct (ks P) as [f ->].
  destruct (ks Q) as [g ->].
  eapply lpo.
Qed.

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

Definition MP_semidecidable := forall X (p : X -> Prop), semi_decidable p -> forall x, ~~ p x -> p x.
Definition Post_logical := forall X (p : X -> Prop), semi_decidable p -> semi_decidable (compl p) -> forall x, p x \/ ~ p x.
Definition Post := forall X (p : X -> Prop), semi_decidable p -> semi_decidable (compl p) -> decidable p.

Lemma LPO_MP_WLPO_iff :
  LPO <-> MP /\ WLPO.
Proof.
  split.
  - intros H. split.
    + intros f Hf. destruct (H f); tauto.
    + intros f. rewrite forall_neg_exists_iff. destruct (H f); tauto.
  - intros [MP WLPO] f.
    destruct (WLPO f).
    + right. now rewrite <- forall_neg_exists_iff.
    + left. eapply MP. now rewrite <- forall_neg_exists_iff.
Qed.

Lemma MP_IP_LPO : IP -> MP -> LPO.
Proof.
  intros IP MP f.
  assert (exists n, forall k, f k = true -> f n = true) as [n Hn].
  - specialize (MP f). apply IP in MP as [n Hn].
    exists n. intros k H. apply Hn. intros H'. apply H'. now exists k.
  - destruct (f n) eqn:E.
    + eauto.
    + right. intros [m Hm].
      specialize (Hn m Hm). congruence.
Qed.

Lemma MP_to_MP_semidecidable :
  MP -> MP_semidecidable.
Proof.
  intros H X p [f Hf] x. red in Hf.
  rewrite Hf. eapply H.
Qed.

Definition MP_semidecidable_ex := forall (p : nat -> Prop), semi_decidable p -> ~~ (exists x, p x) -> exists x, p x.

Lemma MP_semidecidable_to_MP_semidecidable_ex :
  MP_semidecidable -> MP_semidecidable_ex.
Proof.
  intros mp p [f Hf]. red in Hf. setoid_rewrite Hf.
  eapply (mp unit (fun _ => exists x n, f x n = true)).
  exists (fun _ => fun! ⟨x,n⟩ => f x n). intros _.
  split.
  - intros (x & n & Hxn). exists ⟨x,n⟩. now rewrite embedP.
  - intros (xn & Hxn). destruct (unembed xn) as [x n]. eauto.
  - exact tt.
Qed.

Lemma MP_semidecidable_ex_to_MP_semidecidable :
  MP_semidecidable_ex -> MP_semidecidable.
Proof.
  intros mp X p [f Hf] x. red in Hf. setoid_rewrite Hf.
  eapply mp. eapply decidable_semi_decidable.
  exists (fun x0 => f x x0). intros ?. red. reflexivity.
Qed.

Lemma MP_semidecidable_nat_to_MP_semidecidable :
  (forall p : nat -> Prop, semi_decidable p -> forall x, ~~ p x -> p x) -> MP_semidecidable.
Proof.
  intros mp. eapply MP_semidecidable_ex_to_MP_semidecidable.
  intros p [f Hf]. red in Hf. setoid_rewrite Hf.
  eapply (mp (fun _ => exists x n, f x n = true)).
  exists (fun _ => fun! ⟨x,n⟩ => f x n). intros _.
  split.
  - intros (x & n & Hxn). exists ⟨x,n⟩. now rewrite embedP.
  - intros (xn & Hxn). destruct (unembed xn) as [x n]. eauto.
  - exact 0.
Qed.

Lemma MP_semidecidable_to_Post_logical :
  MP_semidecidable -> Post_logical.
Proof.
  intros H X p Hp Hcp x. pattern x.
  eapply H.
  - now eapply semi_decidable_or.
  - tauto.
Qed
.
Definition MP_semidecidable_ex_enumerable := forall X (p : X -> Prop), enumerable p -> ~~ (exists x, p x) -> exists x, p x.

Lemma MP_bla :
  MP_semidecidable_ex -> MP_semidecidable_ex_enumerable.
Proof.
  intros mp X p [f Hf]. red in Hf.
  setoid_rewrite Hf. intros H.
  destruct (mp (fun n => f n <> None)) as [n Hn].
  - eapply decidable_semi_decidable. eapply decidable_iff.
    econstructor. intros n. destruct (f n); firstorder.
  - intros HH. apply H. intros (x & n & HHH). eapply HH. exists n. congruence.
  - destruct (f n) eqn:E; try congruence. now exists x, n.
Qed.

Lemma MP_blub :
  MP_semidecidable_ex_enumerable -> MP_semidecidable_ex.
Proof.
  intros mp p Hp.
  eapply mp. eapply semi_decidable_enumerable; eauto.
Qed.

Lemma Post_logical_to_Post :
  Post_logical -> Post.
Proof.
  intros H X p Hp Hcp.
  destruct (sdec_compute_lor Hp Hcp) as [f Hf].
  - eapply H; eauto.
  - exists f. intros x. red. specialize (Hf x). destruct (f x); firstorder congruence.
Qed.

Lemma Post_nempty_to_MP {X} (x0 : X) :
  (forall (p : X -> Prop), semi_decidable p -> semi_decidable (compl p) -> decidable p) -> MP.
Proof.
  intros H f Hf.
  destruct (H (fun _ => exists n, f n = true)) as [d Hd].
  - exists (fun _ => f). now intros x.
  - exists (fun _ _ => false). firstorder congruence.
  - destruct (decider_decide Hd x0); tauto.
Qed.

Lemma Post_to_MP :
  Post -> MP.
Proof.
  intros H. apply (Post_nempty_to_MP tt). apply H.
Qed.

Lemma semi_decidable_ext {X} (p q : X -> Prop) :
  p ≡{X -> Prop} q -> semi_decidable p -> semi_decidable q.
Proof.
  intros H [f Hf]. exists f. intros x. cbv -[iff] in H.
  rewrite <- H. eapply Hf.
Qed.

Lemma MP_iff_sdec_weak_total :
  MP_semidecidable <-> (forall X (R : X -> bool -> Prop), semi_decidable (uncurry R) -> forall x, ~~ (exists b, R x b) -> exists b, R x b).
Proof.
  split.
  - intros H X R [f Hf] x Hx.
    eapply H with (x := x).
    eapply semi_decidable_ext.
    2: eapply (@semi_decidable_or _ (fun x => R x true) (fun x => R x false)).
    + clear. intros x. split. firstorder. intros [[] ?]; firstorder.
    + exists (fun x n => f (x, true) n). intros x0. red in Hf.
      now rewrite (Hf (x0, true)).
    + exists (fun x n => f (x, false) n). intros x0. red in Hf.
      now rewrite (Hf (x0, false)).
    + eassumption.
  - intros H X p [f Hf] x Hx.
    edestruct (H X (fun x b => p x)).
    + exists (fun '(x, b) n => f x n). intros (?, b). cbn. eapply Hf.
    + intros Hp. eapply Hx. intros Hpx. eapply Hp. exists true. eassumption.
    + eassumption.
Qed.

Lemma MP_cosdec_to_sdec :
  MP ->
  (forall X (p : X -> Prop), co_semi_decidable p -> semi_decidable (compl p)).
Proof.
  intros mp X p [f Hf]. exists f. unfold semi_decider, compl.
  intros x. red in Hf. rewrite Hf. rewrite forall_neg_exists_iff.
  split; eauto.
Qed.

Lemma MP_partial_to_MP {Part : partiality} X (x0 : X) :
  (forall x : part X, ~~ ter x -> ter x) -> MP.
Proof.
  intros mp f Hf.
  destruct (mp (bind (mu_tot f) (fun _ => ret x0))) as [? H].
  intros H. apply Hf. intros [n [m Hm] % mu_tot_ter].
  apply H. exists x0.
  eapply bind_hasvalue.
  exists m. split; eauto. eapply ret_hasvalue.
  eapply bind_hasvalue in H as (? & [] % mu_tot_hasvalue & ?).
  eauto.
Qed.

Lemma MP_to_MP_partial {Part : partiality} :
  MP -> (forall X, forall x : part X, ~~ ter x -> ter x).
Proof.
  intros MP X x.
  assert (ter x <-> exists n, (if seval x n is Some x then true else false) = true). {
    split.
    - intros [a [n H] % seval_hasvalue]. exists n. now rewrite H.
    - intros [n H]. destruct seval as [ a | ] eqn:E; try congruence.
      exists a. eapply seval_hasvalue. eauto.
  }
  rewrite H.
  eapply MP.
Qed.

Module assume_EA.

  Import Assume_EA. (* assumes EA as an axiom, i.e. a parametrically universal enumerator *)

  Lemma MP_iff_stable_W :
    MP <-> Definitions.stable (uncurry W).
  Proof.
    split.
    - intros mp. eapply MP_to_MP_semidecidable; eauto.
      eapply enumerable_semi_decidable. eauto.
      eapply enumerable_W.
    - intros mp. eapply Post_to_MP, Post_logical_to_Post, MP_semidecidable_to_Post_logical,
        MP_semidecidable_nat_to_MP_semidecidable.
      intros p H % enum_iff % m_complete_W.
      eapply red_m_transports_stable. eauto.
      eapply red_m_transitive; eauto. eapply W_uncurry_red.
  Qed.

  Lemma MP_iff_stable_K :
    MP <-> Definitions.stable K0.
  Proof.
    rewrite MP_iff_stable_W.
    split; intros; eapply red_m_transports_stable; eauto.
    - eapply K0_red.
    - eapply red_m_transitive. eapply W_uncurry_red'. eapply W_red_K0.
  Qed.

  Lemma MP_iff_every_stable_m_complete :
    MP <-> forall p : nat -> Prop, enumerable p -> m-complete p -> Definitions.stable p.
  Proof.
    rewrite MP_iff_stable_K. split.
    - intros H p He Hp. eapply red_m_transports_stable. exact H.
      eapply m_complete_K0; eauto.
    - intros H. eapply H. eapply K0_enum. eapply m_complete_K0.
  Qed.

  Lemma MP_iff_any_stable_m_complete :
    MP <-> exists p : nat -> Prop, enumerable p /\ m-complete p /\ Definitions.stable p.
  Proof.
    rewrite MP_iff_every_stable_m_complete. split.
    - intros H. exists K0. repeat split. 3: eapply H.
      all: eauto using m_complete_K0, K0_enum.
    - intros (p & He & Hm & Hp) q Heq Hmq.
      eapply red_m_transports_stable. exact Hp.
      eapply Hm; eauto.
  Qed.

End assume_EA.

Lemma DNE_sdec_to_cosdec :
  DNE ->
  (forall X (p : X -> Prop), semi_decidable (compl p) -> co_semi_decidable p).
Proof.
  intros mp X p [f Hf]. exists f. unfold semi_decider, compl in *.
  intros x. rewrite forall_neg_exists_iff. rewrite <- Hf.
  split; eauto. eapply mp.
Qed.

Require Import SyntheticComputability.Shared.FinitenessFacts.

Require Import SyntheticComputability.Shared.Dec.

Lemma semi_decidable_generative (p : nat -> Prop) :
  MP -> semi_decidable p ->
  ~ exhaustible p -> generative p.
Proof.
  intros mp % MP_to_MP_semidecidable % MP_semidecidable_to_MP_semidecidable_ex Hs Hl l.
  eapply mp.
  - eapply semi_decidable_and. eauto. eapply decidable_semi_decidable, decidable_complement, listable_decidable.
    eapply discrete_nat. exists l. red. reflexivity.
  - apply non_finite_spec; eauto. intros. destruct (Nat.eqb_spec x1 x2); firstorder.
Qed.

Lemma MP_non_finite_generative (p : nat -> Prop) :
  MP -> enumerable p ->
  ~ exhaustible p -> generative p.
Proof.
  intros.
  eapply semi_decidable_generative; eauto.
  eapply enum_iff; eauto.
Qed.

Definition AC_on X Y :=
  forall R : X -> Y -> Prop, (forall x, exists y, R x y) -> exists f : X -> Y, forall x, R x (f x).

Definition AC := forall X Y, AC_on X Y.

Definition UNIF_on X Y := forall R : X -> Y -> Prop,
  (forall x, exists y, R x y) -> exists R' : X -> Y -> Prop, (forall x y, R' x y -> R x y) /\ (forall x, exists! y, R' x y).

Definition AUC_on X Y :=
  forall R : X -> Y -> Prop, (forall x, exists! y, R x y) -> exists f : X -> Y, forall x, R x (f x).

Definition AC_0_0 :=
  AC_on nat nat.

Definition AC_1_0 :=
  AC_on (nat -> nat) nat.

Definition ADC_on X := forall R : X -> X -> Prop, forall x0, (forall x, exists x', R x x') -> exists f : nat -> X, f 0 = x0 /\ forall n, R (f n) (f (S n)).

Definition ADC := forall X, ADC_on X.
Definition ACC := forall X, AC_on nat X.

Lemma total_list {X Y} {R : X -> Y -> Prop} L :
  (forall x, exists y, R x y) -> exists L', Forall2 R L L'.
Proof.
  intros HTot. induction L as [ | x L [L' IH]].
  - exists []. econstructor.
  - destruct (HTot x) as [y H]. exists (y :: L').
    now econstructor.
Qed.

Lemma AC_rel_to_ADC : forall X, AC_on X X -> ADC_on X.
Proof.
  intros X C R x0 Htot.
  eapply C in Htot as [f].
  exists (fun n => Nat.iter n f x0).
  split. reflexivity. intros n. eapply H.
Qed.

Lemma AC_on_to_AUC_on : forall X Y, AC_on X Y -> AUC_on X Y.
Proof.
  intros X Y C R H. eapply C. firstorder.
Qed.

Goal AC -> ADC.
Proof.
  intros ? X Inh.
  eapply AC_rel_to_ADC, H.
Qed.

Goal ADC -> ACC.
Proof.
  intros C X R Htot.
  destruct (Htot 0) as [y0 Hy0].
  unshelve specialize (C (∑ '(n, x), R n x) (fun '(exist _ (n, x) H) '(exist _ (m, y) H2) => m = S n)) as [f].
  - eexists (_, _). eauto.
  - intros [(n, x) H]. destruct (Htot (S n)) as [y Hy]. now exists (exist _ (S n, y) Hy).
  - destruct H as [H0 H].
    pose (N n := fst (proj1_sig (f n))).
    pose (s n := snd (proj1_sig (f n))).
    assert (HN : forall n, N (S n) = S (N n)). {
      intros n. cbv.
      pose proof (H (S n)) as Hsn.
      pose proof (H n) as Hn.
      destruct (f n) as [(m', y') H'].
      destruct (f (S n)) as [(m, y) Hmy]. eassumption.
    }
    assert (HN0 : forall n, N n = N 0 + n) by (induction n; rewrite ?HN; lia).
    assert (H1 : forall n, R (N n) (s n)). {
      intros n. unfold N, s.
      specialize (H n).
      destruct (f n) as [(m, y) Hmy]. exact Hmy.
    }
    pose proof (total_list (seq 0 (N 0)) Htot) as [L' HL'].
    exists (fun n => if le_lt_dec (N 0) n is left _ then s (n - N 0) else (nth n L' (s 0))). intros n.
    destruct (le_lt_dec (N 0) n) as [Hl | Hl].
    + specialize (H1 (n - N 0)). rewrite HN0 in H1.
      now replace n with (N 0 + (n - N 0)) at 1 by lia.
    + rewrite nth_lookup.
      destruct (L' !! n) as [x|] eqn:E.
      * cbn.
        edestruct (Forall2_lookup_l R (seq 0 (N 0)) L') as [? []]. eassumption.
        rewrite lookup_seq; eauto.
        rewrite E in H2. inv H2. eassumption.
      * eapply lookup_ge_None in E. erewrite <- Forall2_length in E; eauto.
        rewrite seq_length in E. lia.
Qed.

Goal ACC -> AC_0_0.
Proof.
  unfold ACC, AC_0_0.
  intros H. eapply H.
Qed.

Lemma AC_1_0_to_AC_0_0 : AC_1_0 -> AC_0_0.
Proof.
  intros C R Htot.
  destruct (C (fun g x => R (g 0) x)) as [f].
  - intros g. eapply Htot.
  - exists (fun x => f (fun _ => x)).
    intros x. eapply (H (fun _ => x)).
Qed.

Lemma AC_0_0_to_AC_nat_bool : AC_0_0 -> AC_on nat bool.
Proof.
  intros C R Htot.
  destruct (C (fun n m => R n (Nat.eqb m 0))) as [f].
  - intros x. destruct (Htot x) as [ [] ].
    + exists 0. firstorder.
    + exists 1. firstorder.
  - eexists. eapply H.
Qed.

Lemma UNIFx_char X Y :
  AC_on X Y <-> AUC_on X Y /\ UNIF_on X Y.
Proof.
  split. 1: intros C; split.
  - intros R Htot. edestruct (C R) as [f Hf]; firstorder.
  - intros R [f Hf] % C. exists (fun x y => f x = y). now firstorder subst.
  - intros [C1 C2] R Htot.
    specialize (C2 _ Htot) as (R' & H1 & H2).
    destruct (C1 _ H2) as [f Hf]. eauto.
Qed.

Lemma Diaconescu :
  (forall X Y, AC_on X Y) -> Fext -> Pext -> LEM.
Proof.
  intros C fext pext P.
  pose (U (x : bool) := x = true \/ P).
  pose (V (x : bool) := x = false \/ P).
  destruct (C ({ p : bool -> Prop | p = U \/ p = V}) bool (fun p b => (proj1_sig p b))) as [f Hf].
  - intros (p & [-> | ->]); cbn.
    + exists true. now left.
    + exists false. now left.
  - pose proof (Hf (exist _ U (or_introl eq_refl))) as H1.
    pose proof (Hf (exist _ V (or_intror eq_refl))) as H2. cbn in *.
    assert (f (exist _ U (or_introl eq_refl)) <> f (exist _ V (or_intror eq_refl)) \/ P) as [H3 | H3]; eauto.
    {
      destruct H1 as [H1 | H1], H2 as [H2 | H2]; eauto.
      firstorder congruence.
    }
    right. intros H.
    assert (U = V) as ->. {
      eapply fext. intros b. eapply pext.
      unfold U, V. intuition.
    }
    eapply H3. repeat f_equal.
    eapply (Pext_to_PI pext).
Qed.

(* *** Compatibility  *)
(* 
Lemma AC_1_0_Fext :
  AC_1_0 -> Fext -> EA -> decidable (compl K_nat_nat).
Proof.
  intros C Fext EA.
  pose proof (fun f => enumerable_code EA _ (enumerable_graph' f)).
  eapply C in H as code Hcode.
  exists (fun f => Nat.eqb (code f) (code (fun _ => 0))).
  eapply Proper_decider. intros ?. reflexivity.
  eapply (K_nat_equiv).
  intros f. split; rewrite NPeano.Nat.eqb_eq.
  - intros E.
    eapply f_equal, Fext, E.
  - intros E n.
    generalize (Hcode f), (Hcode (fun _ => 0)).
    rewrite E. clear E.
    intros Hf H.
    pose proof(enumerator_ext Hf H (ltac:(reflexivity)) ⟨ n, f n ⟩) as E.
    destruct E as [x E%(f_equal unembed)] _; eauto.
    rewrite !embedP in E. now inv E.
Qed. *)

Lemma AUC_to_dec (p : nat -> Prop) :
  AUC_on nat bool -> (forall n, p n \/ ~ p n) -> decidable p.
Proof.
  intros C Hp.
  destruct (C (fun n b => (p n /\ b = true) \/ (~ p n /\ b = false))) as [f Hf].
  - intros n. destruct (Hp n) as [H | H].
    + exists true. split. left. eauto. intros []; firstorder congruence. congruence.
    + exists false. split. right. eauto. intros []; firstorder congruence. congruence.
  - exists f. intros n. destruct (Hf n) as [[H ->] | [H ->]]; firstorder congruence. congruence.
Qed.

Lemma AC_0_0_LPO_incompat' {Part : partiality} :
  AUC_on nat bool -> WLPO -> EPF_bool -> forall p : nat -> Prop,
    semi_decidable p -> decidable (compl p).
Proof.
  intros C LPO % WLPO_semidecidable_iff EPF p Hp.
  eapply AUC_to_dec; eauto.
Qed.

Lemma AC_0_0_LPO_incompat {Part : partiality} :
  AUC_on nat bool -> WLPO -> EPF_bool -> False.
Proof.
  intros C LPO EPF_bool.
  destruct (EPF_SCT_halting) as (K & H1 & H2 & H3 & H4); [eauto|].
  eapply H4. eapply AC_0_0_LPO_incompat'; eauto.
Qed.

Lemma AC_1_0_Fext_CODING :
  AC_1_0 -> Fext -> SCT -> CODING.
Proof.
  intros C Fext (ϕ & Hmono & Hϕ).
  assert (forall f : nat -> nat, exists c, forall x, exists n, ϕ c x n = Some (f x)) as [F HF] % C. {
    intros f. destruct (Hϕ (fun _ => f)) as [c Hc].
    eexists. eapply (Hc 0).
  }
  exists (fun (f : nat -> bool) => F (fun x : nat => if f x then 0 else 1)).
  intros f. split.
  + intros H x.
    pose proof (HF (λ _ : nat, 1) x) as [n1 Hn1]. rewrite <- H in Hn1.
    pose proof (HF (λ x : nat, if f x then 0 else 1) x) as [n2 Hn2].
    eapply monotonic_agnostic in Hn1. 2: eapply Hmono.
    eapply Hn1 in Hn2. destruct (f x); congruence.
  + intros H2. f_equal. eapply Fext. intros x. rewrite H2. reflexivity.
Qed.

Lemma AC_1_0_Fext_incompat {Part : partiality} :
  AC_1_0 -> Fext -> SCT -> False.
Proof.
  intros C funext ct.
  eapply K_nat_bool_undec; [ eauto | ].
  now eapply no_CODING, AC_1_0_Fext_CODING.
Qed.