Require Import CantorPairing.
Require Import Lia.

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

Definition dec (P : Prop) := {P} + {~P}.
Definition Dec {X} p := forall x : X, dec(p x).

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

Lemma eq_dec_nat (x y : nat) : dec (x = y).
Proof.
  unfold dec. decide equality.
Defined.

Lemma lt_dec x y : dec (x < y).
Proof.
  induction y in x |-*.
  - right. lia.
  - destruct x.
    left. lia.
    destruct (IHy x).
    left; lia. right; lia.
Qed.

Lemma dec_conj A B : dec A -> dec B -> dec (A /\ B).
Proof.
  intros [] []; unfold dec; intuition.
Defined.

Lemma dec_disj A B : dec A -> dec B -> dec (A \/ B).
Proof.
  intros [] []; unfold dec; intuition.
Defined.

Lemma dec_imp A B : dec A -> dec B -> dec (A -> B).
Proof.
  intros [] []; unfold dec; intuition.
Defined.

Lemma dec_neg A : dec A -> dec (~ A).
Proof.
  intros []; unfold dec; now (left + right).
Defined.

Lemma neg_and A B : dec A -> dec B -> ~(A /\ B) -> (~A \/ ~B).
Proof.
  intros [] [] ?; tauto.
Defined.

Lemma neg_imp A B : dec A -> dec B -> ~(A -> B) -> A /\ ~B.
Proof.
  intros [][]?; tauto.
Qed.

Hint Resolve neg_and neg_imp eq_dec_nat dec_conj dec_disj dec_imp dec_neg : decs.

Lemma dec_lt_bounded_sig N (p : nat -> Type) :
  (forall x, p x + (p x -> False)) -> { x & ((x < N) * p x)%type } + (forall x, x < N -> p x -> False).
Proof.
  intros Dec_p. induction N.
  right. intros []; lia.
  destruct (IHN) as [IH | IH].
  - left. destruct IH as [x Hx].
    exists x. split. destruct Hx. lia. apply Hx.
  - destruct (Dec_p N) as [HN | HN].
    + left. exists N. split. lia. apply HN.
    + right. intros x Hx.
      assert (x = N \/ x < N) as [->|] by lia; auto.
      now apply IH.
Defined.

Lemma dec_lt_bounded_exist' N p :
  Dec p -> (exists x, x < N /\ p x) + (forall x, x < N -> ~ p x).
Proof.
  intros Dec_p. induction N.
  right. intros []; lia.
  destruct (IHN) as [IH | IH].
  - left. destruct IH as [x Hx].
    exists x. split. lia. apply Hx.
  - destruct (Dec_p N) as [HN | HN].
    + left. exists N. split. lia. apply HN.
    + right. intros x Hx.
      assert (x = N \/ x < N) as [->|] by lia; auto.
Defined.

Lemma dec_lt_bounded_exist N p :
  Dec p -> dec (exists x, x < N /\ p x).
Proof.
  intros Dec_p.
  destruct (dec_lt_bounded_exist' N p Dec_p).
  now left. right. firstorder.
Defined.

Lemma dec_lt_bounded_forall N p :
  Dec p -> dec (forall x, x < N -> p x).
Proof.
  intros Dec_p. induction N.
  left. lia.
  destruct (Dec_p N) as [HN | HN].
  - destruct (IHN) as [IH | IH].
    + left. intros x Hx.
    assert (x = N \/ x < N) as [->|] by lia; auto.
    + right. intros H. apply IH.
      intros x Hx. apply H. lia.
  - right. intros H. apply HN.
    apply H. lia.
Defined.

Lemma neg_lt_bounded_forall N p : Dec p -> (~ forall x, x < N -> p x) -> exists x, x < N /\ ~ p x.
Proof.
  intros Hp H.
  induction N. exfalso. apply H; lia.
  destruct (Hp N).
  - destruct IHN as [n ].
    + intros H1. apply H. intros.
      assert (x = N \/ x < N) as [->|] by lia.
      auto. now apply H1.
    + exists n. intuition lia.
  - exists N. auto.
Qed.

Section WitnessOperator.

  Variable q : nat -> Prop.
  Variable Dec_q : Dec q.

  Inductive T n : Prop :=
    C : (~ q n -> T (S n)) -> T n.

  Lemma grounded n : T n -> T 0.
  Proof.
    induction n; auto.
    intros. apply IHn. now constructor.
  Defined.

  Lemma qT n : q n -> T n.
  Proof.
    intros. now constructor.
  Defined.

  Lemma preWitness : forall n, T n -> {x & q x}.
  Proof.
    apply T_rect.
    intros n _ H. destruct (Dec_q n).
    now exists n. now apply H.
  Defined.

  Theorem Witness : (exists x, q x) -> {x & q x}.
  Proof.
    intros H. apply (preWitness 0).
    destruct H as [n H]. destruct (Dec_q n).
    - eapply grounded, qT, H.
    - tauto.
  Defined.

End WitnessOperator.

Theorem ProductWO (p : nat -> nat -> Prop) : ( forall x y, dec (p x y) ) -> (exists x y, p x y) -> { x & { y & p x y }}.
Proof.
  intros Dec_p H.
  pose (P n := let (x, y) := decode n in p x y).
  assert ({n & P n}) as [n Hn].
  apply Witness.
  - intros n.
    destruct (decode n) as [x y] eqn:E.
    destruct (Dec_p x y); (left + right); unfold P; now rewrite E.
  - destruct H as (x & y & H).
    exists (code (x, y)). unfold P.
    now rewrite inv_dc.
  - destruct (decode n) as [x y] eqn:E.
    exists x, y. unfold P in Hn; now rewrite E in Hn.
Qed.