From Undecidability.FOL.Incompleteness Require Import utils.

From Undecidability.Synthetic Require Import Definitions Undecidability.
From Undecidability.Synthetic Require Import DecidabilityFacts EnumerabilityFacts.
From Undecidability.Shared Require Import Dec.
From Equations Require Import Equations.

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Record FS (S : Type) (neg : S -> S) : Type :=
  mkFS { fprv : S -> Prop
       ; S_discrete : discrete S
       ; P_enumerable : enumerable fprv
       ; consistent : forall s, fprv s -> fprv (neg s) -> False }.
Arguments FS : clear implicits.

Arguments consistent {S neg} _ _ _ _.

Notation "fs ⊢F s" := (fs.(fprv) s) (at level 30).
Notation "fs ⊬F s" := (~fs.(fprv) s) (at level 30).

Definition extension {S : Type} {neg : S -> S} (fs1 fs2 : FS S neg) :=
  forall s, fs1 ⊢F s -> fs2 ⊢F s.

Section facts.
  Context {S : Type} {neg : S -> S} (fs : FS S neg).

  Definition complete := forall s, fs ⊢F s \/ fs ⊢F neg s.
  Definition independent s := fs ⊬F s /\ fs ⊬F neg s.

  Definition weakly_represents (fprv : nat -> Prop) (r : nat -> S) :=
    forall x, fprv x <-> fs ⊢F r x.
  Definition strongly_separates (P1 P2 : nat -> Prop) (r : nat -> S) :=
    (forall x, P1 x -> fs ⊢F r x) /\
    (forall x, P2 x -> fs ⊢F neg (r x)).

  Lemma refutable_semi_decidable : semi_decidable (fun s => fs ⊢F neg s).
  Proof.
    destruct fs.(P_enumerable) as [prov Hprov].
    pose proof fs.(S_discrete) as [S_eqdec]%discrete_iff.

    unshelve eexists.
    { intros s k. refine (match prov k with
                          | Some s' => if S_eqdec (neg s) s' then true else false
                          | None => false end). }
    intros s. unfold enumerator in Hprov. rewrite Hprov.
    apply utils_tac.exists_equiv. intros n.
    destruct (prov n); last easy.
    destruct S_eqdec; firstorder congruence.
  Qed.

  Theorem is_provable : exists f : S -\ bool,
    (forall s, fs ⊢F s <-> f s ▷ true) /\
    (forall s, fs ⊢F neg s <-> f s ▷ false).
  Proof.
    apply enumerable_separable.
    - apply fs.(consistent).
    - apply enumerable_semi_decidable.
      + apply fs.(S_discrete).
      + apply fs.(P_enumerable).
    - apply refutable_semi_decidable.
  Qed.

  Lemma complete_decidable : complete -> decidable fs.(fprv).
  Proof.
    intros complete. destruct is_provable as [f Hf].
    assert (forall x, exists b, f x ▷ b) as Htotal.
    { intros x. destruct (complete x) as [H|H].
      - exists true. now apply Hf.
      - exists false. now apply Hf. }
    exists (fun x => projT1 (totalise Htotal x)).
    intros x. destruct totalise as [[] Hb]; split; cbn.
    - easy.
    - intros _. now apply Hf.
    - intros H%Hf. eapply part_functional; eassumption.
    - discriminate.
  Qed.

End facts.