From SyntheticComputability Require Import ArithmeticalHierarchySemantic reductions SemiDec TuringJump OracleComputability Definitions Limit simple.
From stdpp Require Export list.
Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
Require Export SyntheticComputability.Shared.FinitenessFacts.
Require Export SyntheticComputability.Shared.Pigeonhole.
Require Export SyntheticComputability.Shared.ListAutomation.
Require Import Arith Arith.Compare_dec Lia Coq.Program.Equality List.
Import ListNotations.

Notation "'Σ' x .. y , p" :=
    (sigT ( x .. (sigT ( y p)) ..))
        (at level 200, x binder, right associativity,
        format "'[' 'Σ' '/ ' x .. y , '/ ' p ']'")
    : type_scope.

Notation unique p := ( x x', p x p x' x = x').

  Class Extension :=
  {
      extendP: list Prop;
      extend_dec: l x, (Σ y, extendP l x y) + ( y, extendP l x y);
      extend_uni: l x, unique (extendP l x)
  }.

  Inductive F_ (E: Extension) : list Prop :=
    | Base : F_ E O []
    | ExtendS n l a : F_ E n l extendP l n a F_ E (S n) (a::l)
    | ExtendN n l : F_ E n l ( a, extendP l n a) F_ E (S n) l.

Section Construction.

  Variable E: Extension.

  Lemma F_uni n: unique (F_ E n).
  Proof.
    intros .
    dependent induction n.
    - intros . inv . now inv .
    - intros . inv ; inv .
      assert(l = ) as by now apply IHn.
      f_equal. apply (extend_uni ).
      assert (l = ) as by now apply IHn.
      exfalso. apply ( a ).
      assert (l = ) as by now apply IHn.
      exfalso. apply ( a ).
      now apply IHn.
  Qed.


  Lemma F_mono n m l1 l2: F_ E n F_ E m n m incl .
  Proof.
      intros HE.
      revert ; induction HE in |-*; intros .
      - now assert ( = ) as by (eapply F_uni; eauto).
      - inv ; last now apply IHHE.
        specialize (IHHE l ). eauto.
  Qed.


  Lemma F_pop n x l: F_ E n (x::l) m, F_ E m l.
  Proof.
    intros H. dependent induction H.
    - now exists n.
    - eapply IHF_. eauto.
  Qed.


  Lemma F_pick n x l: F_ E n (x::l) m, F_ E m l extendP l m x.
  Proof.
    intros H. dependent induction H.
    - exists n; eauto.
    - eapply IHF_; eauto.
  Qed.


  Lemma F_pick' n x l: F_ E n (x::l) m, m < n F_ E m l extendP l m x.
    Proof.
      intros H. dependent induction H.
      - exists n; eauto.
      - destruct (IHF_ x l eq_refl) as [m (&&)].
        exists m; eauto.
    Qed.


  Lemma F_computable : Σ f: list ,
     n, F_ E n (f n) length (f n) n.
  Proof.
    set (F := fix f x :=
           match x with
           | O []
           | S x match extend_dec (f x) x with
                   | inr _ f x
                   | inl aH ( aH) :: (f x)
                   end
           end).
    exists F. induction n; simpl.
    - split. constructor. easy.
    - destruct (extend_dec (F n) n); split.
      + eapply ExtendS; first apply IHn. now destruct s.
      + cbn. destruct IHn. .
      + now eapply ExtendN.
      + destruct IHn. .
  Qed.


  Definition F_func := F_computable.
  Lemma F_func_correctness: n, F_ E n (F_func n).
  Proof.
    intros n; unfold F_func.
    destruct F_computable as [f H].
    now destruct (H n).
  Qed.


  Lemma F_func_correctness': n, length (F_func n) n.
  Proof.
    intros n; unfold F_func.
    destruct F_computable as [f H].
    now destruct (H n).
  Qed.


  Definition F_with x := l n, In x l (F_ E n l).

  Lemma F_func_F_with x: F_with x n, In x (F_func n).
  Proof.
    split. intros (l&n&&).
    exists n. assert (l = F_func n) as .
    { eapply F_uni. apply . apply F_func_correctness. }
    done. intros [n Hn]. exists (F_func n), n; split; first done.
    apply F_func_correctness.
  Qed.


  Lemma F_with_semi_decidable: semi_decidable F_with.
  Proof.
    unfold semi_decidable, semi_decider.
    destruct F_computable as [f Hf ].
    exists ( x n (Dec (In x (f n)))).
    intros x. split.
    - intros (l & n & Hxl & Hl).
      exists n. rewrite Dec_auto; first easy.
      destruct (Hf n) as [Hf' _].
      now rewrite (F_uni Hf' Hl).
    - intros (n & Hn%Dec_true).
      exists (f n), n; split; eauto.
      apply Hf.
  Qed.


  Lemma F_with_top x: F_with x l n, (F_ E n l) (F_ E (S n) (x::l)) extendP l n x.
  Proof.
    split; last first.
    { intros (l&n&&&). exists (x::l), (S n). eauto. }
    intros [l [n [Hln Hn]]].
    induction Hn. inversion Hln.
    - destruct (Dec (x=a)) as [|Ex].
      exists l, n; split; first easy. split.
      econstructor; easy. easy.
      eapply IHHn. destruct Hln; congruence.
    - now eapply IHHn.
  Qed.


  Lemma F_with_semi_decider: Σ f, semi_decider f F_with.
  Proof.
    destruct F_computable as [f Hf ].
    exists ( x n (Dec (In x (f n)))).
    intros x. split.
    - intros (l & n & Hxl & Hl).
      exists n. rewrite Dec_auto; first easy.
      destruct (Hf n) as [Hf' _].
      now rewrite (F_uni Hf' Hl).
    - intros (n & Hn%Dec_true).
      exists (f n), n; split; eauto.
      apply Hf.
  Qed.


  Definition χ n x: bool := Dec (In x (F_func n)).
  Definition stable {Q} (f: Q bool) :=
     q n m, n m f n q = true f m q = true.
  Definition stable_semi_decider {Q} P (f: Q bool) :=
    semi_decider (λ x n, f n x) P stable f.

  Lemma F_with_χ : stable_semi_decider F_with χ.
  Proof.
    split. split.
    - intros [n Hn]%F_func_F_with. by exists n; apply Dec_auto.
    - intros [n Hn%Dec_true]. rewrite F_func_F_with. by exists n.
    - intros x n m Hn Hm%Dec_true.
      apply Dec_auto. enough (incl (F_func n) (F_func m)). eauto.
      eapply F_mono; last exact Hn; apply F_func_correctness.
  Qed.


End Construction.

Section StrongInduction.

  Definition strong_induction (p: Type) :
    ( x, ( y, y < x p y) p x) x, p x.
  Proof.
      intros H x; apply H.
      induction x; [intros; | ].
      intros; apply H; intros; apply IHx; .
  Defined.


End StrongInduction.

Tactic Notation "strong" "induction" ident(n) := induction n using strong_induction.

Section EWO.
  Variable p: Prop.
  Inductive T | (n: ) : Prop := C (phi: p n T (S n)).

  Definition T_elim (q: Type)
    : ( n, (p n q (S n)) q n)
       n, T n q n
    := e fix f n a :=
      let (phi) := a in
      e n ( h f (S n) ( h)).

  (*** EWO for Numbers *)

  Lemma TI n :
    p n T n.
  Proof.
    intros H. constructor. intros . destruct ( H).
  Qed.


  Lemma TD n :
    T (S n) T n.
  Proof.
    intros H. constructor. intros _. exact H.
  Qed.


  Variable p_dec: n, dec (p n).

  Definition TE (q: Type)
    : ( n, p n q n)
      ( n, p n q (S n) q n)
       n, T n q n.
  Proof.
    intros .
    apply T_elim. intros n IH.
    destruct (p_dec n); auto.
  Qed.


From now on T will only be used through TI, TD, and TE


  Lemma T_zero n :
    T n T 0.
  Proof.
    induction n as [|n IH].
    - auto.
    - intros H. apply IH. apply TD, H.
  Qed.


  Definition ewo_nat :
    ex p Σ x, p x.
  Proof.
    intros H.
    refine (@TE ( _ Σ x, p x) _ _ 0 _).
    - eauto.
    - easy.
    - destruct H as [n H]. apply (@T_zero n), TI, H.
  Qed.


End EWO.

Section LeastWitness.

  Definition safe p n := k, k < n p k.
  Definition least p n := p n safe p n.

  Fact least_unique p : unique (least p).
  Proof.
    intros n n' [ ] [ ].
    enough (~(n < n') ~(n' < n)) by .
    split; intros H.
    - eapply ; eassumption.
    - eapply ; eassumption.
  Qed.


  Fact safe_O p :
    safe p 0.
  Proof.
    hnf. .
  Qed.


  Fact safe_S p n :
    safe p n p n safe p (S n).
  Proof.
    intros k . unfold safe in *.
    assert (k < n k = n) as [H|H] by .
    - auto.
    - congruence.
  Qed.


  Fact safe_char p n :
    safe p n k, p k k n.
  Proof.
    split.
    - intros H k .
      enough (k < n False) by .
      intros . apply H in . auto.
    - intros H k . apply H in . .
  Qed.


  Fact safe_char_S p n :
    safe p (S n) safe p n p n.
  Proof.
    split.
    - intros H. split.
      + intros k . apply H. .
      + apply H. .
    - intros [ ]. apply safe_S; assumption.
  Qed.


  Fact safe_eq p n k :
    safe p n k n p k k = n.
  Proof.
    intros . unfold safe in *.
    enough (~(k < n)) by .
    specialize ( k). tauto.
  Qed.


  Fact E14 x y z :
    x - y = z least ( k x y + k) z.
  Proof.
    assert (H: least ( k x y + k) (x - y)).
    { split; unfold safe; . }
    split. congruence.
    eapply least_unique, H.
  Qed.


  (*** Certifying LWOs *)

  Section LWO.
    Variable p : Prop.
    Variable p_dec : x, dec (p x).

    Definition lwo :
       n, (Σ k, k < n least p k) + safe p n.
    Proof.
      induction n as [|n IH].
      - right. apply safe_O.
      - destruct IH as [[k ]|].
        + left. exists k. destruct as [ ]. split. . exact .
        + destruct (p_dec n).
          * left. exists n. split. . easy.
          * right. apply safe_S; assumption.
    Defined.


    Definition lwo' :
       n, (Σ k, k n least p k) + safe p (S n).
    Proof.
      intros n.
      destruct (lwo (S n)) as [(k&&)|H].
      - left. exists k. split. . exact .
      - right. exact H.
    Qed.


    Definition least_sig :
      (Σ x, p x) Σ x, (least p) x.
    Proof.
      intros [n H].
      destruct (lwo (S n)) as [(k&&)|].
      - exists k. exact .
      - exfalso. apply ( n). . exact H.
    Qed.


    Definition least_ex :
      ex p ex (least p).
    Proof.
      intros [n H].
      destruct (lwo (S n)) as [(k&&)|].
      - exists k. exact .
      - exfalso. apply ( n). . exact H.
    Qed.


    Definition safe_dec n :
      dec (safe p n).
    Proof.
      destruct (lwo n) as [[k ]|].
      - right. intros H. exfalso.
        destruct as [ ]. apply (H k). exact . apply .
      - left. exact .
    Defined.


    Definition least_dec n :
      dec (least p n).
    Proof.
      unfold least.
      destruct (p_dec n) as [H|H].
      2:{ right. tauto. }
      destruct (safe_dec n) as [|].
      - left. easy.
      - right. tauto.
    Qed.

  End LWO.

  Lemma exists_bounded_dec' P:
  ( x, dec (P x)) k, dec ( n, n < k P n).
  Proof.
    intros Hp k.
    induction k. right; intros [? [? _]]; .
    destruct IHk as [Hw|Hw].
    - left. destruct Hw as [x [ ]]. exists x; split; eauto; .
    - destruct (Hp k). left. exists k; split; eauto; .
      right. intros [x [ ]].
      assert (x = k x < k) as [|Hk] by ; firstorder.
  Qed.


  Lemma exists_bounded_dec P:
    ( x, dec (P x)) k, dec ( n, n k P n).
  Proof.
    intros Hp k.
    induction k. destruct (Hp 0). left. exists 0. eauto.
    right. intros [x [Hx Hx']]. now assert (x=0) as by .
    destruct IHk as [Hw|Hw].
    - left. destruct Hw as [x [ ]]. exists x; split; eauto; .
    - destruct (Hp (S k)). left. exists (S k); split; eauto; .
      right. intros [x [ ]].
      assert (x = S k x k) as [|Hk] by ; firstorder.
  Qed.


  Definition bounded (P: Prop) := Σ N, x, P x x < N.

  Fact bouned_le (P Q: Prop) N :
    ( x, P x x < N)
    ( x, P x Q x) x, x < N P x Q x.
  Proof.
    intros Hn; split.
    - intros [x Hx]. exists x; intuition eauto.
    - intros (x&c&Hc). exists x; intuition eauto.
  Qed.


  Lemma bounded_dec (P Q: Prop):
    ( x, dec (P x)) ( x, dec (Q x))
    bounded P dec ( n, P n Q n).
  Proof.
    intros [N HN].
    assert (dec ( n, n < N P n Q n)) as [H|H].
    - eapply exists_bounded_dec'. intro; eapply and_dec; eauto.
    - left. rewrite bouned_le; eauto.
    - right. intros H'%(@bouned_le _ _ N); easy.
  Qed.

  Lemma dec_neg_dec P: dec P dec ( P).
  Proof. intros [H|H]. right; eauto. now left. Qed.

  Lemma forall_bounded_dec P e:
    ( x, dec (P x)) dec( i, i e P i).
  Proof.
    intros H.
    induction e. destruct (H 0); [left|right]; intros.
    now inv . intros H'. apply n, H'. .
    destruct IHe as [|].
    destruct (H (S e)); [left|right]; intros.
    inv ; first easy. now apply .
    intros . apply n. apply . easy.
    right. intro H'. apply . intros. apply H'. .
  Qed.


End LeastWitness.

Section logic.

  Definition pdec p := p ¬ p.

  Definition Π_1_lem := p : Prop,
    ( x, dec (p x)) pdec ( x, p x).
  Definition Σ_1_dne := p : Prop,
    ( x, dec (p x)) (¬¬ x, p x) x, p x.
  Definition Σ_1_lem := p: Prop,
    ( x, dec (p x)) pdec ( x, p x).

  Hypothesis : LEM_Σ 1.

  Fact assume_Σ_1_lem: Σ_1_lem .
  Proof.
    intros p Hp.
    destruct level1 as (_&&_).
    assert principles.LPO as H by by rewrite .
    destruct (H Hp) as [[k Hk]|].
    - left. exists k. destruct (Hp k); eauto.
      cbn in Hk. congruence.
    - right. intros [k Hk]. apply .
      exists k. destruct (Hp k); eauto.
  Qed.


  Fact assume_Σ_1_dne: Σ_1_dne.
  Proof.
    intros p Hp H.
    destruct (assume_Σ_1_lem Hp) as [|]; eauto.
    exfalso. by apply H.
  Qed.


  Fact assume_Π_1_lem: Π_1_lem.
  Proof.
    intros p Hp.
    destruct level1 as (_&&_).
    assert principles.LPO as H by by rewrite .
    apply principles.LPO_to_WLPO in H.
    assert ( x : , dec (¬ p x)) as Hp' by eauto.
    destruct (H Hp') as [|].
    - left. intro x.
      specialize ( x).
      apply Dec_false in .
      destruct (Hp x); firstorder.
    - right. intros . apply . intros n.
      specialize ( n). destruct (Hp' n); firstorder.
  Qed.


End logic.