KM.Kripke.kripke_sem

From Stdlib Require Import Arith Lia Ensembles.
Require Import Init.Wf.

Require Import syntax.

Section kripke_sem.

(* We define frames. *)

Definition inverse {X : Type} (R : X -> X -> Prop) (x y : X) : Prop := R y x.

    Class model :=
      {
        (* Nodes *)
        nodes : Type ;

        (* Modal Relation *)
        mreachable : nodes -> nodes -> Prop ;
        inv_mreach_wf : well_founded (inverse mreachable) ;

        (* Intuitionistic Relation *)
        ireachable : nodes -> nodes -> Prop ;
        ireach_refl u : ireachable u u ;
        ireach_tran u v w : ireachable u v -> ireachable v w -> ireachable u w ;

        (* Interaction relations *)
        mreach_irrefl_ireach u v : mreachable u v <-> (u <> v /\ ireachable u v) ;

        (* Valuation *)
        val : nodes -> nat -> Prop ;
        persist : forall u v, ireachable u v -> forall p, val u p -> val v p
      }.

Lemma mreach_tran (M : model) :
    forall u v w, mreachable u v -> mreachable v w -> mreachable u w.
Proof.
intros. apply mreach_irrefl_ireach.
split ; [ | apply mreach_irrefl_ireach in H, H0 ; destruct H,H0 ; apply ireach_tran with v ; auto].
intro ; subst.
revert v w H H0.
apply (Fix inv_mreach_wf (fun v => forall w : nodes, mreachable w v -> mreachable v w -> False)).
intros. apply H with w x ; auto.
Qed.

Lemma mreach_irrefl (M : model) :
    forall u, ~ mreachable u u.
Proof.
apply (Fix inv_mreach_wf (fun u => ~ mreachable u u)).
intros u H H0. apply H with u ; auto.
Qed.

Definition next M w v := (@ireachable M) w v /\ w <> v.

(* We can now define the notion of forcing, which interprets
    formulas in points of models. *)

Fixpoint forces (M: model) w (φ : form) : Prop :=
match φ with
  | Var p => val w p
  | Bot => False
  | ψ ∧ χ => (forces M w ψ) /\ (forces M w χ)
  | ψ ∨ χ => (forces M w ψ) \/ (forces M w χ)
  | ψ → χ => forall v, ireachable w v -> forces M v ψ -> forces M v χ
  | Box ψ => forall v, ireachable w v -> forall u, mreachable v u -> forces M u ψ
end.

(* Persistence holds in our semantics. *)

  Lemma Persistence : forall A M w, forces M w A ->
              (forall v, ireachable w v -> forces M v A).
  Proof.
  induction A ; cbn ; intros ; subst ; auto.
  - apply persist with w ; auto.
  - inversion H ; split. apply IHA1 with (w:=w) ; auto.
    apply IHA2 with (w:=w) ; auto.
  - inversion H. left. apply IHA1 with (w:=w) ; auto.
    right. apply IHA2 with (w:=w) ; auto.
  - apply H with (v:=v0) ; auto. apply ireach_tran with v ; auto.
  - apply H with v0 ; auto. apply ireach_tran with v ; auto.
  Qed.

(* We define the local and global
    semantic consequence relations. *)

  Definition loc_conseq (Γ : Ensemble form) (φ : form) :=
  forall M w, (forall ψ, (In _ Γ ψ) -> forces M w ψ) -> (forces M w φ).

  Definition glob_conseq (Γ : Ensemble form) (φ : form) :=
  forall M, (forall w ψ, (In _ Γ ψ) -> forces M w ψ) -> (forall w, forces M w φ).

End kripke_sem.