Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finset path fingraph.
Require Import Relations.

Require Import tactics base.

Import Prenex Implicits.

Definition var := nat.

Inductive form :=
  Var : var -> form
| NegVar : var -> form
| And : form -> form -> form
| Or : form -> form -> form
| Box : form -> form
| Dia : form -> form
| Bstar : form -> form
| Dstar : form -> form
.

Fixpoint pickle t :=
  match t with
    | Var n => Node (0,n) [::]
    | NegVar n => Node (1,n) [::]
    | And s t => Node (2,2) [:: pickle s ; pickle t]
    | Or s t => Node (3,3) [:: pickle s ; pickle t]
    | Box s => Node (4,4) [:: pickle s ]
    | Dia s => Node (5,5) [:: pickle s ]
    | Bstar s => Node (6,6) [:: pickle s ]
    | Dstar s => Node (7,7) [:: pickle s ]
  end.

Fixpoint unpickle t :=
  match t with
    | Node (O,n) [::] => Some (Var n)
    | Node (1,n) [::] => Some (NegVar n)
    | Node (2,2) [:: s' ; t'] =>
      if unpickle s' is Some s then
        if unpickle t' is Some t then Some (And s t)
          else None else None
    | Node (3,3) [:: s' ; t'] =>
      if unpickle s' is Some s then
        if unpickle t' is Some t then Some (Or s t)
          else None else None
    | Node (4,4) [:: s'] =>
      if unpickle s' is Some s then Some (Box s) else None
    | Node (5,5) [:: s'] =>
      if unpickle s' is Some s then Some (Dia s) else None
    | Node (6,6) [:: s'] =>
      if unpickle s' is Some s then Some (Bstar s) else None
    | Node (7,7) [:: s'] =>
      if unpickle s' is Some s then Some (Dstar s) else None
    | _ => None
  end.

Lemma inv : pcancel pickle unpickle.

Lemma eq_form_dec : forall s t : form , { s = t } + { s <> t}.

Definition form_eqMixin := EqMixin (compareP eq_form_dec).
Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.

Definition form_countMixin := PcanCountMixin inv.
Definition form_choiceMixin := CountChoiceMixin form_countMixin.
Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.

Implicit Arguments clos_refl_trans [A].

Structure model := Model {
  state :> Type;
  trans : rel state;
  label : state -> pred var;
  
  
  exs' : pred state -> bool ;
  exsP (p : pred state) : reflect (exists x, p x) (exs' p);
  trans_star : state -> state -> bool;
  trans_starP w v : reflect (clos_refl_trans trans w v) (trans_star w v)
}.

Implicit Types M : model.

Notation "w ---> v" := (trans w v) (at level 35).
Notation "w --->* v" := (trans_star w v) (at level 35).

Lemma trans_star0 M (w : M) : w --->* w.

Lemma trans_star1 M (w v : M) : w ---> v -> w --->* v.

Lemma trans_star_trans M (w v v' : M) : w --->* v -> v --->* v' -> w --->* v'.

Notation "'exs' w , p" := (exs' (fun w => p)) (at level 200, w ident, right associativity).
Notation "'exs' w : M , p" := (exs' (fun w : M => p))
  (at level 200, w ident, right associativity,
    format "'[' 'exs' '/ ' w : M , '/ ' p ']'") : type_scope.

Definition alls M (p : pred M) := ~~ (@exs' M) (fun x => ~~ p x).

Lemma allsP M (p : pred M) : reflect (forall x , p x) (alls p).

Notation "'alls' w , p" := (alls (fun w => p)) (at level 200, w ident, right associativity).

Lemma not_all_ex (M : model) (p : pred M) : ~~ (alls w , p w) = exs w, ~~ p w.

Lemma not_ex_all (M : model) (p : pred M) : ~~ (exs w , p w) = alls w, ~~ p w.

Reserved Notation "w |= s" (at level 35).
Fixpoint eval M (w:M) s :=
    match s with
    | Var n => label w n
    | NegVar n => ~~ label w n
    | And s t => w |= s && w |= t
    | Or s t => w |= s || w |= t
    | Box s => alls v , w ---> v ==> v |= s
    | Dia s => exs v , w ---> v && v |= s
    | Bstar s => alls v , w --->* v ==> v |= s
    | Dstar s => exs v , w --->* v && v |= s
  end
  where "w |= s" := (eval w s).

Definition valid s := forall M (w : M) , w |= s.
Definition sat s := exists M : model, exists w : M , w |= s.
Definition equiv s t := forall M (w:M) , w |= s = w |= t.

Lemma trans_star_case M (w v : M) : w --->* v -> w = v \/ exists2 v' , w ---> v' & v' --->* v.

Lemma Bstar_Box s : equiv (Bstar s) (And s (Box (Bstar s))).

Lemma Dstar_Dia s : equiv (Dstar s) (Or s (Dia (Dstar s))).

Fixpoint Neg (s : form) :=
  match s with
    | Var n => NegVar n
    | NegVar n => Var n
    | And s t => Or (Neg s) (Neg t)
    | Or s t => And (Neg s) (Neg t)
    | Box s => Dia (Neg s)
    | Dia s => Box (Neg s)
    | Bstar s => Dstar (Neg s)
    | Dstar s => Bstar (Neg s)
  end.

Lemma Neg_involutive s : Neg (Neg s) = s .

Lemma eval_Neg M (w:M) s : w |= Neg s = ~~ w |= s.

Lemma valid_unsat s : valid s <-> ~ sat (Neg s).

Lemma equiv_valid s t : equiv s t <-> valid (Or (And s t) (And (Neg s) (Neg t))).

Lemma dec_sat_val : decidable sat -> decidable valid.

Fixpoint synclos s :=
  s :: match s with
         | Var n => [::]
         | NegVar n => [::]
         | And s t => synclos s ++ synclos t
         | Or s t => synclos s ++ synclos t
         | Box s => synclos s
         | Dia s => synclos s
         | Bstar s => Box (Bstar s) :: synclos s
         | Dstar s => Dia (Dstar s) :: synclos s
       end.

Lemma synclos_refl t : t \in synclos t.

Lemma synclos_trans t t' s : t \in synclos t' -> t' \in synclos s -> t \in synclos s.

Ltac sc := rewrite /= ?in_cons ?mem_cat ?synclos_refl ?eq_refl.
Ltac synclos := apply : synclos_trans => // ; sc.
Ltac synclos' tmp := apply : synclos_trans ; last by apply tmp ; sc.

Implicit Arguments SeqSub [T s].
Notation "[ss s ; H ]" := (SeqSub s H) (at level 0).

Section FormulaUniverse.

Variable s : form.
Definition F := seq_sub (synclos s).

Definition Hcond (t : F) (H : {set F}) :=
  match val t with
    | NegVar v => ~~ Var v \in' H
    | And u v => u \in' H && v \in' H
    | Or u v => u \in' H || v \in' H
    | Bstar u => u \in' H && (Box (Bstar u)) \in' H
    | Dstar u => u \in' H || (Dia (Dstar u)) \in' H
    | _ => true
  end.

Definition hintikka (H : {set F}) : bool := forallb t , (t \in H) ==> Hcond t H.

Definition request (H : {set F}) := [set t : F | Box (val t) \in' H].

Definition HU : {set {set F}} := [set H | hintikka H].

Definition TR (S : {set {set F}}) (H H' : {set F}) := [&& H \in S , H' \in S & request H \subset H'].

Definition Ddia (S : {set {set F}}) : bool :=
  forallb H , (H \in enum (mem S)) ==>
  forallb t , (t \in H) ==>
  if val t is Dia u
    then existsb H', TR S H H' && u \in' H'
    else true.

Definition Ddstar (S : {set {set F}}) : bool :=
  forallb H , (H \in enum (mem S)) ==>
  forallb t , (t \in H) ==>
  if val t is (Dstar u)
    then existsb H', [&& connect (TR S) H H' , H' \in S & u \in' H']
    else true.

Definition demo (D : {set {set F}}) := [&& Ddia D , Ddstar D & D \subset HU].

Section ModelExistence.
  Variable D : {set {set F}}.
  Hypothesis demoD : demo D.

  Definition stateD := seq_sub (enum (mem D)).
  Definition transD (w:stateD) (v:stateD) := request (val w) \subset (val v).
  Definition labelD (w:stateD) v := Var v \in' (val w).

  Definition exsD (p : pred stateD) : bool := negb (pred0b p).
  Definition exsPD (p : pred stateD) : reflect (exists w, p w) (exsD p).

  Definition trans_starD (H H' : stateD) := connect transD H H'.
  Definition trans_starPD (H H' : stateD) : reflect (clos_refl_trans transD H H') (trans_starD H H').

  Definition MD :=
    {|
      state := stateD;
      trans := transD;
      label := labelD;
      exsP := exsPD;
      trans_starP := trans_starPD
    |}.

  Canonical Structure stateD_model := MD.
  Lemma hintikkaD : forall H, H \in D -> hintikka H.

  Lemma HC t (H : {set F}) : H \in (enum (mem D)) -> t \in H -> Hcond t H.

  Lemma bstar_trans t sc (H H' : stateD) :
    [ss Bstar t; sc] \in val H -> H --->* H' -> [ss Bstar t; sc] \in val H'.

  Lemma TR_transD (H H' : {set F}) HH HH':
    TR D H H' -> ([ss H ; HH] : stateD) ---> [ss H' ; HH'].

  Lemma connectTR_transD (H H' : {set F}) HH HH' :
    connect (TR D) H H' -> ([ss H ; HH] : stateD) --->* [ss H' ; HH'].

  Lemma model_MD_aux (t : F) (H : stateD) : t \in val H -> H |= (val t).

  Lemma model_existence (t : F) (H : {set F}) : (t \in H) -> H \in D -> sat (val t).

End ModelExistence.

Section SmallModelTheorem.

  Definition H_at M (w : M) := [set t : F | w |= (val t)].

  Lemma H_at_hintikka M (w : M) : hintikka (H_at w).

  Definition D M := [set H | exs w : M , H == H_at w].

  Lemma trans_TR M (w v : M) : w ---> v -> (TR (D M)) (H_at w) (H_at v).

  Lemma trans_star_connect M (w v : M) : w --->* v -> connect (TR (D M)) (H_at w) (H_at v).

  Lemma demoD M : demo (D M).

  Theorem small_model_theorem (t : F) : sat (val t) ->
    exists2 D , demo D & exists2 H , H \in D & t \in H.

  Theorem decidability (t : F) :
    sat (val t) <-> existsb D, demo D && existsb H : {set F}, (t \in H) && (H \in D).
End SmallModelTheorem.

End FormulaUniverse.

Corollary sat_dec: decidable sat.

Corollary valid_dec : decidable valid.

Corollary equiv_dec : decidable2 equiv.