Constructive Analysis of Completeness Theorems


Require Export Gentzen.
Require Export Kripke.
Require Export GenCompleteness.
Require Export Stability.

Exploding and Minimal Models


Section KripkeCompleteness.
  Context { : Signature}.

  Hint Constructors sprv.

  Instance universal_interp : interp term :=
    {| i_f := Func ; i_F := False ; i_P := fun _ _ => False |}.

  Lemma universal_interp_eval t :
    eval t = t[].
  Proof.
    induction t using strong_term_ind; comp; asimpl; try congruence. f_equal.
  Qed.


  Section Contexts.
    Context {b : bottom}.

    Instance K_ctx : kmodel term :=
      {|
        reachable := @incl form ;
        k_interp := universal_interp ;
        k_P := fun A P v => sprv b A None (Pred P v) ;
        k_Bot := fun A => sprv b A None
      |}.
    Proof.
      1,3,4: abstract (eauto using seq_Weak).
      - abstract (intuition; now apply (incl_tran H)).
    Defined.


    Lemma K_ctx_correct (A : list form) :
      ( ⊨(A, K_ctx ) A S [])
      (( B , A B B ;; [] s B S ) ⊨(A, K_ctx) ).
    Proof.
      revert A ; enough (( A , ⊨( A, K_ctx) A S []) ( A , ( B , A B B;; [] s B S ) ⊨( A, K_ctx) )) by intuition.
      induction as [| | [ ] [ ] | [ ]]; cbn; asimpl; split; intros A .
      - tauto.
      - eauto.
      - now rewrite (vec_ext (fun x universal_interp_eval x)).
      - rewrite (vec_ext (fun x universal_interp_eval x)). eauto.
      - intros Hsat. apply IR, . apply Hsat, . 1: intuition. eauto.
      - intros H B HB Hphi % . apply . intros C HC Hxi. apply H.
        1: now transitivity B. eauto using seq_Weak.
      - intros Hsat. apply AllR. pose ( := subst_form (var_term 0 .: ( subst_term (S var_term))) ).
        destruct (find_unused_L ( :: A)). eapply seq_nameless_equiv with (n := x) ( := ).
        + intros Hxi. apply u. constructor. intuition.
        + apply u. omega. intuition.
        + asimpl. apply . rewrite ksat_ext. 2: reflexivity. now apply Hsat.
      - intros H t. apply . intros B HB Hpsi. apply H. assumption.
        apply AllL with ( := t). now asimpl in *.
    Qed.


    Corollary K_ctx_sprv A :
       ⊨(A, K_ctx) A S [].
    Proof.
      now destruct (K_ctx_correct A ).
    Qed.


    Corollary K_ctx_ksat A :
      ( B , A B B ;; [] s B S ) ⊨(A, K_ctx) .
    Proof.
      now destruct (K_ctx_correct A ).
    Qed.

  End Contexts.

  Section ExplodingCompleteness.
    Lemma K_ctx_exploding :
      kexploding (@K_ctx expl).
    Proof.
      intros A P v B HB Hbot % K_ctx_sprv. apply K_ctx_ksat.
      intros B' HB' Hprv. comp. eauto using seq_Weak.
    Qed.


    Lemma K_exp_completeness A :
      A KE A SE .
    Proof.
      intros Hsat. erewrite idSubst_form. apply K_ctx_sprv with ( := ids). 2: reflexivity.
      apply Hsat. 1: apply K_ctx_exploding. intros Hpsi. apply K_ctx_ksat. intros B HB Hxi.
      asimpl in Hxi. eauto.
    Qed.


    Lemma K_exp_seq_ksoundness A :
      A SE A KE .
    Proof.
      intros H % seq_ND. apply @ksoundness with (b := expl). 2: apply H. firstorder.
    Qed.

  End ExplodingCompleteness.

  Section BottomlessCompleteness.
    Lemma K_bottomless_completeness A :
      A KBL A SL .
    Proof.
      intros Hsat. erewrite idSubst_form. apply K_ctx_sprv with ( := ids). 2: reflexivity.
      apply Hsat. 1: apply I. intros Hpsi. apply K_ctx_ksat. intros B HB Hxi.
      asimpl in Hxi. eauto.
    Qed.

  End BottomlessCompleteness.

Standard Models


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

    Variable sprv_stab : A , stable (sprv expl A ).

    Definition cons A := A SE .
    Definition cons_ctx := { A | cons A }.
    Definition ctx_incl (A B : cons_ctx) := incl (proj1_sig A) (proj1_sig B).

    Hint Unfold cons cons_ctx ctx_incl.

    Notation "A <<=C B" := (ctx_incl A B) (at level 20).
    Notation "A ⊢SC phi" := (proj1_sig A SE ) (at level 20).
    Notation "A ;; psi ⊢sC phi" := (proj1_sig A ;; sE ) (at level 20).

    Ltac dest_con_ctx :=
      match goal with
      | [ |- u : cons_ctx, _] let Hu := fresh "H" u in intros [u Hu]
      | [ A : cons_ctx |- _] let HA := fresh "H" A in destruct A as [A HA]
      end.

    Ltac cctx := repeat (progress dest_con_ctx); comp.

    Hint Extern 1 cctx.

    Instance K_std : kmodel term :=
      {|
        reachable := ctx_incl ;
        k_interp := universal_interp ;
        k_P := fun A P v => A SC (Pred P v) ;
        k_Bot := fun A => A SC
      |}.
    Proof.
      - abstract eauto.
      - abstract (cctx; firstorder).
      - abstract (eauto using seq_Weak).
      - abstract (cctx; firstorder).
    Defined.


    Lemma nsprv_cons A :
      ( H, (exist cons A H) SC ) A SE .
    Proof.
      intros Hcon. apply sprv_stab. intros H. apply H. eauto.
    Qed.


    Lemma K_std_correct (A : cons_ctx) :
      ( ⊨(A, K_std) A SC [])
      (( B , A C B B ;; [] sC B SC ) ⊨(A, K_std) ).
    Proof.
      revert A ; enough (( A , ⊨( A, K_std) A SC []) ( A , ( B , A C B B;; [] sC B SC ) ⊨( A, K_std) )) by intuition.
      induction as [| | [ ] [ ] | [ ]].
      all: cbn; asimpl; split; intros A .
      - tauto.
      - intros H. apply H; eauto.
      - now rewrite (vec_ext (fun x universal_interp_eval x)).
      - rewrite (vec_ext (fun x universal_interp_eval x)). intros H. apply H; eauto.
      - intros Hsat. apply IR. apply nsprv_cons. intros Hcon. apply , Hsat, ; cctx.
        1: intuition. eauto.
      - intros H B HB Hphi % . apply . intros C HC Hxi. apply H; cctx.
        1: now transitivity B. eauto using seq_Weak.
      - pose ( := subst_form (var_term 0 .: ( subst_term (S var_term))) ).
        intros Hsat. apply AllR. cctx. destruct (find_unused_L ( :: A)).
        eapply seq_nameless_equiv with (n := x) ( := ).
        + intros Hxi. apply u. constructor. intuition.
        + apply u. omega. intuition.
        + asimpl. apply ( (exist cons A HA)). 1: rewrite ksat_ext. 2: reflexivity. now apply Hsat.
      - intros H t. apply . intros B HB Hpsi. apply H. assumption.
        apply AllL with ( := t). now asimpl in *.
    Qed.


    Corollary K_std_sprv A :
       ⊨(A, K_std) A SC [].
    Proof.
      now destruct (K_std_correct A ).
    Qed.


    Corollary K_std_ksat A :
      ( B , A C B B ;; [] sC B SC ) ⊨(A, K_std) .
    Proof.
      now destruct (K_std_correct A ).
    Qed.


    Lemma K_std_standard :
      kstandard K_std.
    Proof.
      intros []. apply c.
    Qed.


    Lemma K_std_completeness A :
      A KS A SE .
    Proof.
      intros Hsat. erewrite idSubst_form. apply nsprv_cons. intros H. apply K_std_sprv with ( := ids).
      2: reflexivity. apply Hsat. 1: apply K_std_standard. intros Hpsi. apply K_std_ksat.
      intros B HB Hxi. asimpl in Hxi. eauto.
    Qed.


    Lemma K_std_seq_ksoundness A :
      A SE A KS .
    Proof.
      intros H % seq_ND. apply @ksoundness with (b := expl). 2: apply H. firstorder.
    Qed.

  End StandardCompleteness.

  Section MPRequired.
    Variable C : stab_class.
    Hypothesis HC : map_closed C dnt.
    Variable K_completeness : T , C T kvalid_T kstandard T T SE .

    Lemma cend_dn T :
      C T T CE T CE .
    Proof.
      intros HT Hdn. apply DN_T, dnt_to_TCE. cbn. apply (@seq_ND_T _ _ (tmap dnt T) (¬ dnt ))).
      apply K_completeness. 1: apply HC, HT. intros D M St u HT' v Hv Hn. contradict Hdn. intros Hphi % dnt_to_TIE.
      apply strong_ksoundness with ( := kstandard) in Hphi. apply (St v), Hn. 1: reflexivity.
      2: intros; apply kstandard_explodes. 1: apply (Hphi D M St v ).
      intros Hpsi % HT'. apply (ksat_mon Hv Hpsi).
    Qed.

  End MPRequired.
End KripkeCompleteness.