# Library Kstar

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.

Equivalence to alternative Characterizations
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.

# Models

Definition var := 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)
}.
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.

## Extensionality lemmas

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.

## Defining properties and dualities

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.

# Generic construction of finite 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.

# Syntax

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
.

countType and choiceType instances for 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.

# Evaluation

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)
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.

## Negation

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.

Proposition 4.1
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).

# Formula Universe

Most of the theory is developed with respect to a finite formula universe F, built from the syntactic closure of some formula s

Section FormulaUniverse.

Variable s : form.
Definition F := seq_sub (synclos s).
Implicit Type (S : {set {set F}}).

# Hintikka sets, Hintikka systems and demos

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 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 demo (D : {set {set F}}) := [&& Ddia D, Ddstar D & D \subset HU].

Strong eliminations in case Ddia / Ddstar is violated -- used for pruning

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 transD (w:stateD) (v:stateD) := TR D (val w) (val v).
Definition labelD v (w:stateD) := Var v \in' (val w).

Definition MD :=
{|
state := stateD;
trans := transD;
label := labelD;
EXbP := exbP transD ;
EFbP := efbP transD
|}.
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.

Proposition 4.2
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).
Definition satF (A:{set F}) := exists M : model, exists w : M, w |== A.

Section SmallModelTheorem.

# Pruning

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.

Definition Delta := prune HU.

Lemma demo_Delta : demo Delta.

## Pruning preserves the pruning invariant

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.

Definition invariant (S: {set {set F}}) :=
S \subset HU /\ forall H, H \in HU -> satF H -> H \in S.

Lemma inv_sub S : invariant S -> S \subset HU.

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

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

Lemma trans_TR M (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') -> ~ satF H.

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

Lemma invariantHU : invariant HU.

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

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

Lemma invariant_demo S : invariant S -> demo (prune S).

Theorem demo_theorem (t : F) : sat (val t) -> existsb H, (H \in Delta) && (t \in H).

Theorem 4.4
Theorem decidability (t : F) :
sat (val t) <-> existsb H, (H \in Delta) && (t \in H).

End SmallModelTheorem.

End FormulaUniverse.

Corollary 4.5
Corollary sat_dec: decidable sat.

Corollary valid_dec : decidable valid.

Corollary equiv_dec : decidable2 equiv.