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.
Unset Strict Implicit.
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.
Arguments supp L !s.

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

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.
Proof.
  move/subP => sub. case: s.
  elim => //= [|p|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] [|];
    solve [exact: sub| rewrite -?(rwP orP,rwP andP); intuition].
Qed.

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'.
Proof. exact: allU. Qed.

Lemma suppC1 L s : suppC L [fset s] = L |> s.
Proof. exact: all_fset1. Qed.

Lemma suppxx (L : {fset sform}) : literalC L -> suppC L L.
Proof. by apply: in_sub_all => [[[|p|s t|s|s t|s t] [|]]]. Qed.

Lemma suppCD L C C' : suppC L C' -> suppC L (C `\` C') -> suppC L C.
Proof.
  move/allP => S1 /allP S2. apply/allP => s inC.
  case (boolP (s \in C')) => inC'; auto. apply: S2. by rewrite inE; bcase.
Qed.

Lemma suppCWL L1 L2 C : suppC L2 C -> suppC (L1 `|` L2) C.
Proof. apply: sub_all => s. apply: supp_mon; auto with fset. Qed.

Lemma suppC_sub L C C' : C `<=` C' -> suppC L C' -> suppC L C.
Proof. move => H. apply: sub_all_dom. exact/subP. Qed.

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).
  Proof. exact: (svalP (DD (ssvalP p.1) (ssvalP p.2))). Qed.

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

  Unset Printing Records.

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.
  Proof. move: (DmatrixP p). repeat (case => ?). move/(_ x). by case: (leaf _). Qed.

  Lemma root_internal (p : DF * DC) : ~~ leaf (root (Dmatrix p)).
  Proof. move: (DmatrixP p). repeat (case => ?). done. Qed.

  Lemma serial_MRel (x : MType) : exists y, MRel x y.
  Proof.
    case: x => p x. case (boolP (leaf x)) => [lf|].
    - have inF := label_DF lf.
      move: (root_internal (next p.1, SeqSub _ inF)). rewrite negbK => /existsP [y xy].
      exists (existT (next p.1, SeqSub _ inF) y).
      by rewrite /MRel lf xy /= !eqxx.
    - rewrite negbK => /existsP [y xy]. exists (existT p y).
      by rewrite /MRel lift_eq xy.
  Qed.

  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).
  Proof. move: (DmatrixP p). repeat (case => ?). done. Qed.

  Lemma dmat_ev_cond (p : DF * DC) : ev_cond (val p.1) (Dmatrix p).
  Proof. move: (DmatrixP p). repeat (case => ?). done. Qed.

  Lemma sn_edge (p : DF * DC) (x : Dmatrix p) : sn (edge (g := Dmatrix p)) x.
  Proof. move: (DmatrixP p). repeat (case => ?). done. Qed.

  Lemma label_Dl (p : DF * DC) (x : Dmatrix p) : ~~ leaf x -> label x \in Dl.
  Proof. move: (DmatrixP p). repeat (case => ?). move/(_ x). by case: (leaf _). Qed.

  Lemma label_lcon (x : MType) : lcons (label (tagged x)).
  Proof.
    case: x => p x.
    case: (boolP (leaf x)) => [/label_DF /D_cond |/label_Dl] /=.
    - move/Dl_cond. rewrite inE => /andP[? ?] //.
    - move/Dl_cond. rewrite inE => /andP[? ?] //.
  Qed.

  Lemma label_F (p : DF * DC) (x : Dmatrix p) : {subset label x <= F}.
  Proof.
    apply/subP. case: (boolP (leaf x)) => [/label_DF /D_cond |/label_Dl] /=.
    - move/Dl_cond. rewrite inE powersetE => /andP[? ?] //.
    - move/Dl_cond. rewrite inE powersetE => /andP[? ?] //.
  Qed.

  Lemma dag_R (p : DF * DC) (x y : Dmatrix p) : edge x y -> suppC (label y) (R (label x)).
  Proof.
    move: (DmatrixP p). do 3 (case => _). case => /forallP /(_ x) /forall_inP /(_ y) H _.
    exact: H.
  Qed.

  Lemma MRel_R (x y : MType) : MRel x y -> suppC (label (tagged y)) (R (label (tagged x))).
  Proof.
    case: x => p x. case: y => p' y. rewrite /MRel. case/orP => [H|].
    - move: (liftE H) => ?; subst. rewrite lift_eq in H. exact: dag_R.
    - case/and4P => [_ /eqP Hp edg /eqP Hl] /=. move: (dag_R edg). by rewrite label_root -Hl.
  Qed.

  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^-.
  Proof.
    rewrite negbK => /existsP [y xy].
    have/forallP /(_ x) : glocal s_cond (Dmatrix p) by case: (DmatrixP p); intuition.
    rewrite /s_cond (_ : _ == fset0 = false) //=. move/all_inP => H /H {H} /(_ (erefl _)).
    - case/hasP => ?. case/fimsetP => z Hz -> Lz. exists z => //. by rewrite fsetE in Hz.
    - apply: negbTE. apply/emptyPn. exists (label y). by rewrite in_fimset ?fsetE.
  Qed.

  Lemma MRel_D (x : MType) s :
    fAX s^- \in label (tagged x) -> exists2 y, MRel x y & label (tagged y) |> s^-.
  Proof.
    case: x => p x. case (boolP (leaf x)) => lf Ls.
    - have inF := label_DF lf.
      move: (root_internal (next p.1, SeqSub _ inF)) => H. set p' := (_,_) in H.
      have Ls' : fAX s^- \in label (root (Dmatrix p')) by rewrite label_root /=.
      case: (dag_D H Ls') => y Hy Lys. by exists (existT p' y); rewrite // /MRel Hy /p' lf /= !eqxx.
    - case: (dag_D lf Ls) => y Hy Lys. by exists (existT p y); rewrite // /MRel lift_eq Hy.
  Qed.

  Lemma supp_edge (p : DF * DC) (x y : Dmatrix p) s : label x |> fAX s^+ -> edge x y -> label y |> s^+.
  Proof. rewrite -[_ y |> _]suppC1 => H xy. move: (dag_R xy). apply: suppC_sub. by rewrite fsub1 RE. Qed.

  Arguments interp !s.
  Prenex Implicits edge.

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.
  Proof.
    move => [p' y]. rewrite /MRel (negbTE (root_internal _)) [_ && _]/= orbF.
    split => [le|/orP [le|H]].
    - move: (liftE le) => ?;subst. rightb. rewrite lf /= !eqxx. by rewrite lift_eq in le.
    - move: (liftE le) => ?;subst. rewrite lift_eq in le.
      suff: false by []. rewrite -(negbTE lf). apply/existsP. by eexists.
    - case/and4P : H => _. destruct p as [u L]. destruct p' as [u' L'].
      case/eqP => /= ? e; subst. move/eqP => Lx. move: (label_DF lf). rewrite Lx => inDF.
      rewrite [SeqSub _ _](_ : _ = L') ?lift_eq //. apply/eqP. destruct L'. exact: eqxx.
  Qed.

  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).
  Proof. move => R. apply: cAU_eq R; try by rewrite /= label_root. exact: leaf_root_aux. Qed.

  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).
  Proof. move => R. apply: cEU_eq R; try by rewrite /= label_root. exact: leaf_root_aux. Qed.

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))).
  Proof.
    move => p Lst .
    move: (dmat_ev_cond p). rewrite /= /ev_cond Lst /= !suppF.
    case/orP => [?|GL]; first exact: AU0.
    elim: (sn_edge (root _)) Lst => x _ IHsn.
    rewrite /= classic_orb !suppF. case/orP => [?|/and3P [L0 L1 L2]]; first exact: AU0.
    have nlf: ~~ leaf x.
      move/forallP : (GL) => /(_ x). rewrite /a_cond /leaf negbK (negbTE L0) L1.
      case: (boolP (_ == _)) => //. case/emptyPn => ? /fimsetP [y xy _] _.
      apply/existsP. exists y. by rewrite fsetE in xy.
    apply: CTL_def.AUs => // [[? y]]. rewrite {1}/MRel (negbTE nlf) [_ && _]/= orbF => l_edge.
    move: (liftE l_edge) => ?; subst. rewrite lift_eq in l_edge. apply: IHsn (l_edge) _.
    exact: supp_edge l_edge.
  Qed.

  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))).
  Proof.
    move => p S. move: (dmat_ev_cond p).
    rewrite /ev_cond S /= suppF. case/orP => [?|/andP[E1 E2]]; first exact: EU0.
    case/existsP : E2 => z. case/connectP : (rootP z) => xs.
    elim: xs (root _) {S} => [x|y ys IHys x /=].
    - move => _ -> /= ?. exact: EU0.
    - case/andP => xy pth ? ?.
      have M: MRel (existT p x) (existT p y) by rewrite /MRel lift_eq; bcase.
      apply: EUs (M) _ => //=; last exact: IHys.
      move/forallP: E1 => /(_ x) /forall_inP /(_ _ xy). done.
  Qed.

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).
  Proof.
    move => Hnext Lx.
    move: (sn_edge x) Lx . elim => {x} x _ IH Lx.
    rewrite /= !suppF in Lx. case/orP : Lx => [Lx|/andP [L1 L2]]. exact: EU0.
    case: (boolP (leaf x)) => [lf|Hx].
    + apply: leaf_root'. apply: Hnext => //. by rewrite label_root /= !suppF; bcase.
    + case: (dag_D Hx L2) => y xy Hy.
      apply: (EUs (v := existT p y)) => //; [by rewrite /MRel lift_eq xy|exact: IH].
  Qed.

  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).
  Proof.
    move => Hnext Lx.
    move: (sn_edge x) Lx . elim => {x} x _ IH Lx.
    rewrite /= !suppF classic_orb in Lx. case/orP : Lx => [Lx|/and3P [L0 L1 L2]]. exact: AU0.
    case: (boolP (leaf x)) => [lf|Hx].
    + apply: leaf_root. apply: Hnext => //. by rewrite label_root /= !suppF; bcase.
    + apply: CTL_def.AUs => // [[p' y]].
      rewrite {1}/MRel (negbTE Hx) [_ && _]/= orbF => l_edge.
      move: (liftE l_edge) => ?; subst. rewrite lift_eq in l_edge. apply: IH (l_edge) _.
    exact: supp_edge l_edge.
  Qed.

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.
  Proof.
    case: s x. elim => [|p|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] [|] x.
    - rewrite /= => inL. move: (label_lcon x). by rewrite /lcons inL.
    - by simpl.
    - done.
    - rewrite /= => inL.
      case e : (fV p^+ \in label (tagged x)); last by rewrite /MLabel /= e.
      move => _. move: (label_lcon x) => /andP [_ /allP /(_ _ e)]. by rewrite inL.
    - rewrite /= !suppF. by case/orP => [/IHs|/IHt] /=; intuition.
    - rewrite /= !suppF. case/andP => /IHs A /IHt B. by simpl in *; intuition.
    - rewrite /= -RE => HR y /MRel_R S. apply: (IHs true).
      rewrite -suppC1. apply: suppC_sub S. by rewrite fsub1.
    - rewrite /=. case/MRel_D => y xy Hy. move => /(_ y xy). exact: (IHs false).
    - move: x. cofix => x.
      rewrite /= !suppF => /andP [/IHt A]. case/orP => [/IHs B|B]; first exact: AR0.
      apply: CTL_def.ARs => // y /MRel_R => S. apply: supp_eval.
      rewrite -suppC1. apply: suppC_sub S. by rewrite fsub1 RE.
    - move => L_x. apply: cAR_cEU. apply: EU_strengthen (IHs false) (IHt false) _ => {IHs IHt}.
      change (EU_M s t x).
      case: x L_x => p x Lx. rewrite [tagged _]/= in Lx.
      wlog ? : p x Lx / x = root (Dmatrix p) => [W|]; subst.
        apply: EU_lift Lx => L' HL'. exact: W HL' _.
      wlog inF : / (fAR s t^- \in F).
        move => W. rewrite /= !suppF classic_orb in Lx. case/orP : Lx => [?|/and3P [Lx ?]]. exact: EU0.
        move/label_F. move/sfc_F => *. exact: W.
      have Fgt0 : 0 < #|{: DF }|. apply/card_gt0P. by exists (SeqSub _ inF).
      case: p Lx => u. move En : (dist Fgt0 u (SeqSub _ inF)) => n.
      elim: n u En => [|n IHn] u.
      + move/dist0 => -> {u} L Lx. exact: EU_this.
      + move/distS. move/IHn => {IHn} IHn L Lx. apply: EU_lift Lx => L'. exact: IHn.
    - move => L_x. apply: AU_strengthen (IHs true) (IHt true) _ => {IHs IHt}. change (AU_M s t x).
      case: x L_x => p x Lx. rewrite [tagged _]/= in Lx.
      wlog ? : p x Lx / x = root (Dmatrix p) => [W|]; subst.
        apply: AU_lift Lx => L' HL'. exact: W HL' _.
      wlog inF : / (fAU s t^+ \in F).
        move => W. rewrite /= !suppF classic_orb in Lx. case/orP : Lx => [?|/and3P [Lx ?]]. exact: AU0.
        move/label_F. move/sfc_F => *. exact: W.
      have Fgt0 : 0 < #|{: DF }|. apply/card_gt0P. by exists (SeqSub _ inF).
      case: p Lx => u. move En : (dist Fgt0 u (SeqSub _ inF)) => n.
      elim: n u En => [|n IHn] u.
      + move/dist0 => -> {u} L Lx. exact: AU_this.
      + move/distS. move/IHn => {IHn} IHn L Lx. apply: AU_lift (Lx) => L' HL'. exact: IHn.
     - move => H /=. apply: cAU_cER. apply: ER_strengthen (IHs false) (IHt false) _ => {IHs IHt}.
       move: x H. cofix => x. rewrite /= !suppF => /andP [Lt]. case/orP => Ls; first exact: ER0.
       case: (MRel_D Ls) => y xy Ly. apply: ERs xy _. exact: Lt. exact: supp_eval.
  Qed.

  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.
  Proof.
    move => inF inDF. exists MD.
    pose p := (SeqSub _ inF, SeqSub _ inDF). exists (existT p (root (Dmatrix p))).
    split; first exact: fin_finite. move => s supp_s. apply: supp_eval. by rewrite /= label_root.
  Qed.

End ModelConstruction.