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

Fixpoint scl (C: clause) : clause :=
match C with
| nilnil
| +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
| + 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
end.

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

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