(* * Kripke Semantics *)

From Undecidability Require Import FOL.Util.Deduction FOL.Util.Tarski FOL.Util.Syntax.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.
Local Set Implicit Arguments.
Local Unset Strict Implicit.

Local Notation vec := Vector.t.

Section Kripke.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Section Model.

    Variable domain : Type.

    Class kmodel :=
      {
        nodes : Type ;

        reachable : nodes nodes Prop ;
        reach_refl u : reachable u u ;
        reach_tran u v w : reachable u v reachable v w reachable u w ;

        k_interp : interp domain ;
        k_P : nodes P : preds, Vector.t domain (ar_preds P) Prop ;
        (* k_Bot : nodes -> Prop ; *)

        mon_P : u v, reachable u v P (t : Vector.t domain (ar_preds P)), k_P u t k_P v t;
      }.

    Variable M : kmodel.

    Fixpoint ksat {ff : falsity_flag} u (rho : domain) (phi : form) : Prop :=
      match with
      | atom P v k_P u (Vector.map (@eval _ _ _ k_interp ) v)
      | falsity False
      | bin Impl v, reachable u v ksat v ksat v
      | quant All j : domain, ksat u (j .: )
      end.

    Lemma ksat_mon {ff : falsity_flag} (u : nodes) (rho : domain) (phi : form) :
       v (H : reachable u v), ksat u ksat v .
    Proof.
      revert .
      induction ; intros v' H; cbn; try destruct ; try destruct q; intuition; eauto using mon_P, reach_tran.
    Qed.


    Lemma ksat_iff {ff : falsity_flag} u rho phi :
      ksat u v (H : reachable u v), ksat v .
    Proof.
      split.
      - intros v . eapply ksat_mon; eauto.
      - intros H. apply H. eapply reach_refl.
    Qed.

  End Model.

  Notation "rho '⊩(' u ')' phi" := (ksat _ u ) (at level 20).
  Notation "rho '⊩(' u , M ')' phi" := (@ksat _ M _ u ) (at level 20).
  Arguments ksat {_ _ _} _ _ _, _ _ _ _ _ _.

  Hint Resolve reach_refl : core.

  Section Substs.

    Variable D : Type.
    Context {M : kmodel D}.

    Lemma ksat_ext {ff : falsity_flag} u rho xi phi :
      ( x, x = x) ⊩(u,M) ⊩(u,M) .
    Proof.
      induction as [ | b P v | | ] in , , u |-*; intros Hext; comp.
      - tauto.
      - erewrite Vector.map_ext. reflexivity. intros t. now apply eval_ext.
      - destruct ; split; intros H v Hv Hv'; now apply ( v Hext), (H _ Hv), ( v Hext).
      - destruct q; split; intros H d; apply (IHphi _ (d .: ) (d .: )). all: ((intros []; cbn; congruence) + auto).
    Qed.


    Lemma ksat_comp {ff : falsity_flag} u rho xi phi :
       ⊩(u,M) [] ( >> eval (I := @k_interp _ M)) ⊩(u,M) .
    Proof.
      induction as [ | b P v | | ] in , , u |-*; comp.
      - tauto.
      - erewrite Vector.map_map. erewrite Vector.map_ext. 2: apply eval_comp. reflexivity.
      - destruct . setoid_rewrite . now setoid_rewrite .
      - destruct q. setoid_rewrite IHphi. split; intros H d; eapply ksat_ext. 2, 4: apply (H d).
        all: intros []; cbn; trivial; unfold funcomp; now erewrite eval_comp.
    Qed.


  End Substs.

  Context {ff : falsity_flag}.

  Definition kvalid_ctx A phi :=
     D (M : kmodel D) u rho, ( psi, A ksat u ) ksat u .

  Definition kvalid phi :=
     D (M : kmodel D) u rho, ksat u .

  Definition ksatis phi :=
     D (M : kmodel D) u rho, ksat u .

End Kripke.

Notation "rho '⊩(' u ')' phi" := (ksat u ) (at level 20).
Notation "rho '⊩(' u , M ')' phi" := (@ksat _ _ _ M _ u ) (at level 20).

Arguments ksat {_ _ _ _ _} _ _ _, {_ _ _} _ {_} _ _ _.

(* ** Soundness **)

Section KSoundness.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.
  Context {ff : falsity_flag}.

  Ltac clean_ksoundness :=
    match goal with
    | [ H : ?x = ?x _ |- _ ] specialize (H eq_refl)
    | [ H : (?A ?B), : (?A ?B) _ |- _] specialize ( H)
    end.

  Lemma ksoundness A (phi : form) :
    A I kvalid_ctx A .
  Proof.
    intros Hprv D M. remember intu as s. induction Hprv; subst; cbn; intros u HA.
    all: repeat (clean_ksoundness + discriminate). all: (eauto || comp; eauto).
    - intros v Hr Hpi. eapply IHHprv. intros ? []; subst; eauto using ksat_mon.
    - eapply . 3: eapply . all: eauto. apply M.
    - intros d. apply IHHprv. intros [ [ Hp]] % in_map_iff. cbn. rewrite ksat_comp. apply HA, Hp.
    - rewrite ksat_comp. eapply ksat_ext. 2: eapply (IHHprv u HA (eval t)).
      unfold funcomp. now intros [].
    - now apply IHHprv in HA.
  Qed.


  Lemma ksoundness' (phi : form) :
    [] I kvalid .
  Proof.
    intros H % ksoundness. firstorder.
  Qed.


End KSoundness.

(* ** Connection to Tarski Semantics *)

Section ToTarski.

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Program Instance interp_kripke {domain} (I : interp domain) : kmodel domain :=
    {| nodes := unit ; reachable u v := True |}.
  Next Obligation.
    - now apply I in X.
  Defined.

  Lemma kripke_tarski {ff : falsity_flag} domain (I : interp domain) rho phi :
     ksat (interp_kripke I) tt .
  Proof.
    revert . induction ; intros .
    - tauto.
    - tauto.
    - destruct . cbn. rewrite , . intuition. destruct v. tauto.
    - destruct q. cbn. split; intros H; cbn in *.
      + intros i. apply IHphi, H.
      + intros i. apply IHphi, H.
  Qed.


  Lemma kvalid_valid b (phi : form b) :
    kvalid valid .
  Proof.
    intros H domain I . apply kripke_tarski, H.
  Qed.


  Lemma ksatis_satis b (phi : form b) :
    satis ksatis .
  Proof.
    intros (domain & I & & ?). eapply kripke_tarski in H.
    now exists domain, (interp_kripke I), tt, .
  Qed.


End ToTarski.