Require Import Undecidability.FOL.Semantics.Tarski.FragmentFacts.
Require Export Undecidability.FOL.Semantics.Tarski.FragmentCore.
Require Export Undecidability.FOL.Syntax.Facts.
From Undecidability Require Import Shared.ListAutomation.
Import ListAutomationNotations.

Set Default Proof Using "Type".

Local Set Implicit Arguments.
Local Unset Strict Implicit.

Local Notation vec := Vector.t.

#[local] Ltac comp := repeat (progress (cbn in *; autounfold in *)).

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 ;
        

        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_theo (T : form Prop) phi :=
     D (M : kmodel D) u rho, ( psi, T ksat u ) ksat u .

  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 {_ _ _ _ _} _ _ _, {_ _ _} _ {_} _ _ _.

Section Bottom.

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

  Context {domain : Type}.
  Context {M : kmodel domain}.
  Program Definition kmodel_bot
    (F_P : @nodes _ _ _ M Prop)
    (mon_F : u v, reachable u v F_P u F_P v)
     : @kmodel Σ_funcs (@Σ_preds_bot Σ_preds) domain := {|
    nodes := @nodes _ _ _ M ;
    reachable := @reachable _ _ _ M ;
    k_interp := interp_bot False (@k_interp _ _ _ M) ;
    k_P := n P match P with inl _ _ F_P n | inr P' @k_P _ _ _ M n P' end
  |}.
  Next Obligation. apply reach_refl. Qed.
  Next Obligation. now apply reach_tran with v. Qed.
  Next Obligation. destruct P as [|P'].
    + now apply mon_F with u.
    + now apply mon_P with u.
  Qed.


  Definition ksat_bot
    {ff : falsity_flag} (F_P : @nodes _ _ _ M Prop)
    (mon_F : u v, reachable u v F_P u F_P v)
    u (rho : env domain) (phi : form) : Prop
    := @ksat _ Σ_preds_bot domain (kmodel_bot mon_F) falsity_off u (falsity_to_pred ).
  Arguments ksat_bot {_} _ _ _ _.

  Lemma sat_bot_False {ff:falsity_flag} u rho phi
    (e : u v, reachable u v False False)
    : @ksat_bot ff ( _ False) e u @ksat _ _ domain M ff u .
  Proof.
    induction in ,u|-*.
    - easy.
    - easy.
    - destruct . unfold sat_bot, falsity_to_pred in *. cbn.
      split; intros H v Hreach %; apply ; now apply H, .
    - destruct q. unfold sat_bot, falsity_to_pred in *. cbn.
      split; intros H d; apply IHphi, H.
  Qed.


End Bottom.

Arguments ksat_bot {_} {_} {_} {_} {_} _ _ _ _.

Section BottomDef.

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

  Context {ff : falsity_flag}.

  Definition kexploding D (M : kmodel D) F_P mon_F := v rho phi, ksat_bot F_P mon_F v ( ).
  Arguments kexploding _ _ _ _ : clear implicits.
  Definition kvalid_exploding_ctx A phi :=
     D (M : kmodel D) F_P mon_F u rho, kexploding D M F_P mon_F ( psi, A ksat_bot F_P mon_F u ) ksat_bot F_P mon_F u .

  Definition kvalid_exploding phi :=
     D (M : kmodel D) F_P mon_F u rho, kexploding D M F_P mon_F ksat_bot F_P mon_F u .

  Definition ksatis_exploding phi :=
     D (M : kmodel D) F_P mon_F u rho, kexploding D M F_P mon_F ksat_bot F_P mon_F u .

End BottomDef.