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: ) (p: Prop): Prop
  := n, ~~ L, length L = n NoDup L
                x, In x L x f n p x.

Definition exceeds f (p : Prop) :=
   n, ~~ i, n < i f n p i.

Lemma exceeds_majorizes f p :
  exceeds f p majorizes ( 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 & & & ).
    specialize (He (Nat.iter (length l) f 0)). cunwrap.
    destruct He as (i & [ ] & ).
    cprove exists (i :: l).
    split; [ | split].
    + reflexivity.
    + econstructor. intros [] % . 2:eauto. .
    + intros m [ | [ ] % ]; split; eauto.
      rewrite numbers.Nat.iter_succ in *. .
Qed.


Lemma cantor_infinite_exceeds (p q : Prop) :
  ( x, q x p x) cantor_infinite q f, exceeds f p.
Proof.
  intros Hq [F] % cantor_infinite_spec. 2: exact _.
  exists ( n proj1_sig (F (seq 0 (S n)))).
  intros n. destruct F as [i [ ]]; cbn.
  cprove exists i; repeat split; eauto.
  destruct (lt_dec n i); eauto.
  destruct . eapply in_seq. split. . cbn. .
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 : ) : list (list ) := 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 l', NoDup l' ( z, In z l In z l') In l' (gen n).
Proof.
  intros % dupfree_Nodup .
  exists (@rep (EqDec.EqType ) 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 . eapply in_seq. 2:eauto. cbn. .
  - eapply (@rep_power (EqDec.EqType )).
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. .
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 := ( z (~~ p z z n) z > n).

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


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


Lemma nnex_forall_class n m p :
  ~~ ( i, n < i m p i) 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" := ( L, reflects L (map p ( QT)) eval_tt ( QT) L = true) (at level 50).
Notation "l ⊫ QT" := (eval_tt QT l = true) (at level 50).

Lemma list_reflects L : ~~ l, 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 p reflects q p q = .
Proof.
  destruct , ; firstorder congruence.
Qed.


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


Theorem tt_complete_exceeds p :
   ⪯ₜₜ p 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 ( n 1 + list_max (concat [ (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 & & ).
  assert ( j, n < j In j ( (g (a n i))) p j). {
    intros j ( & ). eapply H. split.
    - .
    - match goal with [ |- _ 1 + ?J] enough (j J) by end.
      eapply list_max_in. eapply in_concat_iff. eexists. split. eassumption.
      eapply in_map_iff. exists i. split. eauto. eapply in_seq. .
   }
   assert ( x, In x ( (g (a n i))) ~~ p x star_of p n x). {
     intros x Hx.
     assert (x n n < x) as [HH | HH] by .
    - unfold star_of. split. intros ?. left. eauto. intros [[]|]. eauto. .
    - unfold star_of. split; eauto.
   } red in Hg. unfold reflects in Hg.
   apply (@list_reflects (map p ( (g (a n i))))).
   intros (lp & Hlp).
   pose proof (Hg _ _ Hlp) as .
   enough (lp (g (a n i)) lp (g (a n i))) by tauto.
   rewrite at 1.
   unfold .
   unfold a at 1.
   rewrite Hc. fold (a n i).
   rewrite Bool.not_true_iff_false.
   unfold not.
   match goal with [ |- (? _ False) (? _ False)] enough ( = ) by now subst end.
   clear - Hlp .
   revert Hlp . generalize ( (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 ltac:(firstorder)). rewrite Hlist in Hpstar.
       eapply reflects_ext. eapply decider_complement. 2: eapply .
       intros l.
       eapply (inb_spec _ (uncurry Nat.eqb) (decider_eq_nat) ( , l)).
       unfold reflects in . rewrite 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: Prop) : Prop
  := enumerable p exhaustible (compl p)
       f, majorizes f (compl p).

Lemma hyperimmune_immune p :
  MP ( f, majorizes f p) q : Prop, ( 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 ( q : 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.