FObiint.FO_BiInt_soundness
Require Import List.
Require Import Ensembles.
Require Import Lia.
Require Import FO_BiInt_Syntax.
Require Import FO_BiInt_GHC.
Require Import FO_BiInt_Kripke_sem.
Local Set Implicit Arguments.
Local Unset Strict Implicit.
(* ** Soundness **)
Section Soundness_LEM.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Axiom LEM : forall P, P \/ ~ P.
Lemma ksat_dec : forall A D (M : kmodel D) u rho,
(@ksat _ _ D M u rho A) \/ ((ksat u rho A) -> False).
Proof.
intros. apply LEM.
Qed.
Lemma Ax_valid : forall A, Axioms A -> kvalid A.
Proof.
intros A AX. inversion AX ; subst ; intros w M u rho ; cbn ; intros ; auto.
- apply ksat_mon with v ; auto.
- apply H0 with v1 ; auto. apply reach_tran with v0 ; auto. apply reach_refl.
- destruct H4. apply H0 ; auto. apply (reach_tran H1 H3). apply H2 ; auto.
- destruct H0 ; auto.
- destruct H0 ; auto.
- split. apply H0 ; auto. apply (reach_tran H1 H3). apply H2 ; auto.
- inversion H0.
(* Bi int axioms *)
- destruct (ksat_dec B v rho) ; auto. right. intro H2.
apply H1. apply H2 ; auto. apply reach_refl.
- intros H1. apply H0. intros. apply H1 with v0 ; auto. apply reach_refl.
- intro. apply H0. intros.
pose (ksat_dec C v0 rho). destruct o ; auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ ksat v rho A0 /\ ~ ksat v rho B) \/ ~ (exists v, reachable v v0 /\ ksat v rho A0 /\ ~ ksat v rho B))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply ksat_mon with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (ksat_dec B v1 rho).
destruct o. auto. contradict H6. now exists v1.
- pose (@H0 v0 H1). pose (ksat_dec B v0 rho).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
(* Quantifiers *)
- apply H0 ; auto. apply ksat_comp ; auto.
- apply ksat_comp. unfold funcomp. eapply (ksat_ext v). 2: eapply (H0 (eval rho _)).
intros. unfold scons. destruct x ; auto.
- apply ksat_comp in H0. eexists (eval rho t). eapply (ksat_ext v). 2: eapply H0.
unfold funcomp. intros. unfold scons. destruct x ; auto.
Qed.
Lemma Soundness : forall Γ A, FOBIH_prv Γ A -> loc_conseq Γ A.
Proof.
intros Γ A Hprv. induction Hprv; subst; cbn; intros D M u rho HX.
(* Id *)
- apply HX ; auto.
(* Ax *)
- apply Ax_valid ; auto.
(* MP *)
- unfold kvalid_ctx in IHHprv1,IHHprv2. pose (IHHprv1 _ _ _ _ HX). pose (IHHprv2 _ _ _ _ HX).
simpl in k. apply k ; auto. apply reach_refl.
(* DN *)
- cbn. intros.
assert (J1: kvalid_ctx (Empty_set _) A). apply IHHprv.
apply H0. intros. apply J1 ; auto. intros. inversion H3.
(* Gen *)
- intro d. unfold kvalid_ctx in IHHprv. apply IHHprv. intros. inversion H. destruct H0 ; subst.
apply HX in H1. apply ksat_comp. simpl. unfold funcomp. simpl. auto.
(* EC *)
- intros w Ha0 Ha1. unfold loc_conseq in IHHprv. destruct Ha1.
assert (J2: forall psi : form, (fun x : form => exists B : form, x = B[↑] /\ In form Γ B) psi -> (u ⊩( M, D) (x .: rho)) psi). intros.
destruct H0. destruct H0. subst. apply HX in H1. apply ksat_comp.
simpl. unfold funcomp. simpl. auto. pose (IHHprv _ _ u (x .: rho) J2).
simpl in k. apply k in H ; auto. apply ksat_comp in H. unfold funcomp in H. simpl in H. auto.
Qed.
End Soundness_LEM.
Require Import Ensembles.
Require Import Lia.
Require Import FO_BiInt_Syntax.
Require Import FO_BiInt_GHC.
Require Import FO_BiInt_Kripke_sem.
Local Set Implicit Arguments.
Local Unset Strict Implicit.
(* ** Soundness **)
Section Soundness_LEM.
Context {Σ_funcs : funcs_signature}.
Context {Σ_preds : preds_signature}.
Axiom LEM : forall P, P \/ ~ P.
Lemma ksat_dec : forall A D (M : kmodel D) u rho,
(@ksat _ _ D M u rho A) \/ ((ksat u rho A) -> False).
Proof.
intros. apply LEM.
Qed.
Lemma Ax_valid : forall A, Axioms A -> kvalid A.
Proof.
intros A AX. inversion AX ; subst ; intros w M u rho ; cbn ; intros ; auto.
- apply ksat_mon with v ; auto.
- apply H0 with v1 ; auto. apply reach_tran with v0 ; auto. apply reach_refl.
- destruct H4. apply H0 ; auto. apply (reach_tran H1 H3). apply H2 ; auto.
- destruct H0 ; auto.
- destruct H0 ; auto.
- split. apply H0 ; auto. apply (reach_tran H1 H3). apply H2 ; auto.
- inversion H0.
(* Bi int axioms *)
- destruct (ksat_dec B v rho) ; auto. right. intro H2.
apply H1. apply H2 ; auto. apply reach_refl.
- intros H1. apply H0. intros. apply H1 with v0 ; auto. apply reach_refl.
- intro. apply H0. intros.
pose (ksat_dec C v0 rho). destruct o ; auto. exfalso.
assert (~ ~ ((exists v, reachable v v0 /\ ksat v rho A0 /\ ~ ksat v rho B) \/ ~ (exists v, reachable v v0 /\ ksat v rho A0 /\ ~ ksat v rho B))) by tauto.
apply H5. intros [(v1 & H6 & H7 & H8)|H6].
+ apply H1 in H7 as [H7|H7]; try tauto.
* apply H4. now apply ksat_mon with v1.
* now apply reach_tran with v0.
+ apply H3. intros. pose (ksat_dec B v1 rho).
destruct o. auto. contradict H6. now exists v1.
- pose (@H0 v0 H1). pose (ksat_dec B v0 rho).
destruct o ; auto.
exfalso. apply f. intro. apply H3, H4; trivial. apply reach_refl.
(* Quantifiers *)
- apply H0 ; auto. apply ksat_comp ; auto.
- apply ksat_comp. unfold funcomp. eapply (ksat_ext v). 2: eapply (H0 (eval rho _)).
intros. unfold scons. destruct x ; auto.
- apply ksat_comp in H0. eexists (eval rho t). eapply (ksat_ext v). 2: eapply H0.
unfold funcomp. intros. unfold scons. destruct x ; auto.
Qed.
Lemma Soundness : forall Γ A, FOBIH_prv Γ A -> loc_conseq Γ A.
Proof.
intros Γ A Hprv. induction Hprv; subst; cbn; intros D M u rho HX.
(* Id *)
- apply HX ; auto.
(* Ax *)
- apply Ax_valid ; auto.
(* MP *)
- unfold kvalid_ctx in IHHprv1,IHHprv2. pose (IHHprv1 _ _ _ _ HX). pose (IHHprv2 _ _ _ _ HX).
simpl in k. apply k ; auto. apply reach_refl.
(* DN *)
- cbn. intros.
assert (J1: kvalid_ctx (Empty_set _) A). apply IHHprv.
apply H0. intros. apply J1 ; auto. intros. inversion H3.
(* Gen *)
- intro d. unfold kvalid_ctx in IHHprv. apply IHHprv. intros. inversion H. destruct H0 ; subst.
apply HX in H1. apply ksat_comp. simpl. unfold funcomp. simpl. auto.
(* EC *)
- intros w Ha0 Ha1. unfold loc_conseq in IHHprv. destruct Ha1.
assert (J2: forall psi : form, (fun x : form => exists B : form, x = B[↑] /\ In form Γ B) psi -> (u ⊩( M, D) (x .: rho)) psi). intros.
destruct H0. destruct H0. subst. apply HX in H1. apply ksat_comp.
simpl. unfold funcomp. simpl. auto. pose (IHHprv _ _ u (x .: rho) J2).
simpl in k. apply k in H ; auto. apply ksat_comp in H. unfold funcomp in H. simpl in H. auto.
Qed.
End Soundness_LEM.