From Undecidability.FOLC Require Export GenConstructions.
From Undecidability.FOLC Require Export Consistency.
From Undecidability.FOLC Require Export GenTarski.
From Undecidability.FOLC Require Import Stability.

Completeness


(* ** Standard Models **)

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

  Hint Constructors unused.

  Section BotModel.
    Variable T : theory.
    Hypothesis T_closed : closed_T T.

    Definition input_bot :=
      {|
        NBot := Fal ;
        NBot_closed := (fun n => uf_Fal n) ;

        variant := expl ;

        In_T := T ;
        In_T_closed := T_closed ;

        GenConstructions.enum := form_enum ;
        enum_enum := form_enum_enumerates ;
        enum_unused := form_enum_fresh
      |}.

    Definition output_bot := construct_construction input_bot.

    Instance model_bot : interp term :=
      {| i_f := Func; i_P := fun P v => Pred P v Out_T output_bot ;
        i_F := Out_T output_bot |}.

    Lemma eval_ident (t : term) :
      eval t = subst_term t.
    Proof.
      induction t using strong_term_ind; comp; asimpl; try congruence. f_equal.
    Qed.


    Lemma model_bot_correct :
      ([] Out_T output_bot ).
    Proof.
      induction in |-*. 1,2,3: comp.
      - tauto.
      - now rewrite (vec_ext ( x eval_ident x)).
      - rewrite , . now apply Out_T_impl.
      - cbn. setoid_rewrite IHphi. rewrite Out_T_all.
        split; intros H d; specialize (H d); comp; now asimpl in H.
    Qed.


    Lemma model_bot_classical :
      classical model_bot.
    Proof.
      intros . apply model_bot_correct, Out_T_prv.
      use_theory (nil : list form). apply Pc.
    Qed.


    Lemma model_bot_standard :
      consistent T SM model_bot.
    Proof.
      intros Hcon. split. 1: exact model_bot_classical. intros Hin. apply Hcon.
      apply Out_T_econsistent with output_bot. use_theory []. ctx.
    Qed.


    Lemma model_bot_exploding :
      EM model_bot.
    Proof.
      split. 1: exact model_bot_classical. intros . apply model_bot_correct.
      comp. apply Out_T_prv. use_theory (nil : list form). ointros. oexfalso. ctx.
    Qed.


    Lemma valid_T_model_bot :
       T ids .
    Proof.
      intros H % (Out_T_sub output_bot). apply model_bot_correct; now comp.
    Qed.

  End BotModel.

  Section StandardCompletenes.
    Variables (T : theory) ( : form).
    Hypothesis (HT : closed_T T) (Hphi : closed ).

    Lemma semi_completeness_standard :
      T S T CE .
    Proof.
      intros Hval Hcons. rewrite refutation_prv in Hcons.
      assert (Hcl : closed_T (T (¬ ))) by ( intros ? ? [] ; subst; eauto).
      destruct (model_bot_standard Hcl Hcons) as [Hclass Hb]. apply Hb.
      apply (model_bot_correct Hcl (¬ ) ids). apply Out_T_sub. right. now comp. refine (Hval _ _ _ _ _).
      - now apply model_bot_standard.
      - intros ? ?. apply valid_T_model_bot; intuition.
    Qed.


    Lemma completeness_standard_stability :
      (T S T CE ) stable (T CE ).
    Proof.
      split.
      - intros Hcomp Hdn. apply Hcomp, valid_T_standard_dm. 1: firstorder. intros Hsem.
        apply Hdn. intros H. apply Hsem, (StrongSoundness H).
        + now intros _ ? ? [].
        + intros _ ? ? []. firstorder.
      - intros Hstab Hsem. now apply Hstab, semi_completeness_standard.
    Qed.

  End StandardCompletenes.

  Section MPStrongCompleteness.
    Hypothesis mp : MP.
    Variable (T : theory) ( : form) (L : list form).
    Hypothesis (HT : closed_T T) (Hphi : closed ).
    Hypothesis (He : DecidableEnumerable.enum T L).

    Lemma mp_tprv_stability {p : peirce} {b : bottom} :
       T T .
    Proof.
      apply (enumeration_stability mp (enum_tprv He) (dec_form HdF HdP)).
    Qed.


    Lemma mp_standard_completeness :
      T S T CE .
    Proof.
      intros Hprv % semi_completeness_standard. 2,3: assumption.
      now apply mp_tprv_stability.
    Qed.

  End MPStrongCompleteness.

(* *** Exploding Models **)

  Section ExplodingCompletenes.
    Variables (T : theory) ( : form).
    Hypothesis (HT : closed_T T) (Hphi : closed ).

    Lemma completeness_expl :
      T E T CE .
    Proof.
      intros Hval. assert (Hcl : closed_T (T (¬ ))) by (intros ? ? [] ; subst; eauto).
      apply refutation_prv. apply (@Out_T_econsistent _ _ (output_bot Hcl)); cbn. use_theory []. 2: ctx.
      intros ? [ | []]. apply (model_bot_correct _ ids).
      specialize (Hval term (model_bot Hcl) (model_bot_exploding Hcl) ids).
      assert (@sat _ _ (model_bot Hcl) ids (¬ )) by (apply model_bot_correct, Out_T_sub; comp; firstorder).
      apply H, Hval. intros ? ?. apply valid_T_model_bot; intuition.
    Qed.


    Lemma valid_standard_expld_stability :
      (T S T E ) stable (T CE ).
    Proof.
      rewrite completeness_standard_stability. 2,3: assumption. split.
      - intros Hincl Hval % Hincl. now apply completeness_expl.
      - intros Hcomp Hprv % Hcomp. apply (StrongSoundness Hprv).
        all: now intros _ ? ? [].
    Qed.

  End ExplodingCompletenes.

(* *** Minimal Models **)

  Section FragmentModel.
    Variable T : theory.
    Hypothesis T_closed : closed_T T.

    Variable GBot : form.
    Hypothesis GBot_closed : closed GBot.

    Definition input_fragment :=
      {|
        NBot := GBot ;
        NBot_closed := GBot_closed ;

        variant := lconst ;

        In_T := T ;
        In_T_closed := T_closed ;

        GenConstructions.enum := form_enum ;
        enum_enum := form_enum_enumerates ;
        enum_unused := form_enum_fresh
      |}.

    Definition output_fragment := construct_construction input_fragment.

    Instance model_fragment : interp term :=
      {| i_f := Func; i_P := fun P v => Pred P v Out_T output_fragment ;
        i_F := Out_T output_fragment |}.

    Lemma eval_ident_fragment (t : term) :
      eval t = subst_term t.
    Proof.
      induction t using strong_term_ind; comp; asimpl; try congruence. f_equal.
    Qed.


    Lemma model_fragment_correct :
      ([] Out_T output_fragment ).
    Proof.
      induction in |-*. 1,2,3: comp.
      - tauto.
      - now rewrite (vec_ext ( x eval_ident_fragment x)).
      - rewrite , . now apply Out_T_impl.
      - cbn. setoid_rewrite IHphi. rewrite Out_T_all.
        split; intros H d; specialize (H d); comp; now asimpl in H.
    Qed.


    Lemma model_fragment_classical :
      BLM model_fragment.
    Proof.
      intros . apply model_fragment_correct, Out_T_prv.
      use_theory (nil : list form). apply Pc.
    Qed.


    Lemma valid_T_fragment :
       T ids .
    Proof.
      intros H % (Out_T_sub output_fragment). apply model_fragment_correct; now comp.
    Qed.

  End FragmentModel.

  Section FragmentCompleteness.

    Lemma semi_completeness_fragment T :
      closed_T T closed T M T CL .
    Proof.
      intros HT Hphi Hval. replace with ([ids]) in * by now comp.
      apply (@Out_T_econsistent _ _ (output_fragment HT Hphi)); cbn. use_theory [[ids]]. 2: ctx.
      intros ? [ | []]. apply (model_fragment_correct HT Hphi ids). comp. rewrite instId_form in Hval.
      apply Hval. 1: apply model_fragment_classical. intros ? ?. apply valid_T_fragment; intuition.
    Qed.

  End FragmentCompleteness.
End Completeness.

(* ** Extending the Completeness Results *)

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

  Lemma list_completeness_standard A :
    ST__f valid_L SM A A CE .
  Proof.
    intros stf Hval % valid_L_to_single. apply prv_from_single.
    apply con_T_correct. apply completeness_standard_stability.
    1: intros ? ? []. 1: apply close_closed. 2: now apply valid_L_valid_T in Hval.
    apply stf, fin_T_con_T.
    - intros ? ? [].
    - eapply close_closed.
  Qed.


  Lemma list_completeness_expl A :
    valid_L EM A A CE .
  Proof.
    intros Hval % valid_L_to_single. apply prv_from_single.
    apply tprv_list_T. apply completeness_expl. 1: intros ? ? [].
    1: apply close_closed. now apply valid_L_valid_T in Hval.
  Qed.


  Lemma list_completeness_fragment A :
    valid_L BLM A A CL .
  Proof.
    intros Hval % valid_L_to_single. apply prv_from_single.
    apply tprv_list_T. apply semi_completeness_fragment. 1: intros ? ? [].
    1: apply close_closed. now apply valid_L_valid_T in Hval.
  Qed.

End FiniteCompleteness.

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

  Lemma dn_inherit (P Q : Prop) :
    (P Q) P Q.
  Proof. tauto. Qed.

  Lemma strong_completeness_standard (S : stab_class) T :
    ( (T : theory) ( : form), S T stable (tmap ( : form (sig_lift )[ext_c]) T CE )) @map_closed S (sig_ext ) ( (sig_lift )[ext_c]) S T T S T CE .
  Proof.
    intros sts cls HT Hval. apply sig_lift_out_T. apply completeness_standard_stability.
    1: apply lift_ext_c_closes_T. 1: apply lift_ext_c_closes. 2: apply (sig_lift_subst_valid droppable_S Hval).
    now apply sts.
  Qed.


  Lemma strong_completeness_expl T :
    T E T CE .
  Proof.
    intros Hval. apply sig_lift_out_T, completeness_expl.
    1: apply lift_ext_c_closes_T. 1: apply lift_ext_c_closes.
    apply (sig_lift_subst_valid droppable_E Hval).
  Qed.


  Lemma strong_completeness_fragment T :
    T M T CL .
  Proof.
    intros Hval. apply sig_lift_out_T, semi_completeness_fragment.
    1: apply lift_ext_c_closes_T. 1: apply lift_ext_c_closes.
    apply (sig_lift_subst_valid droppable_BL Hval).
  Qed.


End StrongCompleteness.

Instance enumT_sum {X Y} :
  enumT X enumT Y enumT (X + Y).
Proof.
  intros .
  exists (fix f n := match n with 0 []
                        | S n f n map inl (L_T X n) map inr (L_T Y n)
                end).
  - eauto.
  - intros [x | y].
    + destruct (el_T x) as [n Hn].
      exists (S n). in_app 2. now in_collect x.
    + destruct (el_T y) as [n Hn].
      exists (S n). in_app 3. now in_collect y.
Qed.