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
  end.

Definition sf_closed (C : clause) : Prop :=
  ∀ S, S ∊ C → sf_closed' S C.

Lemma sf_closed_app C D :
  sf_closed C → sf_closed D → sf_closed (C ++D).

Lemma sf_closed_cons S C T :
  S ∊ C → sf_closed C → sf_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 s2 ⇒ scl' (negb b) s1 ++ scl' b s2
                  | _ ⇒ nil
                end.

Fixpoint scl (C: clause) : clause :=
  match C with
    | nil ⇒ nil
    | +s :: C' ⇒ scl' true s ++ scl C'
    | -s :: C' ⇒ scl' false s ++ scl C'
  end.

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
    | + Fal ⇒ True
    | - Var x ⇒ +Var x ∊ C
    | + Imp s t ⇒ sup A (-s :: C) ∧ sup A (+t :: C)
    | - Imp s t ⇒ sup A (+s :: -t :: pos C)
    | _ ⇒ False
  end.

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

Lemma sup_mono A B C :
  A ⊆ B → sup A C → sup B C.

Lemma sup_mono' A C C' :
  sup A C → C ⊆ C' → sup A C'.

Lemma step_mono A B C :
  A ⊆ B → step A C → step B C.

Lemma stepW A C C' :
  C ⊆ C' → step A C → step 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) C → tab C.

  Lemma lfpW C C' :
    C' ∊ power U → C ⊆ C' → lfp step (power U) C → lfp 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 ⊆ U → tab C → lfp step (power U) (rep C U).

  Lemma tab_dec' C :
    C ⊆ U → dec (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.

Consistency

Definition con C := ¬ tab C.

Lemma conW C C' :
  con C → C' ⊆ C → con C'.

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

Lemma con_neg_imp C s t :
  -Imp s t ∊ C → con C → con (+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 ⊆ U → con 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 ⊆ U → con C → ∃ A, A ∊ CD ∧ C ⊆ A ∧ satis' CD A C.

End CanonicalDemo.

Main lemma

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