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 SyntheticComputability.Synthetic.EnumerabilityFacts SyntheticComputability.Synthetic.SemiDecidabilityFacts SyntheticComputability.Synthetic.ReducibilityFacts.
Require Import SyntheticComputability.Shared.ListAutomation.
Require Import List Arith.

Import Assume_EA.

Import ListNotations ListAutomationNotations.

Definition productive (p : nat -> Prop) := exists f : nat -> nat, forall c, (forall x, W c x -> p x) -> p (f c) /\ ~ W c (f c).

Lemma productive_nonenumerable p :
  productive p -> ~ enumerable p.
Proof.
  intros [f Hf] [c Hc] % W_spec.
  destruct (Hf c) as [H1 % Hc H2].
  eapply Hc. tauto.
Qed.

Lemma K0_productive :
  productive (compl K0).
Proof.
  exists (fun n => n). intros c H.
  specialize (H c). unfold K0, compl in *. tauto.
Qed.

Lemma productive_cantor_infinite p :
  productive p -> cantor_infinite p.
Proof.
  specialize List_id as [c_l c_spec]. intros [f Hf].
  eapply (weakly_generative_cantor_infinite). econstructor.
  intros l.
  exists (f (c_l l)). intros Hl. split.
  - specialize (Hf (c_l l)).
    rewrite <- c_spec. eapply Hf.
    intros x. rewrite c_spec. eapply Hl.
  - eapply Hf. intros x. rewrite c_spec. eapply Hl.
Qed.

Lemma productive_subpredicate p :
  productive p ->
  exists q : nat -> Prop, enumerable q /\ cantor_infinite q /\ (forall x, q x -> p x).
Proof.
  intros H.
  eapply cantor_infinite_problem.
  eapply productive_cantor_infinite. eauto.
Qed.

Lemma productive_red p q :
  p ⪯ₘ q -> productive p -> productive q.
Proof.
  intros [f Hf] [g Hg].
  specialize (SMN' f) as [k Hk].
  exists (fun c => f (g (k c))). intros c Hs.
  assert (Hkc : forall x, W (k c) x -> p x) by (intros; now eapply Hf, Hs, Hk).
  split.
  - now eapply Hf, Hg.
  - intros ?. eapply Hg, Hk; eauto.
Qed.

Lemma many_one_complete_subpredicate p :
  m-complete p ->
  exists q : nat -> Prop, enumerable q /\ cantor_infinite q /\ (forall x, q x -> compl p x).
Proof.
  intros Hcomp. eapply productive_subpredicate.
  eapply productive_red.
  - eapply red_m_complement. eapply Hcomp. eapply K0_enum.
  - eapply K0_productive.
Qed.

Definition simple (p : nat -> Prop) :=
  enumerable p /\ ~ exhaustible (compl p) /\ ~ exists q, enumerable q /\ ~ exhaustible q /\ (forall x, q x -> compl p x).

Lemma simple_non_enumerable p :
  simple p -> ~ enumerable (compl p).
Proof.
  intros (H1 & H2 & H3) H4.
  apply H3. eauto.
Qed.

Lemma simple_undecidable p :
  simple p -> ~ decidable p.
Proof.
  intros Hs Hd % decidable_complement % decidable_enumerable; eauto.
  now eapply simple_non_enumerable in Hs.
Qed.

Lemma simple_m_incomplete p :
  simple p -> ~ m-complete p.
Proof.
  intros (H1 & H2 & H3) (q & Hq1 & Hq2 & Hq3) % many_one_complete_subpredicate.
  eapply H3. exists q; repeat split; eauto.
  now eapply unbounded_non_finite, cantor_infinite_unbounded.
Qed.

Lemma non_finite_non_empty {X} (p : X -> Prop) :
  ~ exhaustible p -> ~~ exists x, p x.
Proof.
  intros H1 H2. apply H1. exists []. firstorder.
Qed.

Lemma simple_no_cylinder p :
  (fun '((x, n) : nat * nat) => p x) ⪯₁ p -> ~ simple p.
Proof.
  intros [f [inj_f Hf]] (H1 & H2 & H3). red in Hf.
  apply (non_finite_non_empty _ H2). intros [x0 Hx0].
  apply H3.
  exists (fun x => exists n, x = f (x0, n)). split. 2:split.
  - eapply semi_decidable_enumerable; eauto.
    exists (fun x n => Nat.eqb x (f (x0, n))).
    intros x. split; intros [n H]; exists n; destruct (Nat.eqb_spec x (f (x0, n))); firstorder congruence.
  - eapply unbounded_non_finite, cantor_infinite_unbounded.
    exists (fun n => f (x0, n)). intros. split. eauto.
    now intros ? [=] % inj_f.
  - intros ? [n ->]. red. now rewrite <- (Hf (x0, n)).
Qed.