Require Import nd models.
Require Import List.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.Classical.

Definition LEM := forall p, p \/ ~p.
Definition DN := forall p, ~~ p -> p.

Lemma LEM2DN: LEM -> DN.
Proof.
  intros LEM p H.
  destruct (LEM p); firstorder.
Qed.

Section Models.
  Context {d : DerivationType}.

  Definition evalK' {M: KripkeModel} (Γ: theory) :=
    fun w => forall s, (Γ s) -> @evalK M s w.

  Definition isIEL (M: KripkeModel) := forall w, exists w', verif w w'.


  Definition model_constraint (d : DerivationType) m :=
      if d then True else isIEL m.


  Definition entails {d: DerivationType} (Γ: theory) (φ: form) :=
    forall (M : KripkeModel), model_constraint d M ->
      ((forall w,evalK' Γ w -> @evalK M φ w)).

  Notation "Γ ⊨ φ" := (entails Γ φ) (at level 30).

  Variable M : KripkeModel.

  Lemma monotone_ctx (A:theory) :
    forall w w', cogn w w' -> evalK' A w -> evalK' A w'.
  Proof.
    intros. intros t H1.
    apply eval_monotone with (w0 := w); auto.
  Qed.
End Models.

Section Canonical.

  Context {d : DerivationType}.

  Record mcTheory := mkmcTheory {
                         T: theory;
                         Ttheory: forall φ, (@ndT d T φ) -> T φ;
                         consistentT: ~(T ⊥);
                         prime: is_prime T;
                       }.

  Definition lindenBaumTheory (DN: DN) (Γ: theory) (φ: form) (H: ~(ndT Γ φ)) :mcTheory.
    destruct (Lindenbaum H). destruct H1. destruct H2.

    apply mkmcTheory with (T := (max Γ φ)).
    + tauto.
    + intro. apply H1. apply ndtE. apply ndtA. assumption.
    + intros a b Ha.
       unfold is_primeDN in H2. specialize (H2 a b).
       apply DN in H2. eauto.
  Defined.

  Lemma lindenBaumTheorySubset (DN: DN) Γ (φ: form) (H: ~(ndT Γ φ)) : exists Δ: mcTheory ,Γ ⊆ (T Δ).
  Proof.
    exists (lindenBaumTheory DN H).
    simpl T. assert ( (T (lindenBaumTheory DN H)) = (max Γ φ)). cbv. firstorder. unfold lindenBaumTheory. apply max_subset.
  Qed.

  Definition subsetMKT (A B: mcTheory) := subset (T A) (T B).
  Definition valuationMKT (A: mcTheory) (a: nat) := (T A) (Var a).

  Definition subsetVerif (A B:mcTheory) :=
    forall a, ((T A) (K a)) -> (T B) a.
  Instance canonical: (KripkeModel).
  Proof.
    apply mkKripkeModel with (world := mcTheory) (cogn := subsetMKT) (val := valuationMKT) (verif := subsetVerif).
    all: try firstorder.
    intros A B c d' E. apply Ttheory with (φ := d'). destruct B. simpl. apply ndtA. apply c. apply ndtA in E. apply ndtKpos in E.
      apply Ttheory in E. exact E.
  Defined.

  Lemma deductionGamma (Gamma: mcTheory) (phi: form): ndT (T Gamma) phi <-> (T Gamma) phi.
  Proof.
    split.
    - intro. apply Ttheory in H. exact H.
    - apply ndtA.
  Qed.
  Hint Resolve deductionGamma : core.

  Lemma world_canonical_disjunction (t: mcTheory) ψ φ :
    ((T t) (φ ∨ ψ)) <-> (ndT (T t) φ) \/ ndT (T t) ψ.
  Proof.
    intros. split.
    - intro.
      apply prime.
      apply deductionGamma.
      exact H.
    - intro. destruct H; eauto.
      + apply deductionGamma. apply ndtDIL. eauto.
      + apply deductionGamma. apply ndtDIR. eauto.
  Qed.

End Canonical.

Lemma canonicalIEL (DN: DN): isIEL (@canonical normal).
Proof.
  intros w.
  assert (~(@ndT normal (unbox (T w)) ⊥)).
  {
    intros H % modalShiftingLemma.
    destruct w. apply consistentT0.
    apply @Ttheory0.
    apply @ndtIE with (s := (K ⊥)).
    - apply @ndtW with (T := empty).
      + apply IELKBot.
      + firstorder.
    - simpl T in H. exact H.
  }
  exists (lindenBaumTheory DN H).
  intros x H1. simpl lindenBaumTheory.
  simpl T.
  apply max_subset.
  apply unbox_rewrite.
  exact H1.
Qed.

Section Completeness.

  Lemma truth_lemma {d: DerivationType} (DN: DN): forall (X: form) (t: (@world canonical)),
    (evalK X t) <-> ((T t) X).
  Proof.
    intro x.
    induction x.
    - split.
      + intro H0. apply DN. intro H'.
        assert (H: ~ unbox (T t) ⊢T x).
        * intros H. now apply H', deductionGamma, modalShiftingLemma.
        * assert (exists Δ: mcTheory , (unbox (T t)) ⊆ (T Δ)
                                  /\ ~((T Δ) x)).
          {
            exists (lindenBaumTheory DN H).
            split.
            - apply max_subset.
            - intro. apply ndtA in H1.
              apply does_not_derive in H1; auto.
          }
          destruct H1. destruct H1. apply H2. apply IHx. auto.


      + intros A. simpl evalK. intros r V. apply IHx. auto.
    - split.
      +
        intro.
        apply deductionGamma. apply DN. rewrite deductionGamma.
        intro.
        enough (exists Δ: mcTheory, (T t) ⊆ (T Δ) /\ ((T Δ) x1) /\ ~((T Δ) x2)). destruct H1 as [Δ H2].
        specialize (H Δ). destruct H2. destruct H2. apply H3. apply IHx2. (*apply H0.*) firstorder eauto.
        (*    apply IHx1. exact H2.  *)
        rewrite<- deductionGamma in H0. rewrite ImpAgree in H0.
        destruct (Lindenbaum H0).
        exists (lindenBaumTheory DN H0).
        split. intros x H3. firstorder eauto.

        split.
        * apply deductionGamma. apply ndtW with (x1#(T t)). apply ndtA. left. reflexivity. unfold lindenBaumTheory. cbn. apply max_subset.
        * rewrite<- deductionGamma. destruct H2. auto.
      + intros. intros w H1 H2. apply IHx2. apply deductionGamma. apply ndtIE with (s := x1). apply deductionGamma. apply H1. exact H. apply deductionGamma. apply IHx1. exact H2.
    - split.
      + intro H.
        destruct H.
        apply deductionGamma.
        apply ndtCI; apply ndtA.
        * apply IHx1. exact H.
        * apply IHx2. exact H0.
      + intros H1. split.
        * apply deductionGamma in H1. apply ndtCEL in H1. apply IHx1.
          apply deductionGamma. auto.
        * apply deductionGamma in H1. apply ndtCER in H1. apply IHx2.
          apply deductionGamma. auto.
    - intro. simpl evalK. rewrite world_canonical_disjunction. rewrite IHx1. rewrite IHx2.
      repeat rewrite deductionGamma. tauto.

    - split.
      +
        intro. exfalso. apply H.
      + intro. exfalso. apply (consistentT H).
    - split; firstorder.
  Qed.

  Lemma StrongCompleteness {d: DerivationType} (Γ: theory) (φ: form):
   LEM -> (entails Γ φ) -> Γ ⊢T φ.
  Proof.

    intros DN % LEM2DN H0.
    apply DN.
    intro H.
    unfold entails in H0.
    specialize (H0 canonical).
    enough (exists Δ: mcTheory, ~((T Δ) ⊢T φ) /\ (Γ ⊆ (T Δ))).
    destruct H1 as [Δ H2].
    assert (model_constraint d canonical). {
      destruct d eqn:deq.
      - simpl. auto.
      - apply canonicalIEL. auto.
    }
    specialize (H0 H1 Δ).
    apply H2.
    apply deductionGamma.
    apply truth_lemma. auto.
    apply H0. intros ψ P. apply truth_lemma. auto. apply deductionGamma. destruct H2. apply ndtA.
    apply H3. exact P.
    (* Show that such a theory exists *)
    exists (lindenBaumTheory DN H).
    split.
    apply does_not_derive. exact H.
    apply max_subset.
  Qed.


  Lemma evalKimp {M: KripkeModel} s t w: evalK s w -> evalK (Imp s t) w -> evalK t w.
  Proof.
    intros H0 H1.
    apply H1. apply preorderCogn. auto.
  Qed.

  Lemma evalKdistr {M: KripkeModel} s w w': evalK (K s) w -> verif w w' -> evalK s w'.
  Proof.
    intros.
    apply H.
    exact H0.
  Qed.

  Definition ctx2thy (Γ: context) := fun x => In x Γ.

  Lemma ndSoundIELCtx (A: context) (s: form) {p: DerivationType} (D:@nd p A s):entails (ctx2thy A) s.
  Proof.
    intros M Mc. induction D.
    + eauto.
    + intros. exfalso. apply (IHD) with w; auto.
    + intros w1 c1 H2 c2 H3. apply IHD; auto. intro s'. intro H4. destruct H4. subst s'. assumption. apply eval_monotone with (w := w1); auto.
    + intros w H. apply evalKimp with (s0 := s). apply IHD2; auto. apply IHD1; auto.
    + intros w H w' c H1 w'' v. specialize IHD with w. apply evalKimp with (s0 := s). apply H1. exact v.
      apply evalKdistr with (w0 := w); auto. apply transvalid with (y := w'); auto.
    + intros w H w' v. apply IHD; auto. apply monotone_ctx with (w := w); try tauto; auto. apply vericont; auto.
    + intros w H1. apply IHD in H1; auto. destruct H1. auto.
    + intros w H1. apply IHD in H1; auto. destruct H1. auto.
    + intros w H1. split; auto.
    + intros w H1. left. auto.
    + intros w H1. right. auto.
    + intros w H1. destruct (IHD1 Mc w H1).
    - apply (IHD2 Mc w); auto. apply preorderCogn.
    - apply (IHD3 Mc w); auto. apply preorderCogn.
      + intros w H1 u c.
        apply monotone_ctx with (w' := u) in H1. 2: auto.
        unfold isIEL in Mc. destruct (Mc u).
        specialize (IHD Mc u).
        assert (evalK s x).
        {
          apply IHD; auto.
        }
        intro.
        apply (H2 x). apply vericont. auto.
        apply H0.
  Qed.

  Lemma ndSoundIEL (A: theory) (s: form) {p: DerivationType} (D:@ndT p A s):entails A s.
  Proof.
    intros. destruct D. intros M c w H1. destruct H.
    specialize (ndSoundIELCtx H0) . intro H2. apply H2. auto. intros a Ha.
    apply H1. apply H. apply Ha.
  Qed.

  Lemma ndSound (Γ: theory) A {p: DerivationType}: Γ ⊢T A -> entails Γ A.
  Proof.
    intros. apply ndSoundIEL. auto.
  Qed.

  Inductive uno := Uno.
  Definition cogUno := fun (x: uno) (y: uno) => True.
  Definition unoModel: KripkeModel.
    apply mkKripkeModel with (world := uno) (cogn := cogUno) (verif := cogUno) (val := fun x y => True).
    firstorder eauto.
    firstorder eauto.
    firstorder eauto.
    firstorder eauto.
  Defined.

  Lemma hasConstraint (D: DerivationType): model_constraint D unoModel.
  Proof.
    destruct D; firstorder eauto.
  Qed.

  Lemma ndConsistent (D: DerivationType): ~(nil ⊢ ⊥).
  Proof.
    intro.
    specialize (ndSoundIELCtx H). intro.

    enough (exists M, (exists w, ~(@evalK M ⊥ w) /\ model_constraint D M)).
    destruct H1 as (M & w & (H1 & H2)). specialize (H0 M H2 w).
    apply H1. apply H0. intros a Ha. destruct Ha.


    exists unoModel. exists Uno. split; try apply hasConstraint.
    intro. simpl evalK in H1. auto.
  Qed.
End Completeness.

Notation "Γ ⊨ A" := (entails Γ A) (at level 100).
Section CompletenessLEM.
  Variable (D: DerivationType).
  Definition strongCompleteness := forall Γ φ, (entails Γ φ) -> Γ ⊢T φ.

  Definition falsityStable := forall Γ, ~~(ndT Γ ⊥) -> (ndT Γ ⊥).

  Lemma entailmentBotDN Γ: ~~(entails Γ ⊥) -> entails Γ ⊥.
  Proof.
    intro.
    intros M mc w H1. simpl evalK.
     apply wm with (Γ ⊨ ⊥). intro. destruct H0; try tauto.
    specialize (H0 M mc w H1). apply H0.
  Qed.

  Lemma st2fs: strongCompleteness -> falsityStable.
  Proof.
    intros H T H1.
    assert (~~(entails T ⊥)). {
     firstorder eauto using ndSoundIEL.
    }
    firstorder eauto using entailmentBotDN.
  Qed.

  Lemma fstab2LEM: falsityStable -> LEM.
  Proof.
    intros fstab P.
    pose (T := fun (x: form) => P \/ ~P).
    enough (T ⊢T ⊥).
    destruct H as (Γ & Hgam1 & Hgam2).
    destruct Γ.
    - exfalso. apply (@ndConsistent D). apply Hgam2.
    - unfold T in Hgam1. apply Hgam1 with f. eauto.
    - apply fstab. intro. apply wm with P. intro.
      apply H. apply ndtA. unfold T. apply H0.
  Qed.

  Theorem st2lem: strongCompleteness -> LEM.
  Proof.
     intros H % st2fs. apply fstab2LEM; auto.
  Qed.
End CompletenessLEM.

Section CompletenessEnumerableMP.
  Definition MP := forall (f: nat -> bool), ~~(exists n, f n = true) -> exists n, f n = true.
  Context {d: DerivationType}.

  Definition enumerable (T: theory) := exists (f: nat -> option form), forall x, T x -> exists n, f n = (Some x).
  Definition falsityEnumStable := forall Γ, enumerable Γ -> ~~(ndT Γ ⊥) -> (ndT Γ ⊥).

  Definition strongEnumerableCompleteness :=
    forall Γ φ, enumerable Γ -> (entails Γ φ) -> Γ ⊢T φ.

  Lemma ste2fs: strongEnumerableCompleteness -> falsityEnumStable.
  Proof.
    intros H T H0 H1.
    assert (~~(entails T ⊥)). {
      intro. apply H1. intro. apply ndSoundIEL in H3. congruence.
    }
    apply H. auto. apply entailmentBotDN. auto.
  Qed.

  Definition ftheroy (f: nat -> bool) : nat -> option form.
    intro x.
    destruct (f x) eqn:fx.
    + apply (Some (decode x)).
    + apply None.
  Defined.
  Definition ftheroy' (f: nat -> bool) : nat -> option form :=
    fun n =>
         Some ((decode (n)) ∧ (¬ (decode (n)))).

  Lemma fenum2MP: strongEnumerableCompleteness -> MP.
  Proof.
    intros H1 f H2.
    pose (T := fun (x: form) => exists n, f n = true /\ (exists m, x = (m ∧ ¬ m) /\ (decode n = m) )).
    enough (T ⊢T ⊥).
    destruct H as (Γ & Hgam1 & Hgam2).
    destruct Γ.
    - exfalso. apply (@ndConsistent d). apply Hgam2.
    - unfold T in Hgam1. specialize (Hgam1 f0). destruct Hgam1. eauto. exists x. tauto.
    - apply ste2fs. auto.
      + exists (ftheroy' f).
        intros x1 Hx1. unfold T in Hx1. destruct Hx1 as (nHx1 & Thx1).
        destruct Thx1. destruct (decode_surj x1). destruct H0 as (m1 & Hm1 & Hm2).
        exists (nHx1). unfold ftheroy'. rewrite Hm2, Hm1. reflexivity.
      + intro. apply wm with (exists n, f n = true). intro. destruct H0; try tauto. clear H2.
        apply H. destruct H0 as (n1 & Hn1). apply ndtIE with ((decode n1)).
        apply ndtCER with (decode n1). apply ndtA. exists n1. split; eauto.
         apply ndtCEL with (¬(decode n1)). apply ndtA. exists n1. split; eauto.
  Qed.
End CompletenessEnumerableMP.