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

Require Import edone bcase fset.
Require Import base CTL_def tab_def tab_dec dags demo.

Set Implicit Arguments.
Import Prenex Implicits.

Implicit Types (C:clause) (E: annot).

Tableaux to Demos

We for every subformula closed set F, we construct a demo containing all the consistent plain clauses over F. Since (backward) tablau derivations form trees, the demo arising this way naturally consists of a collection of trees. During the construction we do not work directly on the finite graphs used for the model construction but instead we use labeled trees.

The advantage of using tres always give rise to rooted dags, so these properties are preserved by construction and we do not show that they are preserved by our constructions.

We begin by adapting the definition of demos to trees.

Definition labels_from (T : countType) (X Xl : pred T) (t : tree T) :=
  tlocal (fun x Ts => if Ts == fset0 then x \in Xl else x \in X) t.

Lemma labels_leaf (T : countType) pl p (l : T) : labels_from pl p (Tree l [::]) = p l.

Fixpoint t_has (t' : form) (T : tree clause) :=
  let: Tree l ts := T in l |> t'^- || has (t_has t') ts.

Section DemoTrees.
  Variable (t : tree clause) (L0 LL : {fset clause }).

  Definition trivial := let: Tree l ts := t in nilp ts.

  Definition request_cond : bool := trespects r_cond t.

  Definition scomplete : bool := tlocal s_cond t.

  Definition tree_for L :=
    [&& rlab t == L , request_cond , scomplete & labels_from (mem L0) (mem LL) t ].

  Definition tree_for' L u :=
    ~~ L |> u ||
       match u with
         | fAU s' t'^+ => L |> t'^+ || tlocal (a_cond s' t') t
         | fAR s' t'^- => L |> t'^- || trespects (u_cond s') t && t_has t' t
         | _ => true
       end.

  Definition tree_for_and L u := tree_for' L u && tree_for L.
End DemoTrees.

Every consitent clause is in particular locally conistent.

Definition consistent A := ~~ tab_dec A.

Lemma cons_lcons A : consistent A -> lcons (pr A).

Lemma lcons_void C : consistent (C ,aVoid ) -> lcons C.

We build the canical demo for F, i.e., a demo for all consistent plain clauses.

Section CanonicalDemo.
  Variable (F : {fset sform }).
  Hypothesis sfc_F : sf_closed F.

  Definition D := [fset L in Cs F | literalC L && consistent (L,aVoid )].

  Definition Dl := [fset L in Cs F | literalC L && lcons L].

  Lemma D_sub_Dl : {subset D <= Dl }.

  Lemma ctab1 A1 A : (tab A1 -> tab A) -> consistent A -> consistent A1.

  Lemma ctab2 A1 A2 A : (tab A1 -> tab A2 -> tab A) -> consistent A -> consistent A1 || consistent A2.

We first show that every consistent clause with annotation is supported by a literal clause with the same annotation. The proof goes by induction on the weight of the clause.

  Fixpoint f_weight (s : form) :=
    match s with
      | fImp s t => (f_weight s + f_weight t).+1
      | fAU s t => (f_weight s + f_weight t).+1
      | fAR s t => (f_weight s + f_weight t).+1
      | _ => 0
    end.
  Definition s_weight := [fun s : sform => f_weight (fst s)].

  Lemma sweight_lit s : s_weight s = 0 <-> literal s.

  Definition weight C := fsum s_weight C.

  Lemma weight0 L : (weight L = 0) -> literalC L.

  Lemma weightS L : (0 < weight L) -> ~~ literalC L.

  Ltac Lsupp1 := move => L; rewrite /= ?suppCU !suppC1 !suppF; by bcase.
  Ltac Lsupp2 := by rewrite /= ?fsubUset !fsub1 !inE !ssub_refl.
  Ltac Lsupp3 := rewrite /weight /= ?fsumU !fsum1 /= -?(plusE ,minusE ); apply/leP; omega.

  Lemma support_aux C E : (C ,E ) \in U F -> consistent (C ,E ) ->
     exists L, [&& consistent (L ,E ), literalC L , (L ,E ) \in U F & suppC L C ].
  Qed.

Since all properties of the L in the lemma above are decidable and there are only countably many clauses to cosider we can use Ssreflect's choice operator to obtain a function returning for every cannotated clause a supporting literal clause.

  Lemma supportT A : (A \in U F ) && consistent A ->
     { L | [&& consistent (L,A .2 ), literalC L, (L,A .2 ) \in U F & suppC L A .1 ]}.

  Definition support C E : clause := sval (all_sig_cond fset0 supportT) (C ,E ).

  Section Support.
    Variables (C : clause) (E : annot).
    Hypothesis con_in_U : ((C ,E ) \in U F ) && consistent (C ,E ).
    Let suppP := svalP (all_sig_cond fset0 supportT) (C ,E ) con_in_U.

    Lemma supp_con : consistent (support C E ,E ).

    Lemma supp_lit : literalC (support C E).

    Lemma supp_U : (support C E , E ) \in U F.

    Lemma supp_suppC : suppC (support C E) C.
  End Support.

We now show how to construct the set of successors that are required to satisfy s_cond for states that do have successors.

  Section Jumps.
    Variable A : clause * annot.
    Hypothesis C_cons : consistent A.
    Hypothesis C_inU : A \in U F.

    Definition AXn := [fset u in A .1 | isDia u].
    Definition Rl := R A .1 :: [seq body u |` R A .1 | u <- AXn ].
    Definition successors := [seq (C, aR A .2 ) | C <- Rl ].

    Lemma Rljmp : R A .1 \in Rl.

    Lemma RlR C : C \in Rl -> R A .1 `<=` C.

    Lemma RlconU C : C \in Rl -> ((C , aR A .2 ) \in U F ) && consistent (C , aR A .2 ).

    Lemma succ_CinU : forall B: clause * annot, B \in successors -> (B \in U F ) && (consistent B ).

    Definition JCs := [seq support C0.1 C0.2 | C0 <- successors ].

    Lemma JC_scond : s_cond A .1 (set_of JCs).

    Lemma JC_rcond : [all D in JCs , r_cond A .1 D].

    Lemma JC_inhab : set_of (JCs) != fset0.

In the special case of a plain clause all successors are in D

Lemma JC_inD C : A .2 = aVoid -> C \in JCs -> C \in D.

Useful trees are the leaves and the tree consting just of a consistent clause with sufficently many succesors

    Definition j_leafs := [seq Tree L0 [::] | L0 <- JCs ].
    Definition j_tree := Tree (pr A) j_leafs.

    Lemma j_tree_r_cond : [all T0 in j_leafs , r_cond (A .1) (rlab T0)].

  End Jumps.

  Lemma tree_for_0 L : L \in D -> tree_for (Tree L [::]) Dl D L.

This allows us to construct nontrivial trees for all clauses in D

Lemma j_tree_for L : L \in D -> tree_for (j_tree (L ,aVoid )) Dl D L.

Lemma simple_tree L : L \in D -> {T | ~~ trivial T && tree_for T Dl D L }.

To construct more complex trees, we use two constructions. The first puts a singl new node on top of a forest, the other allows adding an additional leaf to a tree.

  Lemma tree_forI (L : clause) (Ts : seq (tree clause)) :
    L \in Dl ->
    ~~ nilp Ts ->
    s_cond L (set_of [seq (rlab T) | T <- Ts ]) ->
    [all T in Ts , r_cond L (rlab T)] ->
    [all T in Ts , tree_for T Dl D (rlab T)] ->
    tree_for (Tree L Ts) Dl D L.

  Lemma tree_for_cons T s t Ls a:
    consistent (Ls ,a ) -> (Ls ,a ) \in U F -> (pr (Ls ,a )) = (fAX (fAR s t)^- |` Ls ) ->
    literalC Ls -> aR a = aVoid ->
    tree_for T Dl D (rlab T) ->
    suppC (rlab T) (fAR s t ^- |` R Ls) ->
    tree_for (Tree (fAX (fAR s t)^- |` Ls) (T :: j_leafs (Ls ,a ))) Dl D (fAX (fAR s t)^- |` Ls).

  Lemma supp_suppCl s C E : ((s |` C , E ) \in U F ) && consistent (s |` C , E ) -> (support (s |` C) E ) |> s.

  Lemma supp_suppCr s C E : ((s |` C , E ) \in U F ) && consistent (s |` C , E ) -> suppC (support (s |` C) E) C.

We now construct the possibly trivial tree for consistent clauses with AU annotation

Lemma tree_AUH H s t C : ((C , aAU (s ,t ,H )) \in U F ) && consistent (C , aAU (s ,t ,H )) ->
{T : tree clause | suppC (rlab T) (fAU s t ^+ |` C) & tree_for T Dl D (rlab T) && tlocal (a_cond s t) T }.

The construction of trees for AU is similar to the construction above. Using the rules for setting up histories instead of tab_AUh

Lemma tree_AU L s t : L \in D -> { T | ~~ trivial T && tree_for_and T Dl D L (fAU s t ^+) }.

The construction of trees for AR is dual to the construciton of trees for AU. While for AU we needed to apply the induction hypotheis to all successors required by negative AX formulas, the AR annotation forces a sucessor by itself. So we we only need to apply the induction hypothesis to this one clause and then add sufficently many other successors to satisfy s_cond.

  Lemma tree_ARH H C s t : ((C , aAR (s ,t ,H )) \in U F ) && consistent (C , aAR (s ,t ,H )) ->
     {T : tree clause | suppC (rlab T) (fAR s t ^- |` C)
                      & [&& tree_for T Dl D (rlab T), trespects (u_cond s) T & t_has t T]}.

  Lemma tree_AR L s t : L \in D -> { T | ~~ trivial T && tree_for_and T Dl D L (fAR s t ^-) }.

  Lemma tree_demo L u : (u \in F) -> (L \in D) -> { T | ~~ trivial T && tree_for_and T Dl D L u }.

This finishes the construction of tree demos. Once we have tree demos, we need to show that the graphs corresponding to the constructed trees have all the required porperties

  Lemma rgraph_of_root (L : countType) (T : tree L) : label (root (rgraph_of T)) = rlab T.

  Lemma graph_of_labels (T : tree clause) (Dl D: {fset clause }) :
    labels_from (mem Dl) (mem D) T -> glabels_from Dl D (rgraph_of T).

  Lemma graph_has t (T: tree clause) : t_has t T -> ge_cond t (rgraph_of T).

  Lemma tab_demo : demo F Dl D.

End CanonicalDemo.

Finally, we show that tab is complete for plain clauses. To handle the case of an empty subformual universe, we construct a trivial model consisting of a single state with self loop.

Definition relT {X:Type} := [rel x y : X | true ].

Lemma serial_relT (X:Type) : forall x: X, exists y, relT x y.

Definition unit_model := fin_model (fun _ => xpred0) (@serial_relT unit).

Lemma tab_plain_complete C :
~ tab (C , aVoid ) -> exists (M : model) (w:M ), finite M /\ forall s, s \in C -> eval (interp s) w.