Require Import Relations Recdef.

Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finfun finset path fingraph bigop.
Require Import tactics base.

Import Prenex Implicits.

Section Characterizations.
  Variables (X : Type) (R : X -> X -> Prop).

  Definition EX (P : X -> Prop) (x : X) : Prop := exists2 y, R x y & P y.
  Definition AX (P : X -> Prop) (x : X) : Prop := forall y, R x y -> P y.

  Inductive EF (P : X -> Prop) (x : X) : Prop :=
  | EF0 : P x -> EF P x
  | EFs y : R x y -> EF P y -> EF P x.

  CoInductive AG (P : X -> Prop) ( x : X) : Prop :=
  | AGs : P x -> (forall y, R x y -> AG P y) -> AG P x.

  Lemma EX_ext P q x : P =1 q -> (EX P x <-> EX q x).

  Lemma EF_ext P q x : P =1 q -> (EF P x <-> EF q x).

  Hint Resolve rt1n_refl Relation_Operators.rt1n_trans rtn1_refl Relation_Operators.rtn1_trans.

  Implicit Arguments clos_refl_trans_1n [A].
  Implicit Arguments clos_refl_trans_n1 [A].
  Lemma EFC P x : EF P x <-> exists2 y, clos_refl_trans_1n R x y & P y.

  Lemma AGC P x : AG P x <-> forall y, clos_refl_trans_1n R x y -> P y.

End Characterizations.

Definition var := nat.
Definition nvar := nat.

Record model := Model {
  state :> Type;
  trans : state -> state -> Prop;
  label : var -> pred state;
  EXb : pred state -> pred state;
  EXbP (p:pred state) w : reflect (EX trans p w) (EXb p w);
  EFb : pred state -> pred state;
  EFbP (p:pred state) w : reflect (EF trans p w) (EFb p w);
  nlabel : nvar -> pred state;
  nlabelP : forall x : nvar, exists! w, w \in nlabel x
}.
Implicit Types M : model.

Section Models.
  Variable M : model.
  Implicit Types (w v : M) (p : pred M).

  Definition AXb p w := ~~ EXb (predC p) w.
  Definition AGb p w := ~~ EFb (predC p) w.

  Lemma EXb_ext q p w : p =1 q -> EXb p w = EXb q w.

  Lemma AXb_ext q p w : p =1 q -> AXb p w = AXb q w.

  Lemma EFb_ext q p w : p =1 q -> EFb p w = EFb q w.

  Lemma AGb_ext q p w : p =1 q -> AGb p w = AGb q w.

  Lemma AXP p w : reflect (AX trans p w) (AXb p w).

  Lemma negb_EXb p w : ~~ EXb p w = AXb (predC p) w.

  Lemma negb_AXb p w : ~~ AXb p w = EXb (predC p) w.

  Lemma EF_step p w : ~ EF trans p w -> AX trans (fun v => ~ EF trans p v) w.

  Lemma AGP_aux p w : ~ EF trans (fun v => predC p v) w -> AG trans p w.

  Lemma AGP p w : reflect (AG trans p w) (AGb p w).

  Lemma negb_EFb p w : ~~ EFb p w = AGb (predC p) w.

  Lemma negb_AGb p w : ~~ AGb p w = EFb (predC p) w.
End Models.

Section FiniteModel.
  Variables (T : finType) (e : rel T) (label : var -> pred T).
  Implicit Type p : pred T.

  Definition exb p w := existsb v, e w v && p v.
  Lemma exbP p w : reflect (EX e p w) (exb p w).

  Definition efb p w := existsb v, connect e w v && p v.
  Lemma efbP p w : reflect (EF e p w) (efb p w).

End FiniteModel.

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
| Nom : nvar -> form
| NegNom : nvar -> 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 ]
    | Nom n => Node (8,n) [::]
    | NegNom n => Node (9,n) [::]
  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
    | Node (8,n) [::] => Some (Nom n)
    | Node (9,n) [::] => Some (NegNom n)
    | _ => 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.

Fixpoint eval M s :=
  match s with
    | Var v => label v
    | NegVar v => predC (@label M v)
    | And s t => predI (eval M s) (eval M t)
    | Or s t => predU (eval M s) (eval M t)
    | Box s => AXb (eval M s)
    | Dia s => EXb (eval M s)
    | Bstar s => AGb (eval M s)
    | Dstar s => EFb (eval M s)
    | Nom x => nlabel x
    | NegNom x => predC (@nlabel M x)
  end.

Notation "w |= s" := (eval s w) (at level 35).
Notation "w ---> v" := (trans w v) (at level 35).

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.

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)
    | Nom x => NegNom x
    | NegNom x => Nom x
  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
         | Nom n => [::]
         | NegNom n => [:: Nom n]
       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).
Implicit Type (S : {set {set F}}).

Definition nset:= [set t : F | if val t is Nom x then true else false ].
Definition nseq : seq nvar := undup (map (fun u => if val u is Nom x then x else 0) (enum nset)).
Definition N := seq_sub nseq.

Lemma uniq_nseq : uniq nseq.

Lemma nseqP: forall x , x \in nseq <-> Nom x \in synclos s.

Definition nominal (H : {set F}) := existsb t, (t \in H) && if val t is Nom x then true else false.

Lemma nominalE H : nominal H -> exists x , exists Hx , [ss Nom x ; Hx ] \in H.

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
    | NegNom x => ~~ Nom x \in' H
    | _ => true
  end.

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

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

Definition request (H : {set F}) := [set t : F | Box (val t) \in' 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 Dxc (S : {set {set F}}) : bool := forallb x : N, #|[set H \in S | Nom (val x) \in' H]| <= 1.
Definition Dxe (S : {set {set F}}) : bool := forallb x : N, 1 <= #|[set H \in S | Nom (val x) \in' H]|.

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

Lemma DdiaNE (S : {set {set F}}) : ~~ Ddia S ->
    { H : {set F} | H \in S /\ exists2 t : form, Dia t \in' H & forall H', TR S H H' -> ~~ t \in' H' }.

Lemma connect_TR_S S H H' : H \in S -> connect (TR S) H H' -> H' \in S.

Lemma DdstarNE (S : {set {set F}}) : ~~ Ddstar S ->
  { H : {set F} | H \in S /\ exists2 t : form, Dstar t \in' H & forall H', connect (TR S) H H' -> ~~ t \in' H'}.

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

  Definition stateD := seq_sub (enum (mem D)).

  Definition default : stateD.

  Definition transD (w:stateD) (v:stateD) := TR D (val w) (val v).
  Definition labelD v (w:stateD) := Var v \in' (val w).
  Definition nlabelD x (w : stateD) : bool :=
    w \in if x \in nseq
      then [set H : stateD | Nom x \in' (val H)]
      else [set default].

  Lemma nlabelP' : forall x : nvar, exists! H:stateD, nlabelD x H.

  Definition MD :=
    {|
      state := stateD;
      trans := transD;
      label := labelD;
      EXbP := exbP transD ;
      EFbP := efbP transD ;
      nlabelP := nlabelP'
    |}.
  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 synclos_nlabelD n H : Nom n \in synclos s -> (Nom n \in' ssval H <-> nlabelD n H).

  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.

Notation "w |== A" := (forallb t, (t \in A) ==> w |= val t) (at level 35).
Section SmallModelTheorem.

  Definition pick_dc S := (if ~~ Ddia S is true as b return ~~ Ddia S = b -> option {set F}
    then fun p => Some (tag (DdiaNE p)) else fun _ => None) (refl_equal _).

  Lemma pick_dcH S: ~~ Ddia S -> exists H , pick_dc S = Some H.

  Lemma pick_dcS (S : {set {set F}}) H :
    pick_dc S = Some H -> H \in S /\ exists2 u , Dia u \in' H & forall H', TR S H H' -> ~~ u \in' H'.

  Definition pick_rc S := (if ~~ Ddstar S is true as b return ~~ Ddstar S = b -> option {set F}
    then fun p => Some (tag (DdstarNE p)) else fun _ => None) (refl_equal _).

  Lemma pick_rcH S: ~~ Ddstar S -> exists H , pick_rc S = Some H.

  Lemma pick_rcS (S : {set {set F}}) H :
    pick_rc S = Some H -> H \in S /\ exists2 u , Dstar u \in' H & forall H', connect (TR S) H H' -> ~~ u \in' H'.

  Definition step S := if pick_dc S is Some H then S :\ H else
    if pick_rc S is Some H then S :\ H else S.

  Lemma subset_step S : step S \subset S.

  Lemma step_smaller S : step S != S -> #|step S| < #|S|.


  Lemma prune_dc S : Ddia (prune S).

  Lemma prune_rc S : Ddstar (prune S).

  Lemma prune_subset S : prune S \subset S.

  Lemma prune_Dxc S : Dxc S -> Dxc (prune S).

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

  Lemma H_at_sat M (w : M) : w |== H_at w.

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

  Lemma extension M (w : M) (A : {set F}) : w |== A -> A \subset H_at w.

  Section PruningInvariant.
  Variable (M : model).
  Definition satM (H : {set F}) := exists w : M, w |== H.

  Definition invariant S := S \subset HU /\ forall v : M, H_at v \in S.

  Lemma inv_H_at (w : M) (S: {set {set F}}) : invariant S -> H_at w \in S.
  Lemma inv_sub S : invariant S -> S \subset HU.

  Lemma unsat_not_H_at (v : M) (H : {set F}): ~ satM H -> H_at v != H.

  Lemma Ddc_unsat H S u : invariant S ->
    H \in S -> Dia u \in' H -> (forall H' , TR S H H' -> ~~ u \in' H') -> ~ satM H.

  Lemma trans_TR (w v : M) (S: {set {set F}}) : invariant S -> w ---> v -> (TR S) (H_at w) (H_at v).

  Lemma Drc_unsat H S u : invariant S ->
    H \in S -> Dstar u \in' H -> (forall H' , connect (TR S) H H' -> ~~ u \in' H') -> ~ satM H.

  Lemma unsat_inv S H : invariant S -> H \in S -> ~ satM H -> invariant (S :\ H).


  Lemma invariant_step S : invariant S -> invariant (step S).

  Lemma invariant_prune S : invariant S -> invariant (prune S).

  Lemma invariant_Dxe S : invariant S -> Dxe S.

  Lemma invariant_demo S : Dxc S -> invariant S -> demo (prune S) || (prune S == set0).

  Lemma guess : exists f : N -> {set F} , forall x, exists2 w : M, w |= Nom (val x) & f x = H_at w.

  Definition maximal S := [&& S \subset HU , Dxe S , Dxc S & [set H \in HU | ~~ nominal H] \subset S].

  Lemma nominalI H x : Nom x \in' H -> nominal H.

  Lemma H_at_collapse x (w v :M) : Nom x \in' H_at w -> Nom x \in' H_at v -> w = v.

  Lemma guess_S : exists2 S , maximal S & invariant S.

  End PruningInvariant.

  Lemma demo_theorem (t:F) : sat (val t) ->
    existsb S , maximal S && let D := prune S in demo D && existsb H, (H \in D) && (t \in H).

End SmallModelTheorem.

Theorem decidability (t : F) :
  sat (val t) <-> existsb S , maximal S &&
    let D := prune S in demo D && existsb H, (H \in D) && (t \in H).

End FormulaUniverse.

Corollary sat_dec: decidable sat.


Corollary valid_dec : decidable valid.

Corollary equiv_dec : decidable2 equiv.