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.
Require Import CTL_def tab_def.

Set Implicit Arguments.
Import Prenex Implicits.

Hint Constructors tab.

Decidability of Tableau Derivability

We show decidability of tab derivability in three steps.

1) Define a syntactic universe that is closed under backward application of the rules 2) Show that this entails that derivability inside a given universe is decidable 3) Show that every annotated clause is contained in some syntactic universe

Part 1: Syntactic Universe

Section tab_closure.
  Variable F : {fset sform }.
  Hypothesis sfc_F : sf_closed F.

  Lemma sf_AU s t b : ((fAU s t ,b ) \in F ) = ((fAX (fAU s t),b ) \in F ).

  Lemma sf_AR s t b : ((fAR s t ,b ) \in F ) = ((fAX (fAR s t),b ) \in F ).

  Definition Cs := powerset F.
  Definition Hs := powerset Cs.

  Definition AUs := [fset p in positives F `x ` positives F | fAU p.1 p.2 ^+ \in F ].
  Definition ARs := [fset p in negatives F `x ` negatives F | fAR p.1 p.2 ^- \in F ].

  Definition As :=
    aVoid |` [fset aAU (p,H) | p <- AUs , H <-Hs ]
         `|` [fset aAXU (p,H) | p <- AUs , H <-Hs ]
         `|` [fset aAR (p,H) | p <- ARs , H <-Hs ]
         `|` [fset aAXR (p,H) | p <- ARs , H <-Hs ].

  Definition U : {fset clause * annot } := Cs `x ` As.

  Lemma AsX p H : (aAU (p , H ) \in As ) = (aAXU (p , H ) \in As ).

  Lemma AsAU s t H : aAU (s ,t ,H ) \in As = [&& fAU s t ^+ \in F & H \in Hs ].

  Lemma AsAXU s t H : aAXU (s ,t ,H ) \in As = [&& fAX (fAU s t)^+ \in F & H \in Hs ].

  Lemma AsX' p H : (aAR (p , H ) \in As ) = (aAXR (p , H ) \in As ).

  Lemma AsAR s t H : aAR (s ,t ,H ) \in As = [&& fAR s t ^- \in F & H \in Hs ].

  Lemma AsAXR s t H : aAXR (s ,t ,H ) \in As = [&& fAX (fAR s t)^- \in F & H \in Hs ].

  Lemma AsV : aVoid \in As.

  Lemma AU_shift s t C H : (fAU s t ^+ |` C \in Cs ) && (H \in Hs ) = ((C ,aAU (s ,t ,H )) \in U ).

  Lemma AXU_shift s t C H : (fAX (fAU s t)^+ |` C \in Cs ) && (H \in Hs ) = ((C ,aAXU (s ,t ,H )) \in U ).

  Lemma AR_shift s t C H : (fAR s t ^- |` C \in Cs ) && (H \in Hs ) = ((C ,aAR (s ,t ,H )) \in U ).

  Lemma AXR_shift s t C H : (fAX (fAR s t)^- |` C \in Cs ) && (H \in Hs ) = ((C ,aAXR (s ,t ,H )) \in U ).

U is closed under backward application of tableau rules

  Lemma subCs s C : s |` C \in Cs -> s \in F.

  Lemma subU t X C A :
    (sf_closed' F t -> X `<=` F) -> (t |` C ,A ) \in U -> (X `|` C ,A ) \in U.

  Lemma RinU (C : clause) : C \in Cs -> R C \in Cs.

  Lemma tabU_ipl s t C E : (fImp s t ^+ |` C , E ) \in U -> (s ^- |` C , E ) \in U.

  Lemma tabU_ipr s t C E : (fImp s t ^+ |` C , E ) \in U -> (t ^+ |` C , E ) \in U.

  Lemma tabU_in s t C E : (fImp s t ^- |` C , E ) \in U -> ([fset s ^+ , t ^- & C ], E ) \in U.

  Lemma tabU_aR E : E \in As -> aR E \in As.

  Lemma tabU_AXn s C E : (fAX s ^- |` C , E ) \in U -> (s ^- |` R C , aR E ) \in U.

  Lemma tabU_AUpl s t C E : (fAU s t ^+ |` C ,E ) \in U -> (t ^+ |` C ,E ) \in U.

  Lemma tabU_AUpr s t C E : (fAU s t ^+ |` C ,E ) \in U -> ([fset s ^+, fAX (fAU s t)^+ & C ],E ) \in U.

  Lemma tabU_AUnl s t C E : (fAU s t ^- |` C , E ) \in U -> ([fset s ^-, t ^- & C ], E ) \in U.

  Lemma tabU_AUnr s t C E : (fAU s t ^- |` C , E ) \in U -> ([fset t ^-, fAX (fAU s t)^- & C ],E ) \in U.

  Lemma tabU_foc s t C : (fAU s t ^+ |` C , aVoid ) \in U -> (C ,aAU (s , t , fset0 )) \in U.

  Lemma tabU_AUhl s t H C : (C , aAU (s , t , H )) \in U -> (t ^+ |` C , aVoid ) \in U.

  Lemma tabU_AUhr s t H C : (C , aAU (s , t , H )) \in U -> (s ^+ |` C , aAXU (s , t , C |` H )) \in U.

  Lemma tabU_jmp C E : (C ,E ) \in U -> (R C , aR E ) \in U.

  Lemma pr_inCs A : A \in U -> pr A \in Cs.

  Lemma tabU_ufoc A : A \in U -> (pr A , aVoid ) \in U.

  Lemma tabU_ARpl s t C E : (fAR s t ^+ |` C ,E ) \in U -> ([fset s ^+, t ^+ & C ],E ) \in U.

  Lemma tabU_ARpr s t C E : (fAR s t ^+ |` C ,E ) \in U -> ([fset t ^+, fAX (fAR s t)^+ & C ],E ) \in U.

  Lemma tabU_ARnl s t C E : (fAR s t ^- |` C ,E ) \in U -> (t ^- |` C ,E ) \in U.

  Lemma tabU_ARnr s t C E : (fAR s t ^- |` C ,E ) \in U -> ([fset s ^-, fAX (fAR s t)^- & C ],E ) \in U.

  Lemma tabU_ARhl s t H C : (C , aAR (s , t , H )) \in U -> (t ^- |` C , aVoid ) \in U.

  Lemma tabU_ARhr s t H C : (C , aAR (s , t , H )) \in U -> (s ^- |` C , aAXR (s , t , C |` H )) \in U.

  Lemma tabU_foc' s t C : (fAR s t ^- |` C , aVoid ) \in U -> (C , aAR (s , t , fset0 )) \in U.

  Lemma tabU_aAXR s t H C : (C , aAXR (s , t , H )) \in U -> (R C , aAR (s , t , H )) \in U.

  Hint Resolve tabU_ipl tabU_ipr tabU_in tabU_AXn tabU_AUpl tabU_AUpr tabU_AUnl tabU_AUnr tabU_AUhl tabU_AUhr tabU_foc tabU_jmp.

Part 2 : Decidability inside a universe

  Definition step_plain_cases (D : {fset clause * annot }) (C : clause) s E :=
    match s with
      | fF ^+ => true
      | fV p^+ => fV p^- \in C
      | (fImp t1 t2)^+ => ((t1^- |` C ,E ) \in D ) && ((t2^+ |` C ,E ) \in D )
      | (fImp t1 t2)^- => ([fset t1^+, t2^- & C ],E ) \in D
      | fAX s^- => (s ^- |` R C ,aR E ) \in D
      | fAU s t^+ => ((t^+ |` C ,E ) \in D ) && (([fset s ^+, fAX (fAU s t)^+ & C ],E ) \in D )
      | fAU s t^- => (([fset s ^-, t^- & C ], E ) \in D ) && (([fset t^-, fAX (fAU s t)^- & C ],E ) \in D )
      | fAR s t^+ => (([fset s ^+, t^+ & C ], E ) \in D ) && (([fset t^+, fAX (fAR s t)^+ & C ],E ) \in D )
      | fAR s t^- => ((t^- |` C ,E ) \in D ) && (([fset s ^-, fAX (fAR s t)^- & C ],E ) \in D )
      | _ => false
    end.

  Definition step_plain (D : {fset clause * annot }) (A : clause * annot) :=
    [some s in F , [some C in Cs , [some E in As , (A == (s |` C, E)) && step_plain_cases D C s E]]].

  Definition step_annot (D : {fset clause * annot }) A :=
    let: (C,E) := A in
    match E with
      | aAU (s, t, H) => ((t^+ |` C, aVoid ) \in D ) && ((s^+ |` C, aAXU (s, t, C |` H)) \in D ) || (C \in H)
      | aVoid => [some s in positives F , [some t in positives F , [some C' in Cs ,
                          (C == fAU s t^+ |` C') && ((C', aAU (s, t, fset0 )) \in D )]]]
|| [some s in negatives F , [some t in negatives F , [some C' in Cs ,
                          (C == fAR s t^- |` C') && ((C', aAR (s, t, fset0 )) \in D )]]]
| aAR (s, t, H) => ((t^- |` C, aVoid ) \in D ) && ((s^- |` C, aAXR (s, t, C |` H)) \in D ) || (C \in H)
      | aAXR (s ,t, H) => (R C,aAR (s,t,H)) \in D
      | _ => false
    end.

  Definition step_jmp (D : {fset clause * annot }) (A : clause * annot) :=
    let (C,E) := A in (R C , aR E ) \in D.

  Definition step (D : {fset clause * annot }) : {fset clause * annot } :=
    [fset A in U | [|| step_plain D A, step_annot D A| step_jmp D A ]].

  Lemma bounded_step : bounded U step.

  Lemma mono_step : monotone step.

  Lemma plainP C u E :
    step_plain_cases (fset.lfp U step) C u E -> (u |` C ,E ) \in U -> step_plain (fset.lfp U step) (u |` C ,E ).

  Lemma stepP (A : clause * annot) : A \in U -> reflect (tab A) (A \in fset.lfp U step).

  Lemma tab_decF (A : clause * annot) : A \in U -> decidable (tab A).

End tab_closure.

Part 3: Existence of universes for all clauses

Definition sfc C : clause := \bigcup_(s in C ) ssub s.

Lemma sfc_bigcup (T : choiceType) (C : {fset T }) S :
  (forall s, sf_closed (S s)) -> sf_closed (\bigcup_(s in C ) S s).

Lemma closed_sfc C : sf_closed (sfc C).

Lemma sub_sfc C : C `<=` (sfc C ).

Lemma plain_inU {C} : (C ,aVoid ) \in U (sfc C).

Lemma aAU_inU {C s t H} :
  (C ,aAU (s , t , H )) \in U (sfc (fAU s t ^+ |` C `|` \bigcup_(C' in H ) C')).

Lemma aAR_inU {C s t H} :
  (C ,aAR (s , t , H )) \in U (sfc (fAR s t ^- |` C `|` \bigcup_(C' in H ) C')).

Lemma aAXU_inU {C s t H} :
  (C ,aAXU (s , t , H )) \in U (sfc (fAU s t ^+ |` C `|` \bigcup_(C' in H ) C')).

Lemma aAXR_inU {C s t H} :
  (C ,aAXR (s , t , H )) \in U (sfc (fAR s t ^- |` C `|` \bigcup_(C' in H ) C')).

Lemma tab_dec A : decidable (tab A).