Require Import SyntheticComputability.Axioms.EA.
Require Import SyntheticComputability.Shared.Pigeonhole.
Require Import SyntheticComputability.Shared.FinitenessFacts.
Require Import SyntheticComputability.Synthetic.reductions SyntheticComputability.Synthetic.truthtables.
Require Import SyntheticComputability.Synthetic.DecidabilityFacts.
Require Import SyntheticComputability.Shared.ListAutomation.
Require Import List Arith.

Import Assume_EA.
Import ListNotations ListAutomationNotations.

Definition majorizes (f: nat -> nat) (p: nat -> Prop): Prop
  := forall n, ~~ exists L, length L = n /\ NoDup L /\
               forall x, In x L -> x <= f n /\ p x.

Definition exceeds f (p : nat -> Prop) :=
  forall n, ~~ exists i, n < i <= f n /\ p i.

Lemma exceeds_majorizes f p :
  exceeds f p -> majorizes (fun n => Nat.iter n f 0) p.
Proof.
  intros He n. induction n.
  - cprove exists []. repeat split.
    + econstructor.
    + inversion H.
    + inversion H.
  - cunwrap. destruct IHn as (l & <- & IH1 & IH2).
    specialize (He (Nat.iter (length l) f 0)). cunwrap.
    destruct He as (i & [H1 H2] & H3).
    cprove exists (i :: l).
    split; [ | split].
    + reflexivity.
    + econstructor. intros [] % IH2. 2:eauto. lia.
    + intros m [-> | [H4 H5] % IH2]; split; eauto.
      rewrite numbers.Nat.iter_succ in *. lia.
Qed.

Lemma cantor_infinite_exceeds (p q : nat -> Prop) :
  (forall x, q x -> p x) -> cantor_infinite q -> exists f, exceeds f p.
Proof.
  intros Hq [F] % cantor_infinite_spec. 2: exact _.
  exists (fun n => proj1_sig (F (seq 0 (S n)))).
  intros n. destruct F as [i [Hi1 Hi2]]; cbn.
  cprove exists i; repeat split; eauto.
  destruct (lt_dec n i); eauto.
  destruct Hi1. eapply in_seq. split. lia. cbn. lia.
Qed.

Definition ttId := Assume_EA.TT.

Lemma IsFilter_NoDup {X} l l' (p : X -> Prop) :
  IsFilter p l l' -> NoDup l -> NoDup l'.
Proof.
  induction 1; inversion 1; subst.
  - eauto.
  - econstructor. eapply IsFilter_spec in H as (? & ? & ?). firstorder. eauto.
  - eauto.
Qed.

From SyntheticComputability.Shared.Libs.PSL Require Import Power EqDec.

Definition gen (n : nat) : list (list nat) := power (seq 0 (S n)).

Lemma dupfree_Nodup {X} (A : list X) :
  Dupfree.dupfree A <-> NoDup A.
Proof.
  induction A;split;intros H;inv H;repeat econstructor;tauto.
Qed.

Lemma dupfree_rep {X : eqType} (A : list X) U : Dupfree.dupfree U -> Dupfree.dupfree (rep A U).
Proof.
  induction 1.
  - cbn. econstructor.
  - cbn. destruct Dec; cbn.
    + econstructor. intros ? % in_filter_iff. 1:firstorder.
      exact IHdupfree.
    + exact IHdupfree.
Qed.

Lemma gen_spec' n l : NoDup l -> list_max l <= n -> exists l', NoDup l' /\ (forall z, In z l <-> In z l') /\ In l' (gen n).
Proof.
  intros H1 % dupfree_Nodup H2.
  exists (@rep (EqDec.EqType nat) l (seq 0 (S n))). split; [ | split].
  - eapply dupfree_Nodup, dupfree_rep, dupfree_Nodup, seq_NoDup.
  - intros z. rewrite rep_equi. reflexivity. intros x Hx.
    eapply list_max_le, Forall_forall in H2. eapply in_seq. 2:eauto. cbn. lia.
  - eapply (@rep_power (EqDec.EqType nat)).
Qed.

Lemma power_length {X : eqType} (l : list X) : length (power l) = 2 ^ (length l).
Proof.
  induction l; cbn.
  - reflexivity.
  - rewrite app_length, map_length, <- IHl. lia.
Qed.

Lemma gen_length n : length (gen n) = 2 ^ (S n).
Proof.
  unfold gen.
  now rewrite power_length, seq_length.
Qed.

Definition star_of p n := (fun z => (~~ p z /\ z <= n) \/ z > n).

Lemma star_of_nnex n p : (* listable until *)
  ~~ exists i, i < 2^(S n) /\ forall z, ~ In z (nth i (gen n) []) <-> star_of p n z.
Proof.
  enough (~~ exists l, list_max l <= n /\ NoDup l /\ forall z, ~ In z l <-> star_of p n z).
  - cunwrap. destruct H as (l & H1 & H2 & H3).
    epose proof (@gen_spec' n l) as H.
    specialize (H ltac:(firstorder) ltac:(firstorder)) as (l' & H4 & H5 & H6).
    eapply In_nth in H6 as (i & ? & ?).
    cprove exists i. split. rewrite <- gen_length. eauto.
    rewrite H0. setoid_rewrite <- H5. eassumption.
  - pose proof (IsFilter_nnex (seq 0 (S n)) (compl p)). cunwrap.
    destruct H as (l' & Hf). pose proof Hf as (H1 & H2 & H3) % IsFilter_spec.
    cprove exists l'. split. 2:split.
    + eapply list_max_le, Forall_forall. intros ? [? % in_seq _] % H3. lia.
    + eapply IsFilter_NoDup; eauto. eapply seq_NoDup.
    + intros. rewrite H3. unfold star_of. rewrite in_seq. split.
      * intros ?. assert (z <= n \/ z > n) as [Hz | Hz] by lia.
        -- left. split; eauto. intros Hp. eapply H. split. cbn. lia. eauto.
        -- right. eauto.
      * intros [[] | ] [ ]. tauto. lia.
Qed.

(* instead: listable quantification *)
Lemma finite_quant_DN n m (p : nat -> Prop) : (forall i, n < i <= m -> ~~ p i) -> ~~ (forall i, n < i <= m -> p i).
Proof.
  assert (n < m \/ m <= n) as [Hnm | ] by lia. 2:{ intros. cprove intros. lia. }
  intros H. induction m in n, Hnm, H |- *.
  - cprove intros. lia.
  - ccase (p (S m)) as [Hp | Hp].
    + assert (n = m \/ n < m) as [] by lia.
      * subst. cprove intros. assert (i = S m) as -> by lia. eauto.
      * intros ?. eapply IHm.
        -- eassumption.
        -- intros. destruct (Nat.eqb_spec i (S m)); subst. eauto. eapply H. lia.
        -- intros IH. eapply H1. intros. destruct (Nat.eqb_spec i (S m)); subst. eauto. eapply IH. lia.
    + exfalso. eapply H. 2: eauto. lia.
Qed.

Lemma nnex_forall_class n m p :
  ~~ (exists i, n < i <= m /\ ~ p i) <-> ~ forall i, n < i <= m -> p i.
Proof.
  split.
  - intros H Hi. apply H. intros (i & ? & ?). eauto.
  - intros H Hi. apply finite_quant_DN in H. apply H. intros ? ? ?.
    apply Hi. eauto.
Qed.

Notation "p ⊨ QT" := (forall L, Forall2 reflects L (map p (projT1 QT)) -> eval_tt (projT2 QT) L = true) (at level 50).
Notation "l ⊫ QT" := (eval_tt QT l = true) (at level 50).

Lemma list_reflects L : ~~ exists l, Forall2 reflects l L.
Proof.
  induction L as [ | P L].
  - cprove exists []. econstructor.
  - cunwrap. destruct IHL as (l & IH).
    ccase P as [H | H].
    + cprove exists (true :: l). econstructor; firstorder.
    + cprove exists (false :: l). econstructor; firstorder.
Qed.

Lemma reflects_ext b1 b2 p q : reflects b1 p -> reflects b2 q -> p <-> q -> b1 = b2.
Proof.
  destruct b1, b2; firstorder congruence.
Qed.

Lemma list_max_in x l : In x l -> x <= list_max l.
Proof.
  induction l; cbn.
  - firstorder.
  - intros [-> | ]. lia. eapply IHl in H. unfold list_max in H. lia.
Qed.

Theorem tt_complete_exceeds p :
  K0 ⪯ₜₜ p -> exists f, exceeds f (compl p).
Proof.
  intros [g Hg].
  destruct (ttId g) as [c Hc].
  pose (a n i := c (nth i (gen n) [])).
  exists (fun n => 1 + list_max (concat [ projT1 (g (a n i)) | i ∈ seq 0 (2^(S n))])).
  intros n. eapply nnex_forall_class. intros H.
  eapply (@star_of_nnex n p). intros (i & Hi1 & Hi2).
  assert (forall j, n < j /\ In j (projT1 (g (a n i))) -> p j). {
    intros j (H1 & H2). eapply H. split.
    - lia.
    - match goal with [ |- _ <= 1 + ?J] => enough (j <= J) by lia end.
      eapply list_max_in. eapply in_concat_iff. eexists. split. eassumption.
      eapply in_map_iff. exists i. split. eauto. eapply in_seq. lia.
   }
   assert (forall x, In x (projT1 (g (a n i))) -> ~~ p x <-> star_of p n x). {
     intros x Hx.
     assert (x <= n \/ n < x) as [HH | HH] by lia.
    - unfold star_of. split. intros ?. left. eauto. intros [[]|]. eauto. lia.
    - unfold star_of. split; eauto.
   } red in Hg. unfold reflects in Hg.
   apply (@list_reflects (map p (projT1 (g (a n i))))).
   intros (lp & Hlp).
   pose proof (Hg _ _ Hlp) as H2.
   enough (lp ⊫ projT2 (g (a n i)) <-> ~ lp ⊫ projT2 (g (a n i))) by tauto.
   rewrite <- H2 at 1.
   unfold K0.
   unfold a at 1.
   rewrite Hc. fold (a n i).
   rewrite <- Bool.not_true_iff_false.
   unfold not.
   match goal with [ |- (?l1 ⊫ _ -> False) <-> (?l2 ⊫ _ -> False)] => enough (l1 = l2) by now subst end.
   clear - Hlp H1 Hi2.
   revert H1 Hlp Hi2. generalize (projT1 (g (a n i))) as L. clear.
   induction lp; intros L Hpstar Hlp Hlist; cbn -[nth].
   - destruct L; inv Hlp. reflexivity.
   - destruct L; inv Hlp. cbn -[nth].
     f_equal.
     + specialize (Hpstar n0 ltac:(firstorder)). rewrite <- Hlist in Hpstar.
       eapply reflects_ext. eapply decider_complement. 2: eapply H2.
       intros l.
       eapply (inb_spec _ (uncurry Nat.eqb) (decider_eq_nat) (n0 , l)).
       unfold reflects in H2. rewrite H2 in *. rewrite Bool.not_true_iff_false, Bool.not_false_iff_true in Hpstar.
       symmetry. eapply Hpstar.
     + eapply IHlp. intros. eapply Hpstar. eauto. eauto. eauto.
Qed.

From SyntheticComputability Require Import principles.

Definition hypersimple (p: nat -> Prop) : Prop
  := enumerable p /\ ~ exhaustible (compl p) /\
      ~ exists f, majorizes f (compl p).

Lemma hyperimmune_immune p :
  MP -> ~ (exists f, majorizes f p) -> ~ exists q : nat -> Prop, (forall x, q x -> p x) /\ ~ exhaustible q /\ enumerable q.
Proof.
  intros mp Hi (q & Hsub & Hinf & Henum).
  eapply MP_non_finite_generative in Hinf; eauto.
  eapply MoreEnumerabilityFacts.generative_cantor_infinite in Hinf; eauto.
  eapply cantor_infinite_exceeds in Hinf as (f & Hexc); eauto.
  eapply Hi. eexists. eapply exceeds_majorizes; eauto.
Qed.

Lemma hypersimple_tt_incomplete p :
  hypersimple p -> ~ (forall q : nat -> Prop, enumerable q -> q ⪯ₜₜ p).
Proof.
  intros (He & Hinf & Himm) H.
  specialize (H _ K0_enum).
  eapply tt_complete_exceeds in H as (f & H).
  eapply Himm. eexists. eapply exceeds_majorizes; eauto.
Qed.

From SyntheticComputability Require Import simple.

Lemma hypersimple_simple p :
  MP -> hypersimple p -> simple p.
Proof.
  intros mp (He & Hinf & Himm). repeat split; eauto.
  intros (q & Heq & Hinfq & Hsub).
  eapply hyperimmune_immune; eauto.
Qed.