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.
Unset Strict Implicit.
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.
Proof. by rewrite /= fset0E eqxx unfold_in. Qed.

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).
Proof.
  case: A => C a. apply: contraNT. rewrite negb_and negbK -has_predC.
  case/orP => H.
  - suff inC: (fF^+ \in C). rewrite (fset1U inC). by case (tab_dec _).
    case: a H => [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] /=; rewrite !inE ?eqF //.
  - case/hasP : H. case. case => //= p [|//] H. rewrite negbK => H'.
    suff S : forall b, (fV p,b) \in pr' _ `|` C -> (fV p,b) \in C.
      move: H H' => /S H /S H'. rewrite (fset1U H) (fset1U H'). by case (tab_dec _).
    move => { a H H'} a b. rewrite inE.
    by case: a => [[[s t] H]|[[s t] H]|[[s t] H]|[[s t] H]|] /=; rewrite !inE ?eqF //.
Qed.

Lemma lcons_void C : consistent (C,aVoid) -> lcons C.
Proof. move/cons_lcons => /=. by rewrite fset0U. Qed.

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}.
  Proof. move => x. rewrite !inE. case/and3P => -> -> /=. exact: lcons_void. Qed.

  Lemma ctab1 A1 A : (tab A1 -> tab A) -> consistent A -> consistent A1.
  Proof. rewrite /consistent. case (tab_dec A1); case (tab_dec A) => //=. auto. Qed.

  Lemma ctab2 A1 A2 A : (tab A1 -> tab A2 -> tab A) -> consistent A -> consistent A1 || consistent A2.
  Proof. rewrite /consistent. case (tab_dec A2); case (tab_dec A1); case (tab_dec A) => //=. auto. Qed.

  Prenex Implicits tab_Ip tab_In tab_AXn tab_AUp tab_AUn tab_ARp tab_ARn tab_foc tab_AUh tab_jmp tab_foc' tab_ARh tab_aAXR.

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.
  Proof. case: s => [[|p|s t|s|s t|s t] [|]] //. Qed.

  Definition weight C := fsum s_weight C.

  Lemma weight0 L : (weight L = 0) -> literalC L.
  Proof. move/fsum_eq0 => H. apply/allP => x /H. by move/sweight_lit. Qed.

  Lemma weightS L : (0 < weight L) -> ~~ literalC L.
  Proof.
    rewrite lt0n. apply: contra => /allP H. apply/eqP.
    by have/fsum_const : {in L, const 0 s_weight} by move => x /H /sweight_lit.
  Qed.

  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].
  Proof
    with apply: S => //; by [Lsupp1|Lsupp2|Lsupp3].
    pattern C. move: C. apply: @nat_size_ind _ _ weight _ => C IH inU con.
    case: (posnP (weight C)) => [/weight0 ? |wC]; first by exists C; rewrite suppxx //; bcase.
    set G := exists _, _.
    have S C' s : s \in C -> (forall L, suppC L C' -> supp L s) ->
      C' `<=` ssub s -> weight C' < s_weight s -> consistent (C' `|` C `\` [fset s],E) -> G.
      move => inC supp_Cs sub W con'. case: (IH _ _ _ con') => [||L /and4P [C1 C2 C3 C4]].
      - by apply fsum_replace; rewrite ?fsum1 ?fsub1.
      - rewrite (fset1U inC) in inU. move: inU. rewrite !in_fsetX => /andP [H ->].
        rewrite !powersetU !powersetE andbT fsub1 in H *. case/andP: H => [F1 F2].
        rewrite [_ `\` _ `<=` _](sub_trans _ F2) // andbT.
        apply: sub_trans sub _. exact: sf_ssub.
      - exists L. rewrite C1 C2 C3 /=. rewrite suppCU in C4.
        case/andP : C4 => /supp_Cs => HCs. apply: suppCD. by rewrite suppC1.
    case/allPn : (weightS wC). move => [[|p|s t|s|s t|s t] [|]] // inC _; rewrite -(fsetUD1 inC) in con.
    - case/orP: (ctab2 tab_Ip con)...
    - move : (ctab1 tab_In con); rewrite fsetUA...
    - case/orP: (ctab2 tab_ARp con); rewrite fsetUA...
    - case/orP: (ctab2 tab_ARn con); rewrite ?fsetUA...
    - case/orP: (ctab2 tab_AUp con); rewrite ?fsetUA...
    - case/orP: (ctab2 tab_AUn con); rewrite ?fsetUA...
  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]}.
  Proof.
    case: A => C E /andP [H1 H2]. set Ex := (support_aux H1 H2).
    exists (xchoose Ex). exact: xchooseP Ex.
  Qed.

  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).
    Proof. by case/and4P : suppP. Qed.

    Lemma supp_lit : literalC (support C E).
    Proof. by case/and4P : suppP. Qed.

    Lemma supp_U : (support C E, E) \in U F.
    Proof. by case/and4P : suppP. Qed.

    Lemma supp_suppC : suppC (support C E) C.
    Proof. by case/and4P : suppP. Qed.
  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.
    Proof. exact: mem_head. Qed.

    Lemma RlR C : C \in Rl -> R A.1 `<=` C.
    Proof. rewrite in_cons. case/orP => [/eqP ->|/mapP [u _ ->]]; by rewrite ?subxx ?fsubUr. Qed.

    Lemma RlconU C : C \in Rl -> ((C, aR A.2) \in U F) && consistent (C, aR A.2).
    Proof.
      rewrite in_cons; case/orP => [/eqP ->|/mapP [?]].
      by rewrite tabU_jmp ?(ctab1 tab_jmp) -?surjective_pairing.
      rewrite inE andbC. case: (isDiaP _) => //= u -> Hu -> /=.
      by rewrite tabU_AXn ?(ctab1 tab_AXn) -?(fset1U Hu) -?surjective_pairing.
    Qed.

    Lemma succ_CinU : forall B: clause * annot, B \in successors -> (B \in U F) && (consistent B).
    Proof. move => [C E]. by case/mapP => ? /RlconU ? [-> ->]. Qed.

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

    Lemma JC_scond : s_cond A.1 (set_of JCs).
    Proof.
      rightb. apply/allP => u /= Hu. case: (isDiaP _) => //= t Ht.
      pose B := (body u |` R A.1, aR A.2).
      have SB: B \in successors.
        apply/mapP; eexists => //. rewrite inE. rightb. apply/mapP; eexists => //. by rewrite inE Hu Ht.
      existsb (support B.1 B.2). rewrite set_ofE. apply/mapP; exists B => //.
      rewrite -suppC1. apply: suppC_sub (supp_suppC _). by rewrite /B /= fsubUl.
      rewrite -surjective_pairing. exact: succ_CinU.
    Qed.

    Lemma JC_rcond : [all D in JCs , r_cond A.1 D].
    Proof.
      apply/allP => ? /mapP [B HB] ->. case/mapP : HB => C HC -> /=. rewrite /r_cond.
      apply: suppC_sub (supp_suppC _). exact: RlR. exact: RlconU.
    Qed.

    Lemma JC_inhab : set_of (JCs) != fset0.
    Proof.
      suff: support (R A.1) (aR A.2) \in JCs.
        apply: contraTN. rewrite -set_ofE => /eqP->. by rewrite inE.
      apply/mapP. exists (R A.1,aR A.2) => //.
      apply/mapP; exists (R A.1) => //. exact: mem_head.
    Qed.

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.
    Proof.
      move => EQ.
      case/mapP => B HB ->. rewrite [_ \in D]inE.
      have EB : B.2 = aVoid. case/mapP: HB => ? _ -> /=. by rewrite EQ.
      rewrite [B]surjective_pairing in HB. apply succ_CinU in HB.
      rewrite EB in HB *. rewrite supp_lit ?supp_con //.
      move: (supp_U HB). by rewrite in_fsetX => /andP[->].
    Qed.

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)].
    Proof.
      apply/allP => ?. case/mapP => C HC -> /=.
      apply/allP : HC. exact: JC_rcond.
    Qed.

  End Jumps.

  Lemma tree_for_0 L : L \in D -> tree_for (Tree L [::]) Dl D L.
  Proof. by rewrite /tree_for /= fset0F /s_cond !eqxx /= all_fset0. Qed.

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.
  Proof.
    move => inD. move: (inD). rewrite inE => /and3P [L1 L2 L3].
    have L_inU : (L,aVoid) \in U F by rewrite in_fsetX L1 AsV.
    rewrite /tree_for [rlab _]/= fset0U eqxx. apply/and4P; split => //.
  - rewrite /request_cond trespectsE mapK //. apply/andP; split.
    + apply/allP => ? /mapP [l _ ->]. exact: trespects_leaf.
    + move: (JC_rcond L3 L_inU ). apply: sub_all => L' //=. by rewrite fset0U.
  - rewrite /scomplete tlocalE. apply/andP; split.
    + apply/allP => ? /mapP [l _ ->] /=. by rewrite /s_cond fset0E eqxx.
    + rewrite mapK // -{1}[L]prV //= !fset0U. exact: JC_scond.
  - rewrite /j_tree [j_leafs]lock /= !fset0U -lock. rewrite (D_sub_Dl) // inD if_same andbT.
    apply/allP => T. case/mapP => C HC ->. rewrite labels_leaf. exact: JC_inD HC.
  Qed.

  Lemma simple_tree L : L \in D -> {T | ~~ trivial T && tree_for T Dl D L}.
  Proof. move => inD. exists (j_tree (L,aVoid)) => /=. exact: j_tree_for. Qed.

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.
  Proof.
    move => HL NP S R Tr.
    rewrite /tree_for eqxx /request_cond trespectsE /scomplete tlocalE S /= HL.
    rewrite !all_predI in Tr. case/and4P : Tr => p -> -> -> /=.
    rewrite set_of_nilp [nilp _](_ : _ = false) ?andbT; last by case: Ts NP {S R p}.
    apply/allP => ? /mapP [T inTs ->]. exact: (allP R).
  Qed.

  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).
  Proof.
    move => conA inU suppA litLs ar_a /and4P[_ T1 T2 T3] suppT; apply/and4P; split => //.
    - rewrite /request_cond trespectsE [j_leafs]lock /= -/(request_cond _) T1.
      rewrite /r_cond RU R1 fset0U (suppC_sub _ suppT) ?andbT ?andTb; auto with fset.
      apply/andP;split; rewrite -lock.
      + apply/allP => ?. case/mapP => ? ? ->. exact: trespects_leaf.
      + apply/allP => ?. case/mapP => ?. case/mapP => x Hx -> -> /=.
        move: (allP (JC_rcond conA inU)) => /(_ _ Hx). done.
    - rewrite [j_leafs]lock /scomplete tlocalE /= -/(scomplete _) T2 andTb.
      apply/andP;split; rewrite -lock.
      + apply/allP => ?. case/mapP => ? ? ->. by rewrite tlocalE /= /s_cond fset0F eqxx.
      + rewrite /s_cond; rightb. apply/allP => ?. case/fsetUP.
        * rewrite inE [supp]lock [j_leafs]lock => /eqP ->. case: (isDiaP _) => //= u [?].
          existsb (rlab T); rewrite ?set_ofE ?mem_head // -lock -suppC1.
          apply: suppC_sub suppT. by auto with fset.
        * move => inLs. rewrite [supp]lock [j_leafs]lock.
          move: (JC_scond conA inU) => /=. rewrite /s_cond (negbTE (JC_inhab _)) //=.
          move/allP => /(_ _ inLs). case: (isDiaP _) => //= u ?. subst.
          case/hasP => X X1 X2. existsb X; rewrite -lock //.
          rewrite !set_ofE in X1 *. rewrite in_cons. rightb.
          apply/mapP. exists (Tree X [::]) => //. rewrite /j_leafs mem_map //. by move => ? ? [].
    - rewrite [j_leafs]lock /= T3 /=. apply/andP;split.
      + apply/allP => X. rewrite -lock /j_leafs. case/mapP => L0 HL0 ->.
        rewrite labels_leaf. case/mapP: HL0 => ?. case/mapP => ? H -> -> /=.
        move/(RlconU conA inU) : (H) => H'. rewrite /= ar_a in H' *.
        rewrite inE. rewrite supp_lit // supp_con //. move: (supp_U H').
        rewrite in_fsetX. bcase.
      + rewrite set_of_nilp /= inE. rewrite -{1 3}suppA pr_inCs // cons_lcons //= andbT.
        rewrite /literalC allU -/(literalC Ls) litLs andbT.
        by rewrite all_fset1.
  Qed.

  Lemma supp_suppCl s C E : ((s |` C, E) \in U F) && consistent (s |` C, E) -> (support (s |` C) E) |> s.
  Proof. move => ?. rewrite -suppC1. exact: suppC_sub (supp_suppC _). Qed.

  Lemma supp_suppCr s C E : ((s |` C, E) \in U F) && consistent (s |` C, E) -> suppC (support (s |` C) E) C.
  Proof. move => ?. exact: suppC_sub (supp_suppC _). Qed.

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 }.
  Proof.
    move => U1.
    have H_in_Hs : H \in Hs F.
      case/andP: U1. rewrite in_fsetX => /andP [_]. rewrite AsAU //. by bcase.
    move: C U1. pattern H. set P := (fun _ => _). move: H_in_Hs. rewrite powersetE.
    apply: slack_ind => /= {H} H IH H_in_Hs C. rewrite /P in IH * => {P} /andP [U1 CC].
    case/orS : (ctab2 tab_AUh CC) => C2.
    -
      have U2 := tabU_AUhl sfc_F U1.
      have inD : support (t^+ |` C) aVoid \in D.
        rewrite inE supp_con ?supp_lit ?andbT; try bcase.
        suff : (support (t^+ |` C) aVoid, aVoid) \in U F by rewrite in_fsetX; bcase.
        by apply: supp_U; bcase.
      exists (Tree (support (t^+ |` C) aVoid) [::]). rewrite /=. rewrite suppCU /=; apply/andP; split.
        rewrite suppC1 /= suppF. leftb. by apply: supp_suppCl; bcase. by apply: supp_suppCr; bcase.
      apply/andP; split.
      + rewrite /tree_for /= fset0F !eqxx inD all_fset0 andbT /=. by rewrite /s_cond eqxx.
      + rewrite /a_cond /= fset0F eqxx suppF -suppC1. by apply: suppC_sub (fsubUl _ _) (supp_suppC _); bcase.

    -
      
      have U2 := tabU_AUhr sfc_F U1.
      have IH_cond : H `<` C |` H.
        rewrite fproper1. apply: contra CC => inH. rewrite (fset1U inH). by case (tab_dec _).
      have IH_cond2 : C |` H `<=` Cs F.
        rewrite fsubUset H_in_Hs andbT fsub1. case/fsetXP : U2. rewrite powersetU. by bcase.
      move: IH => /(_ _ IH_cond2 IH_cond) => /(all_sig_cond (Tree fset0 [::])) IH.

      set E := aAXU (s, t, C |` H) in U2 C2.
      set L := (support (s^+ |` C) E, E).
      have CL : consistent L by apply: supp_con; bcase.
      have CpL : lcons (pr L). exact: cons_lcons.

      set P := fun C0 => ((C0, aAU (s, t, C |` H)) \in U F) && consistent (C0, aAU (s, t, C |` H)).
      have SP : forall C0, C0 \in Rl L -> P C0.
        move => C0 inS. apply: (@succ_CinU L CL). by apply: supp_U; bcase.
        rewrite -[aAU _]/(aR E) mem_map //. by move => ? ? [].

      set Ts := map (sval IH) (Rl L).
      have/negbTE Ts_inhab : set_of [seq rlab i | i <- Ts] != fset0.
        by rewrite set_of_nilp.

      have /andP [Ts1 Ts2] : [all T in Ts, tree_for T Dl D (rlab T)] && [all T in Ts, tlocal (a_cond s t) T].
        rewrite -all_predI. apply/allP => x. case/mapP => C' /SP P_C' -> {x} /=. by case: (svalP IH C' P_C').

      exists (Tree (pr L) Ts); last (apply/andP; split).
      - rewrite /= suppCU. apply/andP; split.
        + rewrite suppC1 /= !inE /= andbT !suppF -!suppC1. rightb.
          apply: suppCWL. rewrite suppC1. by apply: supp_suppCl; bcase.
        + apply: suppCWL. by apply: supp_suppCr; bcase.
      - apply: tree_forI => //.
        + rewrite inE CpL pr_inCs //= ?andbT. rewrite /literalC allU.
          rewrite fset1Es /=. by apply: supp_lit; bcase. by apply: supp_U; bcase.
        + rightb. apply/allP => ?. case (isDiaP _) => //= u ->. case/fsetUP => [|inS]; first by rewrite inE => /eqP.
          existsb (rlab (sval IH (u^- |` R L.1))).
          * rewrite set_ofE in_cons. rightb. apply/mapP;eexists => //. apply/mapP; eexists => //.
            apply/mapP. exists (fAX u^-) => //. by rewrite inE.
          * rewrite -suppC1.
            have/(svalP IH) : P (u^- |` R L.1).
              apply: SP. rewrite inE. rightb. apply/mapP. exists (fAX u^-) => //. by rewrite inE.
            case => X _. apply: suppC_sub X. by rewrite /= fsub1 !inE.
        + apply/allP => T. case/mapP => C' inRl ->. move/(svalP IH) : (SP _ inRl) => [X _]. apply: suppC_sub X.
          apply RlR in inRl. rewrite RU /= R1. apply: fsetUSU. exact: subxx. apply: sub_trans inRl. exact: subxx.
      - rewrite tlocalE {2}/a_cond Ts_inhab Ts2 /= suppF -suppC1.
        apply: suppCWL. apply: suppC_sub (supp_suppC _); by [auto with fset | bcase].
  Qed.

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^+) }.
  Proof.
    move => inD /=.
    case: (boolP (L |> fAU s t^+)) => [|S]; last first.
    - case: (simple_tree inD) => T HT. rewrite /tree_for_and /tree_for'. exists T. by bcase.
    rewrite /= !suppF. case/orS => [St|].
    - case: (simple_tree inD) => T HT. exists T. rewrite /tree_for_and /tree_for'. by bcase.
    - move: (inD); rewrite inE => /and3P [L1 L2 L3] /andP [L4 L5].
      pose P C := ((C, aAU (s, t, fset0)) \in U F) && consistent (C, aAU (s, t, fset0)).
      have S1P : forall C, C \in Rl (L, aVoid) -> P C.
        move => C. rewrite in_cons. case/orP => [/eqP-> /=| /mapP [?]].
        - rewrite /P. apply/andP; split.
          apply: tabU_foc => //. rewrite -(R1 (fAX (fAU s t)^+)) -RU -(fset1U L5) -[aVoid]/(aR aVoid).
          apply: tabU_jmp => //. by rewrite in_fsetX L1 AsV.
          apply: (ctab1 tab_foc). rewrite -(R1 (fAX (fAU s t)^+)) -RU -(fset1U L5) -[aVoid]/(aR aVoid).
          exact: (ctab1 tab_jmp).
        - rewrite inE andbC. case: (isDiaP _) => //= u -> Hu -> /=. rewrite /P. apply/andP; split.
          + apply: tabU_foc => //. rewrite fsetUCA -(R1 (fAX (fAU s t)^+)) -RU -(fset1U L5) -[aVoid]/(aR aVoid).
            apply: tabU_AXn => //. by rewrite in_fsetX -(fset1U Hu) L1 AsV.
          + apply: (ctab1 tab_foc). rewrite fsetUCA -(R1 (fAX (fAU s t)^+)) -RU -(fset1U L5) -[aVoid]/(aR aVoid).
            apply: (ctab1 tab_AXn). by rewrite -(fset1U Hu).

      have tree_AUH' := all_sig_cond (Tree fset0 [::] : tree clause) (@tree_AUH fset0 s t).
      pose treeH := sval tree_AUH'.

      exists (Tree L (map treeH (Rl (L,aVoid)))). apply/andP; split => //.
      rewrite /tree_for_and. apply/andP; split.
        + rewrite /tree_for'. do 2 rightb. rewrite tlocalE. apply/andP; split.
          apply/allP => ? /mapP [C] /S1P HC ->. by case : (svalP tree_AUH' _ HC) => _ /andP[_].
        + by rewrite /a_cond L4 set_of_nilp.
        + apply: tree_forI => //.
          * exact: D_sub_Dl.
          * rightb. apply/allP => ?. case (isDiaP _) => // u -> inL.
            have B: body (fAX u^-) |` R L \in Rl (L,aVoid). rewrite in_cons. rightb. apply: map_f. by rewrite inE /= inL.
            existsb (rlab (treeH (body (fAX u^-) |` R L))). by rewrite set_ofE map_f // map_f.
            rewrite /= suppF -suppC1. case : (svalP tree_AUH' _ (S1P _ B)) => X _.
            apply: suppC_sub X. by rewrite /= fsub1 3!inE fset11.
          * apply/allP => ?. case/mapP => C' inRl ->.
            rewrite /r_cond. case: (svalP tree_AUH' _ (S1P _ inRl)) => X _. apply: suppC_sub X.
            apply: sub_trans (RlR inRl) _. exact: fsubUr.
          * apply/allP => ?. case/mapP => C' inRl ->. by case: (svalP tree_AUH' _ (S1P _ inRl)) => _ /andP [? ?].
  Qed.

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]}.
  Proof.
    move => U1.
    have H_in_Hs : H \in Hs F.
      case/andP: U1. rewrite in_fsetX => /andP [_]. rewrite AsAR //. by bcase.
      move: C U1. pattern H. set P := (fun _ => _). move: H_in_Hs. rewrite powersetE.
    apply: slack_ind => /= {H} H IH H_in_Hs C. rewrite /P in IH * => {P} /andP [U1 CC].
    case/orS : (ctab2 tab_ARh CC) => C2.
    - set L := support (t^- |` C) aVoid.
      have LCU : ((t^- |` C,aVoid) \in U F) && consistent (t^- |` C, aVoid).
        rewrite C2 andbT. exact: tabU_ARhl U1.
      move:(supp_suppC LCU). rewrite -/L /= suppCU suppC1 => /andP [A ?].
      exists (Tree L [::]).
      + rewrite /= !suppCU !suppC1 /= !suppF. by bcase.
      + rewrite tree_for_0 /= ?suppF ?A /= ?fset0F ?all_fset0 //.
        rewrite inE. rewrite supp_con // supp_lit //. move: (supp_U LCU).
        rewrite in_fsetX /L. by bcase.
    - have IH_cond : H `<` C |` H.
        rewrite fproper1. apply: contra CC => inH. rewrite (fset1U inH). by case (tab_dec _).
      have IH_cond2 : C |` H `<=` Cs F.
        rewrite fsubUset H_in_Hs andbT fsub1. by case/fsetXP : U1.       set E := aAXR (s, t, C |` H) in C2.
      set Ls := support (s^- |` C) E.
      set L := pr (Ls,E).
      have LCU : ((s^- |` C,E) \in U F) && consistent (s^- |` C, E).
        rewrite C2 andbT. exact: tabU_ARhr.
      have CLE: consistent (Ls,E). exact: supp_con.
      have CP: lcons L. exact: cons_lcons.
      have CX: ((R Ls, aAR (s, t, C |` H)) \in U F)
              && consistent (R Ls, aAR (s, t, C |` H)).
        apply/andP; split; last exact: (ctab1 tab_aAXR).
        apply: tabU_aAXR => //. apply: supp_U. by bcase.
      case: (IH _ IH_cond2 IH_cond _ CX) => TH T1 /and3P[T2 T3 T4].
      exists (Tree L (TH :: [seq Tree L0 [::] | L0 <- JCs (Ls,E)])).
      + move: (supp_suppC LCU). rewrite -/Ls !suppCU /L /= => /andP [? ?].
        apply/andP;split; last exact: suppCWL.
        rewrite suppC1 /= !suppF !inE orTb andbT -!suppC1. rightb. exact: suppCWL.
        rewrite /rlab. apply/and3P; split.
      + apply: tree_for_cons => //.
        * rewrite /Ls. exact: supp_U.
        * apply: supp_lit. bcase.
      + rewrite trespectsE. apply/andP; split.
        * rewrite [JCs]lock /= T3 /=. apply/allP => ?. case/mapP => ? _ ->. exact: trespects_leaf.
        * apply/allP => ? _. rewrite /u_cond /L /= suppF.
          move: (supp_suppCl LCU). rewrite -!suppC1. exact: suppCWL.
      + rewrite /=. bcase.
  Qed.

  Lemma tree_AR L s t : L \in D -> { T | ~~ trivial T && tree_for_and T Dl D L (fAR s t^-) }.
  Proof.
    move => inD.
    case: (boolP (L |> fAR s t^-)) => [|S]; last first.
    - case: (simple_tree inD) => T HT. exists T. rewrite /tree_for_and /tree_for'. by bcase.
    rewrite /= !suppF classic_orb. case/orS.
    - case: (simple_tree inD) => T HT Ls. exists T.
      rewrite /tree_for_and /tree_for'. by bcase.
    - move: (inD); rewrite inE => /and3P [L1 L2 L3] /and3P [L6 L4 L5].
      have C1: consistent (fAR s t^- |` R L, aVoid).
        rewrite -[aVoid]/(aR aVoid). apply: (ctab1 tab_AXn). by rewrite -(fset1U L5).
      have CH: ((R L, aAR (s, t, fset0)) \in U F) && consistent (R L, aAR (s, t, fset0)).
        apply/andP; split; last exact: (ctab1 tab_foc').
        apply: tabU_aAXR => //. by rewrite -AXR_shift // -(fset1U L5) L1 powersetE sub0x.
      case: (tree_ARH CH) => TH T1 /and3P[T2 t3 T4].
      exists (Tree L (TH :: [seq Tree L0 [::] | L0 <- JCs (L,aVoid)])).
      rewrite [JCs]lock /= -lock. apply/andP; split.
      + rewrite /tree_for'. do 2 rightb. rewrite [JCs]lock /= -!andbA -!lock.
        apply/and4P; split => //.
        * apply/allP => ?. case/mapP => ? _ ->. exact: trespects_leaf.
        * apply/allP => x. rewrite set_ofE in_cons. case/orP => [/eqP ->|] //. by bcase.
      + rewrite {1 3}(fset1U L5).
        apply: tree_for_cons => //.
        * by rewrite in_fsetX AsV.
        * by rewrite /= fset0U -(fset1U L5).
   Qed.

  Lemma tree_demo L u : (u \in F) -> (L \in D) -> { T | ~~ trivial T && tree_for_and T Dl D L u }.
  Proof.
    case: u => [[|x|s t|s|s t|s t]] [|] inF inD;
      try by [case: (simple_tree inD) => T HT; exists T; rewrite /tree_for_and /tree_for'].
    - exact: tree_AR.
    - exact: tree_AU.
  Qed.

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.
  Proof. done. Qed.

  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).
  Proof.
    move/rgraph_of_local => H x.
    move/forallP : H => /(_ x). case: (boolP (_ == fset0)) => H.
    - suff -> : leaf x by []. apply: contraL H => /existsP [y xy].
      apply/emptyPn; exists (label y). by rewrite in_fimset // inE in_fsetT.
    - suff/negbTE -> : ~~ leaf x by []. case/emptyPn : H => ? /fimsetP [y y1 _].
      rewrite inE in_fsetT negbK in y1 *. by apply/existsP; exists y.
   Qed.

  Lemma graph_has t (T: tree clause) : t_has t T -> ge_cond t (rgraph_of T).
  Proof.
    move => H. suff [U U1 U2] : exists2 U, U \in subtrees T & rlab U |> t^-.
      by apply/existsP; exists (SeqSub _ U1).
    move: T H. apply: simple_tree_rect => C Ts IH /orP [supp|/hasP [U' in_Ts]].
    - exists (Tree C Ts) => //. exact: mem_head.
    - case/(IH _ in_Ts) => U'' U3 U4. exists U'' => //. apply: subtrees_trans U3 _.
      exact: subtrees1.
  Qed.

  Lemma tab_demo : demo F Dl D.
  Proof.
    move => L u inF inD. pose T := (tree_demo inF inD).
    exists (rgraph_of (sval T)). move: (svalP T) => /andP [nt /andP [tf' tf]].
    case/and4P: tf => rl rc sc lf.
    - split. by rewrite rgraph_of_root (eqP rl).
    - split. exact: rgraph_of_acyclic.
    - split. exact: rgraph_of_local.
    - split. exact: rgraph_of_respects.
    - split.       case/orP : tf' => H; [leftb|rightb];first by rewrite rgraph_of_root (eqP rl).
      move: H. move: {inF T nt rc sc lf} (sval T) rl. case: u => [[|p|s t|s|s t|s t]] //.
      + case => // T /eqP e. case/orP; first by rewrite rgraph_of_root e => ->.
        case/andP => [U E]. rightb. apply/andP; split.
        exact: rgraph_of_respects. exact: graph_has.
      + case => // T /eqP e. case/orP; first by rewrite rgraph_of_root e => ->.
        case (_ |> _) => //=. exact: rgraph_of_local.
    - split. rewrite negbK. destruct (sval T) as [l ts]. destruct ts as [|t ts] => //.
      have inT: t \in subtrees (Tree l (t :: ts)). by rewrite /= in_cons mem_cat subtrees_refl.
      apply/existsP. exists (SeqSub _ inT). by rewrite /= /graph_of_rel /= mem_head.
    - exact: graph_of_labels.
  Qed.

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.
Proof. move => x. by exists x. Qed.

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.
Proof.
  case: (fset0Vmem C) => [-> _ |[s inC] not_bl].
  - exists unit_model. exists tt. split => [|?]; [apply: finiteI => //| by rewrite inE].
  - pose F := @closed_sfc C. pose GD := tab_demo F. pose L := support F C aVoid.
    have con_in_U : ((C, aVoid) \in U (sfc C)) && consistent (C, aVoid).
      rewrite in_fsetX AsV powersetE sub_sfc //=. apply/negP. by case: (tab_dec _).
    have in_sfc : s \in (sfc C). exact: (subP (sub_sfc _)).
    have inDF : L \in D (sfc C). rewrite inE supp_lit // supp_con //.
      move: (supp_U F con_in_U). by case/fsetXP => ->.
    pose p := (SeqSub _ in_sfc, SeqSub _ inDF).
    exists (MD GD). exists (existT p (root (Dmatrix GD p))).
    split; first exact: fin_finite.
    move => t t_inC. apply: supp_eval => //=.
    + exact: D_sub_Dl.
    + rewrite /Dl => D. rewrite !inE. bcase.
    + rewrite label_root /= -suppC1.
      apply: suppC_sub; last by apply supp_suppC. by rewrite fsub1.
Qed.