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

Require Import edone bcase fset.
Require Import base modular_hilbert .

Set Implicit Arguments.
Import Prenex Implicits.

CTL in Coq

We define the semantics of CTL using induction and co-indcution. While we only need AX, AU, and AR to define the evaluation function, we also define the duals. These are used mainly when constructing models.

Notation "P =p Q" := (forall x, P x <-> Q x) (at level 40).
Definition PredC X (p : X -> Prop) x := ~ p x.
Section Characterizations.

  Variables (X : Type) (e : X -> X -> Prop).

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

  CoInductive cAR (p q : X -> Prop) (w : X) : Prop :=
  | AR0 : p w -> q w -> cAR p q w
  | ARs : q w -> (forall v, e w v -> cAR p q v) -> cAR p q w.

  Inductive cAU (p q : X -> Prop) (w : X) : Prop :=
  | AU0 : q w -> cAU p q w
  | AUs : p w -> (forall v, e w v -> cAU p q v) -> cAU p q w.

  CoInductive cER (p q : X -> Prop) (w : X) : Prop :=
  | ER0 : p w -> q w -> cER p q w
  | ERs v : q w -> e w v -> cER p q v -> cER p q w.

  Inductive cEU (p q : X -> Prop) (w : X) : Prop :=
  | EU0 : q w -> cEU p q w
  | EUs v : p w -> e w v -> cEU p q v -> cEU p q w.

  Lemma cAU_cER (p q : X -> Prop) (w : X) :
    cER (PredC p) (PredC q) w -> ~ cAU p q w.

  Lemma cAR_cEU (p q : X -> Prop) (w : X) :
    cEU (PredC p) (PredC q) w -> ~ cAR p q w.

  Lemma AU_strengthen (p1 q1 p2 q2 : X -> Prop) w :
    (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) ->
    cAU p1 q1 w -> cAU p2 q2 w.

  Lemma AR_strengthen (p1 q1 p2 q2 : X -> Prop) w :
    (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) ->
    cAR p1 q1 w -> cAR p2 q2 w.

  Lemma ER_strengthen (p1 q1 p2 q2 : X -> Prop) w :
    (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) ->
    cER p1 q1 w -> cER p2 q2 w.

  Lemma EU_strengthen (p1 q1 p2 q2 : X -> Prop) w :
    (forall v, p1 v -> p2 v) -> (forall v, q1 v -> q2 v) ->
    cEU p1 q1 w -> cEU p2 q2 w.

  Lemma cAU_eq (x y : X) (p q : pred X) :
    p x = p y -> q x = q y -> e x =p e y -> cAU p q x -> cAU p q y.

  Lemma cEU_eq (x y : X) (p q : pred X) :
     p x = p y -> q x = q y -> e x =p e y -> cEU p q x -> cEU p q y.

End Characterizations.

Formulas

Definition var := nat.

Inductive form :=
| fF
| fV of var
| fImp of form & form
| fAX of form
| fAR of form & form
| fAU of form & form.

Lemma eq_form_dec (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.

To use formulas and other types built arund formulas as base type for the finite set libaray, we need to show that formulas are countable. We do this by embedding formulas into the Ssreflect's generic trees

Module formChoice.
  Import GenTree.

  Fixpoint pickle (s : form) :=
    match s with
      | fV v => Leaf v
      | fF => Node 0 [::]
      | fImp s t => Node 1 [:: pickle s ; pickle t]
      | fAX s => Node 2 [:: pickle s ]
      | fAU s t => Node 3 [:: pickle s ; pickle t]
      | fAR s t => Node 4 [:: pickle s ; pickle t]
    end.

  Fixpoint unpickle t :=
    match t with
      | Leaf v => Some (fV v)
      | Node 0 [::] => Some (fF)
      | Node 1 [:: t ; t' ] =>
          obind (fun s => obind (fun s' => Some (fImp s s')) (unpickle t')) (unpickle t)
      | Node 2 [:: t ] => obind (fun s => Some (fAX s)) (unpickle t)
      | Node 3 [:: t ; t' ] =>
        obind (fun s => obind (fun s' => Some (fAU s s')) (unpickle t')) (unpickle t)
      | Node 4 [:: t ; t' ] =>
        obind (fun s => obind (fun s' => Some (fAR s s')) (unpickle t')) (unpickle t)
      | _ => None
    end.

  Lemma pickleP : pcancel pickle unpickle.
End formChoice.

Definition form_countMixin := PcanCountMixin formChoice.pickleP.
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.

Models

Definition stable X Y (R : X -> Y -> Prop) := forall x y, ~ ~ R x y -> R x y.
Definition determined X Y (R : X -> Y -> Prop) := forall x y, R x y \/ ~ R x y.

Record sts := STS {
  state :> Type;
  trans : state -> state -> Prop;
  label : var -> state -> Prop;
  serial : forall w:state, exists v, trans w v
}.

Fixpoint eval (M:sts) (s : form) :=
  match s with
    | fF => (fun _ => False)
    | fV v => label v
    | fImp s t => (fun w => eval M s w -> eval M t w)
    | fAX s => cAX (@trans M) (eval M s)
    | fAR s t => cAR trans (eval M s) (eval M t)
    | fAU s t => cAU trans (eval M s) (eval M t)
    end.

Record model := Model { sts_of :> sts; modelP : determined (@eval sts_of) }.

Hilbert System

Section Hilbert.
  Local Notation "s ---> t" := (fImp s t).

  Inductive prv : form -> Prop :=
  | rMP s t : prv (s ---> t) -> prv s -> prv t
  | axK s t : prv (s ---> t ---> s)
  | axS s t u : prv ((u ---> s ---> t ) ---> (u ---> s ) ---> u ---> t)
  | axDN s : prv (((s ---> fF ) ---> fF ) ---> s)
  | rNec s : prv s -> prv (fAX s)
  | axN s t : prv (fAX (s ---> t) ---> fAX s ---> fAX t)

  | AU_ind s t u : prv (t ---> u) -> prv (s ---> fAX u ---> u) -> prv ((fAU s t ) ---> u)
  | axAUI s t : prv (t ---> fAU s t)
  | axAUf s t : prv (s ---> fAX (fAU s t) ---> fAU s t)

  | rAR_ind s t u :
      prv (u ---> t) -> prv (u ---> (s ---> fF ) ---> fAX u) -> prv (u ---> fAR s t)
  | axARE s t : prv (fAR s t ---> t)
  | axARu s t : prv (fAR s t ---> (s ---> fF ) ---> fAX (fAR s t))

  | ax_serial : prv (fAX fF ---> fF)

  .

  Canonical Structure prv_mSystem := MSystem rMP axK axS.
  Canonical Structure prv_pSystem := PSystem axDN.
  Canonical Structure prv_kSystem := KSystem rNec axN.
  Canonical Structure prv_ctlSystem := CTLSystem AU_ind axAUI axAUf rAR_ind axARE axARu.

  Lemma soundness s : prv s -> forall (M:model) (w:M), eval s w.

  Definition EU s t := ~~: fAR (~~: s) (~~: t).

Unlike in our previous work on modal logics with transitive closure, we require of models, that the evaluation relation is not only stable under double negation bun indeed is determined. The reason for this is the coinductive modality AR. Using stability for classical reasoing violates the guard condition for coinductive proofs.

End Hilbert.

Finite Models

A model is finite, if the underlying type of states is a finite type. We show that we can turn any serial boolean transiton relation and labeling over a fintype into a model. We obtain stability by giving a boolean evaluation function which reflects the satisfaction relation. For this we need to evaluate the evanutalities. This requires boolean reflections of AU and AR which we obtain using fixpoint computations.

Inductive finite (M:model) : Prop :=
  finiteI (T:finType) : M.(state) = T :> Type -> finite M.

Section AUb.
  Variables (T: finType) (e : rel T) (p q : pred T).
  Definition AU_fun (X : {set T }) :=
    [set x | q x] :|: [set x | p x && [forall (y | e x y), y \in X ]].

  Lemma AU_mono : mono AU_fun.

  Definition AUb w := w \in lfp AU_fun.

  Lemma auP w : reflect (cAU e p q w) (AUb w).

  Definition EU_fun (X : {set T }) :=
    [set x | q x] :|: [set x | p x && [exists (y | e x y), y \in X ]].

  Lemma EU_mono : mono EU_fun.

  Definition EUb w := w \in lfp EU_fun.

  Lemma euP w: reflect (cEU e p q w) (EUb w).

End AUb.

Definition ARb (T:finType) (e: rel T) (p q : pred T) w := ~~ EUb e (predC p) (predC q) w.

Lemma arP (T:finType) (e : rel T) (p q : pred T) w:
  reflect (cAR e p q w) (ARb e p q w).

Section FiniteModels.
  Variables (T: finType) (e : rel T) (l: var -> pred T).
  Hypothesis serial_e : forall x, exists y, e x y.

  Definition fin_sts := {| label := l ; serial := serial_e |}.

  Fixpoint evalb s :=
    match s with
    | fV p => l p
    | fF => xpred0
    | fImp s t => fun w => evalb s w ==> evalb t w
    | fAX s => fun w => [forall (v | e w v) , evalb s v]
    | fAU s t => AUb e (evalb s) (evalb t)
    | fAR s t => ARb e (evalb s) (evalb t)
  end.

  Lemma evalP (w:fin_sts) s : reflect (eval s w) (evalb s w).

  Lemma fin_modelP : determined (@eval fin_sts).

  Definition fin_model := {| sts_of := fin_sts ; modelP := fin_modelP |}.

  Lemma fin_finite : finite fin_model.
End FiniteModels.

Signed Formulas

Our decision methods for CTL employ signed formulas. we also define a number of inversion lemmas and other useful constructiuons

Definition sform := (form * bool) %type.
Notation "s ^-" := (s,false ) (at level 20, format "s ^-").
Notation "s ^+" := (s,true ) (at level 20, format "s ^+").

Definition interp s := match s with (t,true ) => t | (t,false ) => fImp t fF end.

Definition body s := match s with fAX t^+ => t^+ | fAX t^- => t^- | _ => s end.

Definition positive (s:sform) := if s is t^+ then true else false.
Definition positives C := [fset s.1 | s <- [fset t in C | positive t]].

Lemma posE C s : (s \in positives C ) = (s ^+ \in C ).

Definition negative (s:sform) := ~~ positive s.
Definition negatives C := [fset s.1 | s <- [fset t in C | negative t]].

Lemma negE C s : (s \in negatives C ) = (s ^- \in C ).

Definition isBox s := if s is fAX s^+ then true else false.

Inductive isBox_spec s : bool -> Type :=
| isBox_true t : s = fAX t ^+ -> isBox_spec s true
| isBox_false : isBox_spec s false.

Lemma isBoxP s : isBox_spec s (isBox s).

Definition isDia s := if s is fAX s^- then true else false.

Inductive isDia_spec s : bool -> Type :=
| isDia_true t : s = fAX t ^- -> isDia_spec s true
| isDia_false : isDia_spec s false.

Lemma isDiaP s : isDia_spec s (isDia s).

Definition clause := {fset sform }.

Definition R C := [fset body s | s <- [fset t in C | isBox t]].

Lemma RE C s : (s ^+ \in R C ) = (fAX s ^+ \in C ).

Lemma Rpos s C : s ^- \notin R C.

Lemma RU (C C' : clause) : R (C `|` C') = (R C `|` R C').

Lemma R1 (s : sform) : R [fset s ] = if s is fAX u^+ then [fset u^+] else fset0.

Lemma R0 : R fset0 = fset0.

Subformula Closure

Fixpoint ssub' b s :=
  (s ,b ) |` match s with
             | fImp s t => ssub' (negb b) s `|` ssub' b t
             | fAX t => ssub' b t
             | fAU s t => (fAX (fAU s t),b ) |` (ssub' b s `|` ssub' b t)
             | fAR s t => (fAX (fAR s t),b ) |` (ssub' b s `|` ssub' b t)
             | _ => fset0
           end.

Lemma ssub'_refl s b : (s ,b ) \in ssub' b s.

Definition ssub (s : sform) := let (t,b) := s in (ssub' b t).

Lemma ssub_refl s : s \in ssub s.

Definition sf_closed' (F : {fset sform }) (s:sform) :=
  match s with
    | (fImp s t,b) => ((s ,negb b) \in F ) && ((t,b) \in F )
    | (fAX s, b) => (s ,b) \in F
    | (fAU s t, b) => [&& (fAX (fAU s t),b) \in F , (s ,b) \in F & (t,b) \in F ]
    | (fAR s t, b) => [&& (fAX (fAR s t),b) \in F , (s ,b) \in F & (t,b) \in F ]
    | _ => true
  end.

Definition sf_closed (F :{fset sform }) := forall s, s \in F -> sf_closed' F s.

Lemma sf_closed'_mon (X Y : clause) s : sf_closed' X s -> X `<=` Y -> sf_closed' Y s.

Lemma sfcU (X Y : {fset sform }) : sf_closed X -> sf_closed Y -> sf_closed (X `|` Y).

Lemma sf_ssub F s : sf_closed F -> s \in F -> ssub s `<=` F.

Lemma sfc_ssub s : sf_closed (ssub s).