KM.Kripke.soundness

From Stdlib Require Import List Arith Lia Ensembles.
Export ListNotations.

Require Import syntax.
Require Import KMH_export.
Require Import kripke_sem.

Axiom LEM : forall P, P \/ ~ P.
(* We actually only need decidable equality on nodes and
  decidability of the forcing relation *)

Section soundness.

(* We can show that all axioms of KM are valid on all
    models of our semantics. *)

Lemma Ax_valid : forall A, Axioms A ->
  (forall M w, forces M w A).
Proof.
intros A Ax. destruct Ax as [Ax | Ax].
(* Intuitionistic axioms *)
+ inversion Ax ; cbn ; intros ; subst ; cbn ; intros ; auto.
  - apply Persistence with (w:=v) ; auto.
  - apply H0 with v1 ; auto. apply ireach_tran with v0 ; auto. apply ireach_refl.
  - destruct H4 ; auto. apply H0 ; auto. apply ireach_tran with v0 ; auto.
  - destruct H0 ; auto.
  - destruct H0 ; auto.
  - split. apply H0 ; auto. apply ireach_tran with v0 ; auto. apply H2 ; auto.
  - subst. contradiction.
(* Modal axioms *)
+ inversion Ax ; cbn ; intros ; subst ; cbn ; intros.
  (* K *)
  - apply H0 with v1 u ; auto. apply ireach_tran with v0 ; auto. apply ireach_refl.
    apply H2 with v1 ; auto.
  (* L *)
  - revert v H H0.
    apply (well_founded_ind inv_mreach_wf (fun v => ireachable w v ->
    (forall v0 : nodes, ireachable v v0 -> (forall v1 : nodes,
    ireachable v0 v1 -> forall u : nodes, mreachable v1 u -> forces M u A0) ->
    forces M v0 A0) -> forces M v A0)).
    intros x H0 iwx H1. apply H1 ; try apply ireach_refl.
    intros y ixy z myz.
    destruct (LEM (x = y)) ; subst.
    * apply H0 in myz ; auto.
      ++ apply ireach_tran with y ; auto. apply mreach_irrefl_ireach in myz ; destruct myz ; auto.
      ++ intros. apply H1 ; auto.
         apply ireach_tran with z ; auto. apply mreach_irrefl_ireach in myz ; destruct myz ; auto.
    * apply H0.
      ++ apply mreach_tran with y ; auto. apply mreach_irrefl_ireach ; split ; auto.
      ++ apply ireach_tran with x ; auto. apply ireach_tran with y ; auto.
         apply mreach_irrefl_ireach in myz ; destruct myz ; auto.
      ++ intros. apply H1 ; auto. apply ireach_tran with y ; auto.
         apply ireach_tran with z ; auto. apply mreach_irrefl_ireach in myz ; destruct myz ; auto.
  (* NA *)
  - edestruct (LEM (forces M v B)) as [P | NP] ; [ left ; auto | ].
    right. intros. apply H0 with v ; auto.
    * apply ireach_refl.
    * apply mreach_irrefl_ireach. split ; auto.
      intro ; subst ; auto.
Qed.

Theorem lKM_Soundness : forall Γ phi, (KMH_prv Γ phi) -> (loc_conseq Γ phi).
Proof.
intros Γ phi D. induction D ; intros M w Hw.
(* Id *)
- apply Hw ; auto.
(* Ax *)
- apply Ax_valid ; destruct H ; firstorder.
(* MP *)
- unfold loc_conseq in *. cbn in *. apply IHD1 with w ; auto. apply ireach_refl.
(* Nec *)
- subst. unfold loc_conseq in *. cbn in *. intros. apply IHD ; auto.
  intros ; contradiction.
Qed.

Theorem gKM_Soundness : forall Γ phi, (gKMH_prv Γ phi) -> (glob_conseq Γ phi).
Proof.
intros Γ phi D. induction D ; intros M HΓ w.
(* Id *)
- apply HΓ ; auto.
(* Ax *)
- apply Ax_valid ; destruct H ; firstorder.
(* MP *)
- unfold glob_conseq in *. cbn in *. apply IHD1 with w ; auto. apply ireach_refl.
(* Nec *)
- subst. unfold glob_conseq in *. cbn in *. intros. apply IHD ; auto.
Qed.

End soundness.