Require Export Gentzen.
Require Export Kripke.
Require Export GenCompleteness.
Require Export Stability.
Section KripkeCompleteness.
Context {Sigma : Signature}.
Hint Constructors sprv.
Instance universal_interp : interp term :=
{| i_f := Func ; i_F := False ; i_P := fun _ _ => False |}.
Lemma universal_interp_eval rho t :
eval rho t = t[rho].
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) rho phi :
(rho ⊨(A, K_ctx ) phi -> A ⊢S phi[rho]) /\
((forall B psi, A <<= B -> B ;; phi[rho] ⊢s psi -> B ⊢S psi) -> rho ⊨(A, K_ctx) phi).
Proof.
revert A rho; enough ((forall A rho, rho ⊨( A, K_ctx) phi -> A ⊢S phi[rho]) /\ (forall A rho, (forall B psi, A <<= B -> B;; phi[rho] ⊢s psi -> B ⊢S psi) -> rho ⊨( A, K_ctx) phi)) by intuition.
induction phi as [| t1 t2 | phi [IHphi1 IHphi2] psi [IHpsi1 IHpsi2] | phi [IHphi1 IHphi2]]; cbn; asimpl; split; intros A rho.
- tauto.
- eauto.
- now rewrite (vec_ext (fun x => universal_interp_eval rho x)).
- rewrite (vec_ext (fun x => universal_interp_eval rho x)). eauto.
- intros Hsat. apply IR, IHpsi1. apply Hsat, IHphi2. 1: intuition. eauto.
- intros H B HB Hphi % IHphi1. apply IHpsi2. intros C xi HC Hxi. apply H.
1: now transitivity B. eauto using seq_Weak.
- intros Hsat. apply AllR. pose (phi' := subst_form (var_term 0 .: (rho >> subst_term (S >> var_term))) phi).
destruct (find_unused_L (phi' :: A)). eapply seq_nameless_equiv with (n := x) (phi0 := phi').
+ intros xi Hxi. apply u. constructor. intuition.
+ apply u. omega. intuition.
+ asimpl. apply IHphi1. rewrite ksat_ext. 2: reflexivity. now apply Hsat.
- intros H t. apply IHphi2. intros B psi HB Hpsi. apply H. assumption.
apply AllL with (t0 := t). now asimpl in *.
Qed.
Corollary K_ctx_sprv A rho phi :
rho ⊨(A, K_ctx) phi -> A ⊢S phi[rho].
Proof.
now destruct (K_ctx_correct A rho phi).
Qed.
Corollary K_ctx_ksat A rho phi :
(forall B psi, A <<= B -> B ;; phi[rho] ⊢s psi -> B ⊢S psi) -> rho ⊨(A, K_ctx) phi.
Proof.
now destruct (K_ctx_correct A rho phi).
Qed.
End Contexts.
Section ExplodingCompleteness.
Lemma K_ctx_exploding :
kexploding (@K_ctx expl).
Proof.
intros A rho P v B HB Hbot % K_ctx_sprv. apply K_ctx_ksat.
intros B' psi HB' Hprv. comp. eauto using seq_Weak.
Qed.
Lemma K_exp_completeness A phi :
A ⊫KE phi -> A ⊢SE phi.
Proof.
intros Hsat. erewrite <-idSubst_form. apply K_ctx_sprv with (rho := ids). 2: reflexivity.
apply Hsat. 1: apply K_ctx_exploding. intros psi Hpsi. apply K_ctx_ksat. intros B xi HB Hxi.
asimpl in Hxi. eauto.
Qed.
Lemma K_exp_seq_ksoundness A phi :
A ⊢SE phi -> A ⊫KE phi.
Proof.
intros H % seq_ND. apply @ksoundness with (b := expl). 2: apply H. firstorder.
Qed.
End ExplodingCompleteness.
Section BottomlessCompleteness.
Lemma K_bottomless_completeness A phi :
A ⊫KBL phi -> A ⊢SL phi.
Proof.
intros Hsat. erewrite <-idSubst_form. apply K_ctx_sprv with (rho := ids). 2: reflexivity.
apply Hsat. 1: apply I. intros psi Hpsi. apply K_ctx_ksat. intros B xi HB Hxi.
asimpl in Hxi. eauto.
Qed.
End BottomlessCompleteness.
Section StandardCompleteness.
Context {HdF : eq_dec Funcs} {HdP : eq_dec Preds}.
Context {HeF : enumT Funcs} {HeP : enumT Preds}.
Variable sprv_stab : forall A psi phi, stable (sprv expl A psi phi).
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 phi) (at level 20).
Notation "A ;; psi ⊢sC phi" := (proj1_sig A ;; psi ⊢sE phi) (at level 20).
Ltac dest_con_ctx :=
match goal with
| [ |- forall 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 phi :
(forall H, (exist cons A H) ⊢SC phi) -> A ⊢SE phi.
Proof.
intros Hcon. apply sprv_stab. intros H. apply H. eauto.
Qed.
Lemma K_std_correct (A : cons_ctx) rho phi :
(rho ⊨(A, K_std) phi -> A ⊢SC phi[rho]) /\
((forall B psi, A <<=C B -> B ;; phi[rho] ⊢sC psi -> B ⊢SC psi) -> rho ⊨(A, K_std) phi).
Proof.
revert A rho; enough ((forall A rho, rho ⊨( A, K_std) phi -> A ⊢SC phi[rho]) /\ (forall A rho, (forall B psi, A <<=C B -> B;; phi[rho] ⊢sC psi -> B ⊢SC psi) -> rho ⊨( A, K_std) phi)) by intuition.
induction phi as [| t1 t2 | phi [IHphi1 IHphi2] psi [IHpsi1 IHpsi2] | phi [IHphi1 IHphi2]].
all: cbn; asimpl; split; intros A rho.
- tauto.
- intros H. apply H; eauto.
- now rewrite (vec_ext (fun x => universal_interp_eval rho x)).
- rewrite (vec_ext (fun x => universal_interp_eval rho x)). intros H. apply H; eauto.
- intros Hsat. apply IR. apply nsprv_cons. intros Hcon. apply IHpsi1, Hsat, IHphi2; cctx.
1: intuition. eauto.
- intros H B HB Hphi % IHphi1. apply IHpsi2. intros C xi HC Hxi. apply H; cctx.
1: now transitivity B. eauto using seq_Weak.
- pose (phi' := subst_form (var_term 0 .: (rho >> subst_term (S >> var_term))) phi).
intros Hsat. apply AllR. cctx. destruct (find_unused_L (phi' :: A)).
eapply seq_nameless_equiv with (n := x) (phi0 := phi').
+ intros xi Hxi. apply u. constructor. intuition.
+ apply u. omega. intuition.
+ asimpl. apply (IHphi1 (exist cons A HA)). 1: rewrite ksat_ext. 2: reflexivity. now apply Hsat.
- intros H t. apply IHphi2. intros B psi HB Hpsi. apply H. assumption.
apply AllL with (t0 := t). now asimpl in *.
Qed.
Corollary K_std_sprv A rho phi :
rho ⊨(A, K_std) phi -> A ⊢SC phi[rho].
Proof.
now destruct (K_std_correct A rho phi).
Qed.
Corollary K_std_ksat A rho phi :
(forall B psi, A <<=C B -> B ;; phi[rho] ⊢sC psi -> B ⊢SC psi) -> rho ⊨(A, K_std) phi.
Proof.
now destruct (K_std_correct A rho phi).
Qed.
Lemma K_std_standard :
kstandard K_std.
Proof.
intros []. apply c.
Qed.
Lemma K_std_completeness A phi :
A ⊫KS phi -> A ⊢SE phi.
Proof.
intros Hsat. erewrite <-idSubst_form. apply nsprv_cons. intros H. apply K_std_sprv with (rho := ids).
2: reflexivity. apply Hsat. 1: apply K_std_standard. intros psi Hpsi. apply K_std_ksat.
intros B xi HB Hxi. asimpl in Hxi. eauto.
Qed.
Lemma K_std_seq_ksoundness A phi :
A ⊢SE phi -> A ⊫KS phi.
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 : forall T phi, C T -> kvalid_T kstandard T phi -> T ⊩SE phi.
Lemma cend_dn T phi :
C T -> ~ ~ T ⊩CE phi -> T ⊩CE phi.
Proof.
intros HT Hdn. apply DN_T, dnt_to_TCE. cbn. apply (@seq_ND_T _ _ (tmap dnt T) (¬ (¬ dnt phi))).
apply K_completeness. 1: apply HC, HT. intros D M St u rho HT' v Hv Hn. contradict Hdn. intros Hphi % dnt_to_TIE.
apply strong_ksoundness with (C0 := kstandard) in Hphi. apply (St v), Hn. 1: reflexivity.
2: intros; apply kstandard_explodes. 1: apply (Hphi D M St v rho).
intros psi Hpsi % HT'. apply (ksat_mon Hv Hpsi).
Qed.
End MPRequired.
End KripkeCompleteness.