Require Export ND.

Section GenCons.
  Context {Sigma : Signature}.
  Context {HdF : eq_dec Funcs} {HdP : eq_dec Preds}.
  Context {HeF : enumT Funcs} {HeP : enumT Preds}.

  Context {b : bottom}.
  Variable GBot : form.
  Hypothesis GBot_closed : closed GBot.

  Notation "⊥" := GBot.
  Notation "A ⊢G phi" := (@prv Sigma class b A phi) (at level 30).
  Notation "T ⊩G phi" := (@tprv Sigma class b T phi) (at level 30).

  Definition econsistent T T' := T' ⊩G ⊥ -> T ⊩G ⊥.

  Section Union.
    Variable f : nat -> theory.
    Hypothesis econsistent_f : forall n, econsistent (f n) (f (S n)).
    Hypothesis f_le : forall m n, m <= n -> f m ⊑ f n.

    Definition union (f : nat -> theory) := fun t => exists n, f n t.

    Lemma union_f phi :
      union f ⊩G phi -> exists n, f n ⊩G phi.
    Proof.
      intros (A & HA1 & HA2). enough (exists n, A ⊏ f n) as [n H] by now exists n, A.
      clear HA2; induction A.
      - exists 0; firstorder.
      - destruct IHA as [n Hn]; destruct (HA1 a) as [m Hm]; firstorder.
        exists (max n m); intros ? []; subst.
        + eapply f_le; [apply Nat.le_max_r | firstorder].
        + eapply f_le; [apply Nat.le_max_l | firstorder].
    Qed.

    Lemma union_sub n :
      f n ⊑ union f.
    Proof.
      firstorder.
    Qed.

    Lemma union_econsistent :
      econsistent (f 0) (union f).
    Proof.
      intros [n H] % union_f. induction n; unfold econsistent in *; eauto.
    Qed.

    Lemma union_closed :
      (forall n, closed_T (f n)) -> closed_T (union f).
    Proof.
      intros f_closed ? n [m H]. now apply f_closed with (n := m) (phi := phi).
    Qed.
  End Union.

  Section Explosion.
    Variable T : theory.
    Hypothesis Hclosed : closed_T T.

    Variable e : nat -> form.
    Hypothesis He : forall phi, exists n, e n = phi.

    Definition exp_axiom phi := ⊥ --> close phi.

    Lemma exp_axiom_lift phi A :
      exp_axiom phi el A -> exp_axiom phi el (map (subst_form form_shift) A).
    Proof.
      intros H. apply in_map_iff. exists (exp_axiom phi). split. 2: assumption.
      apply subst_unused_closed' with (xi := form_shift) (phi0 := exp_axiom phi).
      intros ?. constructor. apply GBot_closed. apply close_closed.
    Qed.

    Fixpoint exp n :=
      match n with
      | 0 => T
      | S n => exp n ⋄ exp_axiom (e n)
      end.
    Definition Exp := union exp.

    Lemma Exp_sub :
      T ⊑ Exp.
    Proof.
      apply union_sub with (n := 0) (f := exp).
    Qed.

    Lemma Exp_econsistent :
      econsistent T Exp.
    Proof.
      apply union_econsistent.
      - intros n (B & HB & Hprv) % prv_T_impl. use_theory B.
        opeirce (close (e n)). oimport Hprv. oapply 0. ctx.
      - induction 1; intros ?; firstorder.
    Qed.

    Lemma Exp_closed :
      closed_T Exp.
    Proof.
      apply union_closed. induction n; intuition. intros ? ? []; intuition; subst.
      constructor; [apply GBot_closed | apply close_closed].
    Qed.

    Definition exploding T := forall phi, (⊥ --> close phi) ∈ T.

    Lemma Exp_exploding :
      exploding Exp.
    Proof.
      intros phi. destruct (He phi) as [n Hn]. exists (S n). right; now subst.
    Qed.

    Lemma exploding_inherit T1 T2 :
      exploding T1 -> T1 ⊑ T2 -> exploding T2.
    Proof.
      firstorder.
    Qed.

  End Explosion.

  Notation "¬ phi" := (phi --> GBot) (at level 20).
  Notation "∃ phi" := (¬ ∀ ¬ phi) (at level 56, right associativity).

  Ltac ointro_all :=
    match goal with
    | [ |- ?A ⊢ ∀ ?phi] => apply AllI; cbn; asimpl
    end.

  Ltac ointro_impl :=
    match goal with
    | [ |- _ ⊢ (_ --> _)] => apply II
    | [ |- _ ⊢ (¬ _)] => apply II
    end.

  Ltac ointro := ointro_impl + ointro_all + fail "Nothing to intro!".
  Ltac ointros := repeat ointro.

  Lemma GExp A phi :
    (exp_axiom phi) el A -> A ⊢G ⊥ -> A ⊢G phi.
  Proof.
    intros Hel Hbot. apply close_extract. exact (IE (Ctx Hel) Hbot).
  Qed.

  Ltac oexfalso := apply GExp; [intuition |].

  Lemma GDN A phi :
    (exp_axiom phi) el A -> A ⊢G ¬ (¬ phi) -> A ⊢G phi.
  Proof.
    intros Hx H.
    oimport (Pc A phi GBot). oimport H. oapply 1. ointros. oexfalso. oapply 1. ctx.
  Qed.

  Ltac oindirect := apply GDN; [intuition| apply II].
  Ltac clean H := unfold subst1; rewrite! (subst_unused_closed' _ H).
  Ltac clean_GBot := clean GBot_closed.

  Lemma GExE A phi psi :
    exp_axiom psi el A -> A ⊢G (∃ phi) -> (phi :: map (subst_form form_shift) A) ⊢G psi[↑] -> A ⊢G psi.
  Proof.
    intros Hx Hex Hinst.
    oindirect. oimport Hex. oapply 0. ointros. clean_GBot. oapply 2. ouse Hinst.
  Qed.

  Ltac odestruct n := eapply GExE; [intuition|ctx_index n|]; cbn; asimpl.

  Lemma GExI A t phi :
    A ⊢G phi [t .: ids] -> A ⊢G ∃ phi.
  Proof.
    intros Hc. apply II.
    ospecialize 0 t. clean_GBot. oapply 0. ouse Hc.
  Qed.

  Ltac oexists t :=
    eapply (@GExI _ t); cbn; asimpl.

  Lemma GXM A phi psi :
    exp_axiom psi el A -> (phi :: A) ⊢G psi -> (¬ phi :: A) ⊢G psi -> A ⊢G psi.
  Proof.
    intros Hx Ht Hf. oindirect.
    oassert (¬ phi). ointros. oapply 1. ouse Ht. oapply 1. ouse Hf.
  Qed.

  Ltac oxm form :=
    apply (@GXM _ form); [intuition| |].

  Definition DPexp1 phi := exp_axiom (∃ (phi --> (∀ phi)[↑])).
  Definition DPexp2 phi := exp_axiom (phi [(var_term O) .: (shift >> (shift >> var_term))]).
  Definition DPexp3 phi := exp_axiom phi.

  Lemma GDP A phi :
    DPexp1 phi el A -> DPexp2 phi el A -> DPexp3 phi el A -> A ⊢G ∃ (phi --> (∀ phi)[↑]).
  Proof.
    intros ? H1 H2. do 2 apply exp_axiom_lift in H1. do 1 apply exp_axiom_lift in H2. oxm (∃ (¬ phi)).
    - odestruct 0. clean_GBot. oexists (var_term 0). ointros. oexfalso. clean_GBot. oapply 1. ctx.
    - oexists (var_term 0). ointros. oindirect. clean_GBot. oapply 2. oexists (var_term 0). clean_GBot. ctx.
  Qed.

  Section Henkin.
    Variable T : theory.
    Hypothesis Hclosed : closed_T T.
    Hypothesis Hexp : exploding T.

    Variable e : nat -> form.
    Hypothesis He : forall phi, exists n, e n = phi.
    Hypothesis Hunused : forall n m, n <= m -> unused m (e n).

    Definition henkin_axiom phi := (phi --> ((∀ phi)[↑])).

    Lemma henkin_axiom_unused n phi :
      unused n (∀ phi) -> unused (S n) (¬ (henkin_axiom phi)).
    Proof.
      inversion 1. unfold henkin_axiom. constructor; [| apply GBot_closed].
      capply uf_Impl. capply unused_after_subst. subst. intros x.
      decide (x = n). 1: subst; now left. right; constructor; congruence.
    Qed.

    Fixpoint henkin n :=
      match n with
      | O => T
      | S n => henkin n ⋄ subst_form ((var_term n)..) (henkin_axiom (e n))
      end.

    Lemma henkin_unused n :
      forall phi m, phi ∈ (henkin n) -> n <= m -> unused m phi.
    Proof.
      induction n; cbn.
      - intros. now apply Hclosed.
      - intros phi [| m] H1 H2. omega.
        assert (unused (S m) (e n)) by (apply Hunused; omega).
        assert (unused (S (S m)) (e n)) by (apply Hunused; omega).
        assert (unused m (e n)) by (apply Hunused; omega).
        destruct H1. capply IHn. omega. subst. constructor.
        + apply unused_after_subst. intros []; comp. 1: right; constructor; omega.
          decide (S m = n0). 1: subst; now left. right; constructor; omega.
        + constructor. asimpl. assumption.
    Qed.

    Lemma henkin_le m n :
      m <= n -> henkin m ⊑ henkin n.
    Proof.
      induction 1; firstorder.
    Qed.

    Definition Henkin := union henkin.

    Lemma Henkin_consistent :
      econsistent T Henkin.
    Proof.
      refine (union_econsistent _ henkin_le). intros n.
      assert (unused n (e n)) by now apply Hunused.
      cbn; intros (A & HA1 & HA2) % prv_T_impl.
      rewrite <- (subst_unused_closed' ((var_term n)..) GBot_closed) in HA2.
      apply -> (@nameless_equiv Sigma class b A (¬ (henkin_axiom (e n))) n) in HA2.
      - use_theory (exp_axiom GBot :: DPexp1 (e n) :: DPexp2 (e n) :: DPexp3 (e n) :: A). shelve.
        oimport (@GDP (exp_axiom GBot :: DPexp1 (e n) :: DPexp2 (e n) :: DPexp3 (e n) :: A) (e n)).
        odestruct 0. oimport HA2. shelve. clean_GBot. oapply 0. ctx.
      - apply henkin_axiom_unused; constructor; apply Hunused; omega.
      - intros ? H' % HA1. eapply henkin_unused. apply H'. constructor.
      Unshelve.
        + intros ? [<- | [<- | [ <- | [<- |]]]]. 5: intuition.
          all: apply henkin_le with (m := 0); [omega | apply Hexp].
        + intros ? ?. now do 6 right.
    Qed.

    Definition is_Henkin T := forall T' phi, T ⊑ T' -> (forall t, T' ⊩G phi[t..]) -> T' ⊩G ∀ phi.

    Lemma Henkin_is_Henkin :
      is_Henkin Henkin.
    Proof.
      intros T' phi HT' Hall. destruct (He phi) as [n Hn]. destruct (Hall (var_term n)) as (A & HA1 & HA2).
      use_theory (subst_form ((var_term n)..) (henkin_axiom phi) :: A).
      - intros ? [<- |]; [| intuition]; subst. apply HT'. exists (S n). now right.
      - oimport HA2. comp. oapply 1. ctx.
    Qed.

    Lemma is_Henkin_inherit T1 T2 :
      is_Henkin T1 -> T1 ⊑ T2 -> is_Henkin T2.
    Proof.
      firstorder.
    Qed.

    Lemma Henkin_T :
      T ⊑ Henkin.
    Proof.
      apply union_sub with (f := henkin) (n := 0).
    Qed.
  End Henkin.

  Section Omega.
    Variable e : nat -> form.
    Hypothesis He : forall phi, exists n, e n = phi.

    Variable T : theory.
    Hypothesis Hexp : exploding T.
    Hypothesis Hhenkin : is_Henkin T.

    Definition maximal T := forall f, econsistent T (T ⋄ f) -> f ∈ T.

    Definition econsistent_join T phi := fun psi => T psi \/ (econsistent T (T ⋄ phi) /\ psi = phi).
    Infix "∘" := econsistent_join (at level 20).

    Lemma econsistent_join_sub T' phi :
      (T' ∘ phi) ⊑ (T' ⋄ phi).
    Proof.
      firstorder.
    Qed.

    Lemma consistent_join_step T' phi psi :
      T' ∘ psi ⊩G phi -> T' ⊩G phi \/ econsistent T' (T' ⋄ psi).
    Proof.
      intros (A & HA1 & HA2).
      enough (A ⊏ T' \/ econsistent T' (T' ⋄ psi)) as [] by ((left; exists A; intuition) + now right).
      clear HA2; induction A.
      - firstorder.
      - destruct (HA1 a), IHA; intuition. all: eauto with contains_theory.
    Qed.

    Fixpoint omega n : theory :=
      match n with
      | 0 => T
      | S n => omega n ∘ e n
      end.

    Lemma omega_le n m :
      n <= m -> omega n ⊑ omega m.
    Proof.
      induction 1; firstorder.
    Qed.

    Definition Omega : theory := union omega.

    Lemma econsistent_Omega :
      econsistent T Omega.
    Proof.
      refine (union_econsistent _ omega_le). intros n H. destruct (consistent_join_step H).
      all: firstorder.
    Qed.

    Lemma econsistency_inheritance T1 T2 T1' T2' :
      econsistent T1 T1' -> T1 ⊑ T2 -> T2' ⊑ T1' -> econsistent T2 T2'.
    Proof.
      firstorder.
    Qed.

    Lemma econsistency_trans T1 T2 T3 :
      econsistent T1 T2 -> econsistent T2 T3 -> econsistent T1 T3.
    Proof.
      firstorder.
    Qed.

    Lemma maximal_Omega :
      maximal Omega.
    Proof.
      intros phi H. destruct (He phi) as [n Hn].
      apply (union_sub (n := S n)); cbn; rewrite -> Hn. right; split; [| reflexivity].
      eapply econsistency_inheritance.
      + exact (econsistency_trans econsistent_Omega H).
      + apply omega_le with (n := 0). omega.
      + firstorder.
    Qed.

    Lemma econsistent_prv T' T'' phi :
      econsistent T' T'' -> T'' ⊩G phi -> econsistent T' (T'' ⋄ phi).
    Proof.
      intros HT Hphi Hbot. now apply HT, (prv_T_remove Hphi).
    Qed.

    Lemma maximal_prv T' phi :
      maximal T' -> T' ⊩G phi -> phi ∈ T'.
    Proof.
      intros Hin Hprv. now apply Hin, econsistent_prv.
    Qed.

    Lemma Omega_prv phi :
      Omega ⊩G phi -> phi ∈ Omega.
    Proof.
      intros Hprv. now apply (maximal_prv maximal_Omega).
    Qed.

    Lemma Omega_T :
      T ⊑ Omega.
    Proof.
      change T with (omega 0). apply (union_sub (n := 0)).
    Qed.

    Lemma Omega_impl phi psi :
      phi --> psi ∈ Omega <-> (phi ∈ Omega -> psi ∈ Omega).
    Proof.
      split.
      - intros Himp Hphi. apply Omega_prv.
        use_theory [phi --> psi; phi]. oapply 0. ctx.
      - intros H. apply maximal_Omega. intros (A & HA1 & HA2) % prv_T_impl.
        apply (prv_T_remove (phi := psi)).
        + apply elem_prv, H, Omega_prv.
          use_theory (exp_axiom phi :: exp_axiom psi :: A).
          * intros ? [<- | [ <- | H'']]; [apply Omega_T, Hexp | apply Omega_T, Hexp | now apply HA1].
          * oindirect. oimport HA2. oapply 0. ointros. oexfalso. oapply 2. ctx.
        + use_theory (psi :: A). oimport HA2. oapply 0. ointros. ctx.
    Qed.

    Lemma Omega_all phi :
      ∀ phi ∈ Omega <-> (forall t, phi[t..] ∈ Omega).
    Proof.
      split; intros Hprv.
      - intros t. apply Omega_prv. use_theory [∀ phi]. ospecialize 0 t. ctx.
      - apply Omega_prv, (Hhenkin Omega_T). eauto using elem_prv.
    Qed.
  End Omega.
End GenCons.

Section Composition.
  Context {Sigma : Signature}.
  Context {HdF : eq_dec Funcs} {HdP : eq_dec Preds}.
  Context {HeF : enumT Funcs} {HeP : enumT Preds}.

  Structure ConstructionInputs : Type :=
    {
      NBot : form ;
      NBot_closed : closed NBot ;
      
      variant : bottom ;

      In_T : theory ;
      In_T_closed : closed_T In_T ;

      enum : nat -> form ;
      enum_enum : forall phi, exists n, enum n = phi ;
      enum_unused : forall n m, n <= m -> unused m (enum n)
    }.

  Structure ConstructionOutputs (In : ConstructionInputs) :=
    {
      Out_T : theory ;
      Out_T_econsistent : @econsistent Sigma (variant In) (NBot In) (In_T In) Out_T ;
      Out_T_sub : In_T In ⊑ Out_T ;

      Out_T_prv : forall phi, @tprv Sigma class (variant In) Out_T phi -> phi ∈ Out_T ;
      Out_T_all : forall phi, ∀ phi ∈ Out_T <-> (forall t, phi[t..] ∈ Out_T) ;
      Out_T_impl : forall phi psi, phi --> psi ∈ Out_T <-> (phi ∈ Out_T -> psi ∈ Out_T)
    }.

  Lemma construct_construction (In : ConstructionInputs) :
    ConstructionOutputs In.
  Proof.
    destruct In as [NBot NBot_closed system T T_closed e e_enum e_unused].
    eexists (Omega NBot e (Henkin (Exp NBot T e) e)); cbn.
    + capply econsistency_trans. capply econsistency_trans. capply Exp_econsistent.
      capply Henkin_consistent. capply Exp_closed. capply Exp_exploding. capply econsistent_Omega.
    + transitivity (Henkin (Exp NBot T e) e). transitivity (Exp NBot T e).
      apply Exp_sub. apply Henkin_T. apply Omega_T.
    + capply Omega_prv.
    + capply Omega_all. capply Henkin_is_Henkin.
    + capply Omega_impl. capply exploding_inherit.
      - capply Exp_exploding.
      - capply Henkin_T.
  Qed.
End Composition.