Require Import Setoid.
Require Import ConstructiveEpsilon.
From Undecidability.Synthetic Require Export DecidabilityFacts.
From Undecidability.Shared Require Export Dec.

Definition iffT (X Y : Type) : Type := (X -> Y ) * (Y -> X ).
Notation "X <=> Y" := (iffT X Y) (at level 95, no associativity).

Definition surj {X Y} (f : X -> Y) := forall y, exists x , f x = y.
Definition inj {X Y} (f : X -> Y) := forall x x', f x = f x' -> x = x'.
Definition bij {X Y} (f : X -> Y) := inj f /\ surj f.

Basic logical notions.

Definition definite P := P \/ ~P.
Definition Definite {X} p := forall x : X, definite (p x).
Definition LEM := forall P, definite P.
Definition stable P := ~~P -> P.
Definition Stable {X} p := forall x : X, stable (p x).
Definition DNE := forall P, stable P.
Definition MP := forall (f : nat -> nat), stable (exists n , f n = 0).
Definition UC X Y := forall R, (forall x:X, exists ! y:Y , R x y ) -> exists f , forall x, R x (f x).

Fact LEM_DNE :
  (LEM <-> DNE ) /\ (DNE -> MP ).
Proof.
  unfold LEM, DNE, MP. repeat split.
  - intros lem p. now destruct (lem p).
  - intros dne p. apply dne. unfold definite; tauto.
  - intros dne f. apply dne.
Qed.

Fact DN_remove {A B} :
  ~~A -> (A -> ~B ) -> ~B.
Proof. tauto. Qed.

Fact DN_chaining {A B : Prop} :
  ~ ~ A -> ~ ~(A -> B ) -> ~ ~ B.
Proof. tauto. Qed.

Fact DN {A : Prop} :
  A -> ~~A.
Proof. tauto. Qed.

Fact NNN_N A :
  ~~~A <-> ~A.
Proof. tauto. Qed.

Fact DN_forall_stable {X} p :
  Stable p -> (forall x : X, ~~p x ) -> forall x, p x.
Proof. unfold Stable; firstorder. Qed.

Definitions in synthetic computability.

The below definitions are chosen to be as convienient as possible for synthetic computability proofs. They may in some cases differ from the definition that is stated in the paper, since these have been choosen such that they are closest to intuition. Both definitions are however always equivalent, and the equivalence proofs can be found further down in this file.

Definition decider {X} p f := forall x : X, p x <-> f x = true.
Definition dec (P : Prop) := {P } + {~P }.
Definition Dec {X} p := inhabited(forall x : X, {p x } + {~p x }).
Definition Dec_sigT {X} p := forall x : X, {p x } + {~p x }.
Definition witnessing {X} (p : X -> Prop) := ex p -> sigT p.
Definition enumerable {X} p := exists f : nat -> option X , forall x, p x <-> exists n , f n = Some x.

Definition Enumerable X := exists f : nat -> option X , forall x, exists n , f n = Some x.
Definition Discrete X := Dec (fun p : X * X => fst p = snd p).
Definition Separated X := Dec (fun p : X * X => fst p <> snd p).
Definition Markov X := forall p : X -> Prop, Dec p -> (~~ ex p ) -> ex p.
Definition Witnessing X := forall p : X -> Prop, Dec_sigT p -> witnessing p.

Equivalent characterizations

Fact Dec_decider {X} p :
  Dec p <-> ex (@decider X p).
Proof.
  split.
  - intros [D].
    exists (fun x => if D x then true else false).
    intros x. destruct (D x); cbn; intuition congruence.
  - intros [f decf]. constructor. intros x.
    specialize (decf x).
    destruct (f x) eqn:Hx; [left; tauto|right].
    now intros ?%decf.
Qed.

Fact Dec_transport {X} p q :
  Dec p -> (forall x : X, p x <-> q x ) -> Dec q.
Proof.
intros [Dec_p] Equiv. constructor. intros x.
destruct (Dec_p x) as [H|H];
[left | right]; firstorder.
Qed.

Fact Dec_decider_nat p :
  Dec p -> exists f : nat -> nat , forall x : nat, p x <-> f x = 0.
Proof.
  intros [f decf]%Dec_decider.
  exists (fun n => if f n then 0 else 1).
  intros x. specialize (decf x).
  destruct (f x) eqn:Hx; try tauto.
  rewrite decf. split; congruence.
Qed.

Fact Dec_sigT_decider {X} p :
  Dec_sigT p <=> sigT (@decider X p).
Proof.
  split.
  - intros D.
    exists (fun x => if D x then true else false).
    intros x. destruct (D x); cbn; intuition congruence.
  - intros [f decf]. intros x.
    specialize (decf x).
    destruct (f x) eqn:Hx; [left; tauto|right].
    now intros ?%decf.
Qed.

Fact dec_Dec_sig_T P :
  dec P <=> Dec_sigT (fun _ : True => P).
Proof.
  split.
  - intros []; now constructor.
  - intros []; unfold dec; tauto.
Qed.

Lemma DN_Dec_equiv X (p : X -> Prop) :
  ~ ~ Dec p <-> ((Dec_sigT p -> False ) -> False ).
Proof.
  split.
  - intros nnH. apply (DN_remove nnH).
    intros [H]. intros nH. apply nH.
    intros x. apply H.
  - intros nnH nH. apply nnH. intros H.
    apply nH. constructor. apply H.
Qed.

Lemma Dec_equivalent_predicates {X} {p P: X -> Prop} :
  (forall x, P x <-> p x ) -> Dec P -> Dec p.
Proof.
  intros H [Dec_P].
  constructor. intros x.
  destruct (Dec_P x); specialize (H x);
    (left; tauto) || right; tauto.
Qed.

Lemma Witnessing_equiv X :
  Witnessing X <=>
  forall (f : X -> bool), (exists x , f x = true ) -> {x & f x = true }.
Proof.
  split; intros H.
  - intros f. apply H.
    intros x. decide equality.
  - intros p [f Hf]%Dec_sigT_decider Ex.
    unfold decider in *.
    destruct (H f).
    + destruct Ex as [x Hx]. exists x. now apply Hf.
    + exists x. now apply Hf.
Qed.

Fact Discrete_equiv {X} :
  Discrete X <-> ex (@decider (X * X) (fun '(x , y ) => x = y)).
Proof.
  unfold Discrete. rewrite Dec_decider.
  split; intros [f Hf]; exists f; intros [x y]; apply (Hf (x,y)).
Qed.

Fact Discrete_sum {X} :
  Discrete X <-> inhabited(forall x y : X, {x = y } + {~ x = y }).
Proof.
  split; intros [H]; constructor.
  - intros x y. destruct (H (x,y)); cbn in *; tauto.
  - intros [x y]; cbn. destruct (H x y); tauto.
Qed.

Fact Separated_equiv {X} :
  Separated X <-> ex (@decider (X * X) (fun '(x , y ) => x <> y)).
Proof.
  unfold Separated. rewrite Dec_decider.
  split; intros [f Hf]; exists f; intros [x y]; apply (Hf (x,y)).
Qed.

Fact Separated_sum {X} :
  Separated X <-> inhabited(forall x y : X, {~ x = y } + {~~ x = y }).
Proof.
  split; intros [H]; constructor.
  - intros x y. destruct (H (x,y)); cbn in *; tauto.
  - intros [x y]; cbn. destruct (H x y); tauto.
Qed.

Fact enumerable_nat p :
  enumerable p ->
  exists f , forall x : nat, p x <-> exists n : nat , f n = S x.
Proof.
  intros [f Hf].
  exists (fun n => match f n with Some x => S x | _ => 0 end).
  intros x. rewrite Hf. split; intros [n Hn]; exists n.
  - now rewrite Hn.
  - destruct (f n); congruence.
Qed.

Fact enumerable_equiv X :
  Enumerable X <-> enumerable (fun x : X => True).
Proof.
  split; intros [g Hg]; exists g; firstorder.
Qed.

Fact enumerable_surjection {X} :
  X -> Enumerable X -> exists f : nat -> X , surj f.
Proof.
  intros x0 [g Hg].
  exists (fun n => match g n with Some x => x | None => x0 end).
  intros x. specialize (Hg x) as [n Hn].
  exists n. now rewrite Hn.
Qed.

Fact MP_Markov_nat :
  MP <-> Markov nat.
Proof.
  split.
  - intros mp p [Dec_p] nnH.
    specialize (mp (fun x => if Dec_p x then 0 else 1)).
    destruct mp as [n Hn].
    + apply (DN_chaining nnH), DN.
      intros [n Hn]. exists n.
      destruct (Dec_p n) eqn:fn; congruence.
    + exists n. destruct (Dec_p n) eqn:?; congruence.
  - intros markov f.
    refine (markov (fun n => f n = 0) _).
    constructor; intros ?.
    decide equality.
Qed.

Lemma UC_Def_Dec X (p : X -> Prop) :
  UC X bool -> Definite p -> Dec p.
Proof.
  intros uc Def. apply Dec_decider.
  refine (uc (fun x y => p x <-> y = true) _).
  intros n. destruct (Def n) as [h|h].
  - exists true; split; [tauto|].
    intros []; try congruence.
    intros H. now rewrite H in h.
  - exists false; split.
    + split; try tauto; congruence.
    + intros []; try congruence.
    intros H. now rewrite H in h.
Qed.

Fact MP_Dec_stable :
  MP -> forall (p : nat -> Prop), Dec p -> stable (ex p).
Proof.
  intros mp p [f Hf]%Dec_decider nnH.
  destruct (mp (fun n => if f n then 0 else 1)) as [y Hy].
  - apply (DN_chaining nnH), DN. intros [y Hy].
    exists y. apply Hf in Hy. now destruct (f y).
  - exists y. apply Hf. now destruct (f y).
Qed.

Fact forall__neg_exists_neg X (p : X -> Prop) :
  (forall x, p x ) -> ~ exists x , ~ p x.
Proof. firstorder. Qed.

Fact Stable_neg_exists_neg__forall {X} (p : X -> Prop) :
  Stable p -> (~ exists x , ~ p x ) -> forall x, p x.
Proof. firstorder. Qed.