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 CTL_def dags.

Set Implicit Arguments.
Import Prenex Implicits.

Implicit Types (C:clause).

Demos

We define demos as an interface between the tableau calculus and the model construction. Before we define demos, we define literals, the support relation and local consistency.

Definition lcons (L : clause) :=
  (fF ^+ \notin L ) && [all s in L , if s is fV p^+ then fV p^- \notin L else true ].

Fixpoint literal (s : sform) :=
  let: (t,_) := s in
  match t with
    | fV _ => true
    | fAX _ => true
    | fF => true
    | _ => false
  end.

Definition literalC (L : clause) := [all s in L , literal s].

Fixpoint supp' (L : clause) u b :=
    match u,b with
      | fImp s t,true => supp' L s false || supp' L t true
      | fImp s t,false => supp' L s true && supp' L t false
      | fAU s t,true => supp' L t true
                       || supp' L s true && ((fAX (fAU s t),true ) \in L )
      | fAU s t,false => supp' L t false
                       && (supp' L s false || ((fAX (fAU s t),false ) \in L ))
      | fAR s t,true => supp' L t true
                       && (supp' L s true || ((fAX (fAR s t),true ) \in L ))
      | fAR s t,false => supp' L t false
                       || supp' L s false && ((fAX (fAR s t), false ) \in L )
      | _,_ => (u ,b ) \in L
    end.

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

Notation "L |> t" := (supp L t) (at level 30).
Lemma suppF C s b : supp' C s b = C |> (s ,b ).

For locally a locally consistent clause L, the collection of formulas supported by L corresponds to an (infinite) Hintikka set.

Lemma supp_mon L1 L2 s : L1 `<=` L2 -> L1 |> s -> L2 |> s.

Definition suppC L C := [all s in C , supp L s].

Lemma suppCU L C C' : suppC L (C `|` C') = suppC L C && suppC L C'.

Lemma suppC1 L s : suppC L [fset s ] = L |> s.

Lemma suppxx (L : {fset sform }) : literalC L -> suppC L L.

Lemma suppCD L C C' : suppC L C' -> suppC L (C `\` C') -> suppC L C.

Lemma suppCWL L1 L2 C : suppC L2 C -> suppC (L1 `|` L2) C.

Lemma suppC_sub L C C' : C `<=` C' -> suppC L C' -> suppC L C.

Now define demos. Most demo properties can be expressed using the glocal predicate or the respects predicate. The former checks that some predicate holds for every node and its immediate successors. The latter checks a predicate on every pair of nodes connected by an edge.

Section Demo.
  Variables (F : {fset sform }) (Dl D : {fset clause }).
  Hypothesis sfc_F : sf_closed F.

  Definition ge_cond t' (G : rGraph clause) :=
    [exists x, @dags.label _ G x |> t'^-].

  Definition s_cond C Cs :=
    (Cs == fset0 ) || [all u in C , isDia u ==> [some D in Cs , D |> body u]].

  Definition a_cond s' t' C (Cs : {fset clause }) :=
    if Cs == fset0 then C |> t'^+ else C |> s'^+.

  Definition r_cond C D := suppC D (R C).

  Definition u_cond s' (C _ : clause) := C |> s'^-.

  Definition ev_cond u (G : rGraph clause) :=
    let L := label (root G) in
    ~~ L |> u ||
       match u with
         | fAU s' t'^+ => L |> t'^+ || glocal (a_cond s' t') G
         | fAR s' t'^- => L |> t'^- || respects (u_cond s') G && ge_cond t' G
         | _ => true
       end.

  Definition glabels_from (G : graph clause) :=
    forall x : G, if leaf x then label x \in D else label x \in Dl.

    Definition dgraph G u L :=
       label (root G) = L
    /\ terminates (erel G)
    /\ glocal s_cond G
    /\ respects r_cond G
    /\ ev_cond u G
    /\ ~~ leaf (root G)
    /\ glabels_from G.

  Definition demo := forall L u, (u \in F) -> (L \in D) -> { G : rGraph clause | dgraph G u L }.
End Demo.

Demos to Models

Section ModelConstruction.
  Variables (F : {fset sform }) (Dl D : {fset clause }) (DD : demo F Dl D).

  Hypothesis sfc_F : sf_closed F.
  Hypothesis D_cond : {subset D <= Dl }.
  Hypothesis Dl_cond : {subset Dl <= [fset L in powerset F | lcons L]}.

We turn both F and D into finite types and construct a finite matrix of dgraphs indexed by the finite type DF * DC

  Definition DF := seq_sub F.
  Definition DC := seq_sub D.

  Definition Dmatrix (p: DF * DC) := (sval (DD (ssvalP p .1) (ssvalP p .2))).

  Lemma DmatrixP (p: DF * DC) : dgraph Dl D (Dmatrix p) (val p .1) (val p .2).

  Definition MType := { p : DF * DC & Dmatrix p }.
  Definition MLabel p (x:MType) := fV p ^+ \in label (tagged x).

For the definition of the transistion relation, we use the litf_edge construction to lift all the internal edges of the various dags to transitions in the model. We define a cyclic next fuction we define on finite types

  Definition MRel (x y : MType) :=
     lift_edge x y ||
      (let: (existT p a, (existT q a')) := (x ,y ) in
       [&& leaf a, q.1 == next p.1 , edge (root (Dmatrix q)) a' & label a == val q.2 ]).

To construct a finite model, we need to show that MRel is serial

  Lemma label_DF (p : DF * DC) (x : Dmatrix p) : leaf x -> label x \in D.

  Lemma root_internal (p : DF * DC) : ~~ leaf (root (Dmatrix p)).

  Lemma serial_MRel (x : MType) : exists y, MRel x y.

  Definition MD := fin_model MLabel serial_MRel.

We define a number of lemmas to extract dag properties and lift porperies from the dags to the model MD

  Lemma label_root (p : DF * DC) : label (root (Dmatrix p)) = val (p .2).

  Lemma dmat_ev_cond (p : DF * DC) : ev_cond (val p .1) (Dmatrix p).

  Lemma sn_edge (p : DF * DC) (x : Dmatrix p) : sn (edge (g := Dmatrix p)) x.

  Lemma label_Dl (p : DF * DC) (x : Dmatrix p) : ~~ leaf x -> label x \in Dl.

  Lemma label_lcon (x : MType) : lcons (label (tagged x)).

  Lemma label_F (p : DF * DC) (x : Dmatrix p) : {subset label x <= F }.

  Lemma dag_R (p : DF * DC) (x y : Dmatrix p) : edge x y -> suppC (label y) (R (label x)).

  Lemma MRel_R (x y : MType) : MRel x y -> suppC (label (tagged y)) (R (label (tagged x))).

  Lemma dag_D (p : DF * DC) (x : Dmatrix p) s :
    ~~ leaf x -> fAX s ^- \in label x -> exists2 y, edge x y & label y |> s ^-.

  Lemma MRel_D (x : MType) s :
    fAX s ^- \in label (tagged x) -> exists2 y, MRel x y & label (tagged y) |> s ^-.

  Lemma supp_edge (p : DF * DC) (x y : Dmatrix p) s : label x |> fAX s ^+ -> edge x y -> label y |> s ^+.

We define special predicates over MD that express the eventualities in terms of support instead of eval. In the proof of the support lemma, this will be what is left to show after the induction hypothesis has been applied.

  Definition AU_M s t (x : MD) :=
    cAU MRel (fun z => label (tagged z) |> s ^+) (fun z => label (tagged z) |> t ^+) x.

  Definition EU_M s t (x : MD) :=
    cEU MRel (fun z => label (tagged z) |> s ^-) (fun z => label (tagged z) |> t ^-) x.

We make use uf the fact, that CTL cannot distinguish between equally labeled states that have the same successorts. In particular this means that an eventuallity is satisfied at the leaf of one dag, if it is satiesfied at the equally labeled root of the next row.

  Lemma leaf_root_aux (p : DF * DC) (x : Dmatrix p) (lf : leaf x) :
      forall y, MRel (existT (next p .1 , SeqSub (label x) (label_DF lf))
                (root (Dmatrix (next p .1 , SeqSub (label x) (label_DF lf))))) y <->
                MRel (existT p x) y.

  Lemma leaf_root s t (p : DF * DC) (x : Dmatrix p) (lf : leaf x) :
    AU_M s t (existT (next p .1 , SeqSub _ (label_DF lf)) (root (Dmatrix (next p .1 , SeqSub _ (label_DF lf))))) ->
    AU_M s t (existT p x).

  Lemma leaf_root' s t (p : DF * DC) (x : Dmatrix p) (lf : leaf x) :
    EU_M s t (existT (next p .1 , SeqSub _ (label_DF lf)) (root (Dmatrix (next p .1 , SeqSub _ (label_DF lf))))) ->
    EU_M s t (existT p x).

Every eventuality is fulfilled at the root of its correspinding dag.

  Lemma AU_this (s t : form) (L : DC) (inF : fAU s t ^+ \in F) :
    let p := (SeqSub (fAU s t ^+) inF , L ) in
    label (root (Dmatrix p)) |> fAU s t ^+ -> AU_M s t (existT p (root (Dmatrix p))).

  Lemma EU_this (s t : form) (L : DC) (inF : fAR s t ^- \in F) :
    let p := (SeqSub (fAR s t ^-) inF , L ) in
    label (root (Dmatrix p)) |> fAR s t ^- -> EU_M s t (existT p (root (Dmatrix p))).

We can always defer fullfilling an eventuality to the next row.

  Lemma EU_lift (s t : form) (p : DF * DC) (x : Dmatrix p) :
    (forall L', label (root (Dmatrix (next p .1 , L'))) |> fAR s t ^-
             -> EU_M s t (existT (next p .1 , L') (root (Dmatrix (next p .1 , L'))))) ->
    label x |> fAR s t ^- -> EU_M s t (existT p x).

  Lemma AU_lift (s t : form) (p : DF * DC) (x : Dmatrix p) :
    (forall L', label (root (Dmatrix (next p .1 , L'))) |> fAU s t ^+
             -> AU_M s t (existT (next p .1 , L') (root (Dmatrix (next p .1 , L'))))) ->
    label x |> fAU s t ^+ -> AU_M s t (existT p x).

Finally, we can prove that every state in the model satisfies all signed formulas it supports. The interesting cases are those for the eventualities. In either case we first show that it suffices to consider eventualities at root of a fragment by defering to the next row in the matix. Only after this we start the induction on the distance between the current row and the row for the eventuality under consideration

  Lemma supp_eval s (x : MD) : label (tagged x) |> s -> eval (interp s) x.

  Lemma model_existence u L :
    u \in F -> L \in D -> exists (M : model) (w : M ), finite M /\ forall s, L |> s -> eval (interp s) w.

End ModelConstruction.