Library Deci

Require Import LFS2 Semi.

Tactic Notation "done" := (subst; simpl; auto; clear; now firstorder).

Syntactic closures

Definition sf_closed' (S : sform) (C : clause) : Prop :=
  match S with
    | + Imp s t-s C +t C
    | - Imp s t+s C -t C
    | _True

Definition sf_closed (C : clause) : Prop :=
   S, S Csf_closed' S C.

Lemma sf_closed_app C D :
  sf_closed Csf_closed Dsf_closed (C++D).

Lemma sf_closed_cons S C T :
  S Csf_closed Csf_closed' S (T::C).

Complication: We cannot recurse through signed formulas.

Fixpoint scl' (b : bool) (s : form) : clause :=
  sign b s :: match s with
                  | Imp s1 s2scl' (negb b) s1 ++ scl' b s2
                  | _nil

Fixpoint scl (C: clause) : clause :=
  match C with
    | nilnil
    | +s :: C'scl' true s ++ scl C'
    | -s :: C'scl' false s ++ scl C'

Lemma in_scl' b s :
  sign b s scl' b s.

Lemma scl'_correct b s :
  sf_closed (scl' b s).

Lemma scl_correct C :
  sf_closed (scl C) C scl C.

Decidability of tableaux

We show that tab is decidable using the decidability theorem for finite least fixpoints. We start with the step predicate, which we define based on a support predicate (read sup A C as "A supports C")

Definition sup (A : list clause) (C : clause) : Prop :=
   D, D A D C.

Definition step' (A : list clause) (S : sform) (C : clause) : Prop :=
  match S with
    | + FalTrue
    | - Var x+Var x C
    | + Imp s tsup A (-s :: C) sup A (+t :: C)
    | - Imp s tsup A (+s :: -t :: pos C)
    | _False

Definition step (A : list clause) (C : clause) : Prop :=
   S, S C step' A S C.

Lemma sup_mono A B C :
  A Bsup A Csup B C.

Lemma sup_mono' A C C' :
  sup A CC C'sup A C'.

Lemma step_mono A B C :
  A Bstep A Cstep B C.

Lemma stepW A C C' :
  C C'step A Cstep A C'.

Instance step_equi_proper :
  Proper (eq ==> @equi sform ==> iff) step.

Lemma step_dec A C :
  dec (step A C).

Instance tab_equi_proper :
  Proper (@equi sform ==> iff) tab.

Lemma tab_push S C :
  S C → (tab C tab (S::C)).

Section Decidability.
  Variable U : clause.
  Variable sfcU : sf_closed U.

  Lemma lfp_tab C :
    lfp step (power U) Ctab C.

  Lemma lfpW C C' :
    C' power UC C'lfp step (power U) Clfp step (power U) C'.

  Lemma pos_imp_U s t C :
    +Imp s t :: C U-s :: C U +t :: C U.

  Lemma neg_imp_U s t C :
    -Imp s t :: C U+s :: -t :: C U.

  Lemma tab_lfp C :
    C Utab Clfp step (power U) (rep C U).

  Lemma tab_dec' C :
    C Udec (tab C).

End Decidability.

Lemma tab_dec C :
  dec (tab C).

Canonical demos

Let U be a subformula-closed clause. We show that the system of maximal consistent subclauses of U is a demo (called the canonoical demo for U), and that every consistent subset of U can be extended to a maximal consistent subclause of U. Thus the canonical demo for U satisfies every consistent subset of U. We assume that tab is decidable.

Definition con C := ¬ tab C.

Lemma conW C C' :
  con CC' Ccon C'.

Lemma con_pos_imp C s t :
  ( C, dec (tab C)) →
  +Imp s t Ccon Ccon (-s :: C) con (+t :: C).

Lemma con_neg_imp C s t :
  -Imp s t Ccon Ccon (+s :: -t :: pos C).

Section CanonicalDemo.
  Variable U : clause.
  Variable sfcU : sf_closed U.
  Context {tab_dec : C, dec (tab C)}.

Extension to maximal consistent subclauses

  Lemma extension C :
    C Ucon C{C' | C' power U C C' qmax con U C'}.

The system of maximal consistent subclauses of U is a demo satisfying every consistent subset of U.

  Definition CD : model :=
    filter (qmax con U) (power U).

  Lemma CD_demo :
    demo CD.

  Lemma CD_con_satis C :
    C Ucon C A, A CD C A satis' CD A C.

End CanonicalDemo.

Main lemma

Lemma main C :
  {sat C} + {tab C}.