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) (e : X -> X -> Prop).

  Definition EX (p : X -> Prop) (w : X) : Prop := exists2 v, e w v & p v.
  Definition AX (p : X -> Prop) (w : X) : Prop := forall v, e w v -> p v.

  Inductive EF (p : X -> Prop) (w : X) : Prop :=
  | EF0 : p w -> EF p w
  | EFs v : e w v -> EF p v -> EF p w.

  CoInductive AG (p : X -> Prop) (w : X) : Prop :=
  | AGs : p w -> (forall v, e w v -> AG p v) -> AG p w.

  Inductive AF (p : X -> Prop) (w : X) : Prop :=
  | AF0 : p w -> AF p w
  | AFs : (forall v, e w v -> AF p v) -> AF p w.

  CoInductive EG (p : X -> Prop) : X -> Prop :=
  | EGs w v : p w -> e w v -> EG p v -> EG p w.

  Lemma EX_ext p q w : p =1 q -> (EX p w <-> EX q w).

  Lemma EF_ext p q w : p =1 q -> (EF p w <-> EF q w).

  Lemma AF_ext p q w : p =1 q -> (AF p w <-> AF q w).

End Characterizations.

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);
  
  AFb : pred state -> pred state;
  AFbP (p:pred state) w : reflect (AF trans p w) (AFb p w)
}.

Implicit Type M : model.
Notation "w ---> v" := (trans w v) (at level 35).

Section Dualities.
  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.
  Definition EGb p w := ~~ AFb (predC p) w.

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

  Lemma AFb_ext q p w : p =1 q -> AFb p w = AFb q w.

  Lemma EFb_ext q p w : p =1 q -> EFb p w = EFb 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.

  Lemma AF_step p w : ~ AF trans p w -> EX trans (fun v => ~ AF trans p v) w.

  Lemma EGP_aux p w : ~ AF trans (fun v => predC p v) w -> EG trans p w.

  Lemma EGP p w : reflect (EG trans p w) (EGb p w).

  Lemma negb_afb p w : ~~ AFb p w = EGb (predC p) w.

  Lemma nedb_egb p w : ~~ EGb p w = AFb (predC p) w.

End Dualities.

Inductive form :=
  P_ of var | NP_ of var
| AND_ of form & form | OR_ of form & form
| EX_ of form | AX_ of form
| EF_ of form | AG_ of form
| AF_ of form | EG_ of form.

Fixpoint eval M (s : form) :=
  match s with
    | P_ v => label v
    | NP_ v => predC (@label M v)
    | AND_ s t => predU (eval M s) (eval M t)
    | OR_ s t => predI (eval M s) (eval M t)
    | EX_ s => EXb (eval M s)
    | AX_ s => AXb (eval M s)
    | EF_ s => EFb (eval M s)
    | AG_ s => AGb (eval M s)
    | AF_ s => AFb (eval M s)
    | EG_ s => EGb (eval M s)
    end.

Section FiniteModel.
  Variables (T : finType) (e : rel T) (label : var -> pred T).
  Implicit Types p q : 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).

  Variable p : pred T.
  Definition F A := A :|: [set x | p x] :|: [set x | forallb y, e x y ==> (y \in A)].
  Lemma monoF : mono F.

  Definition afb w := w \in mu F.
  Lemma afbP w : reflect (AF e p w) (afb w).
End FiniteModel.