Require Export PropL.
Implicit Types x y z : var.
Implicit Types s t : form.
Implicit Types alpha beta : assn.
Implicit Types A B : context.
Implicit Types m n k : nat.
Implicit Types x y z : var.
Implicit Types s t : form.
Implicit Types alpha beta : assn.
Implicit Types A B : context.
Implicit Types m n k : nat.
Fixpoint eval alpha s : bool :=
match s with
| Var x ⇒ alpha x
| Imp s t ⇒ if eval alpha s then eval alpha t else true
| Fal ⇒ false
end.
Fixpoint satis alpha s : Prop :=
match s with
| Var x ⇒ if alpha x then True else False
| Imp s1 s2 ⇒ satis alpha s1 → satis alpha s2
| Fal ⇒ False
end.
Lemma satis_eval alpha s :
satis alpha s ↔ eval alpha s = true.
Instance satis_dec alpha s : dec (satis alpha s).
Lemma satis_pos_imp alpha s t :
satis alpha (Imp s t) ↔ ¬ satis alpha s ∨ satis alpha t.
Lemma satis_neg_imp alpha s t :
¬ satis alpha (Imp s t) ↔ satis alpha s ∧ ¬ satis alpha t.
Definition valid s : Prop :=
∀ alpha, satis alpha s.
Lemma valid_unsat s :
valid s ↔ ¬ ∃ alpha, satis alpha (Not s).
Definition bent A s : Prop :=
∀ alpha, (∀ t, t el A → satis alpha t) → satis alpha s.
Lemma ndc_bent A s :
ndc A s → bent A s.
Inductive sform : Type :=
| Pos : form → sform
| Neg : form → sform.
Definition clause := list sform.
Notation "+ s" := (Pos s) (at level 35).
Notation "- s" := (Neg s).
Implicit Types S T : sform.
Implicit Types C D : clause.
Instance sform_eq_dec S T : dec (S = T).
Definition uns S : form :=
match S with +s ⇒ s | -s ⇒ Not s end.
Fixpoint satis' alpha C : Prop :=
match C with
| nil ⇒ True
| T::C' ⇒ satis alpha (uns T) ∧ satis' alpha C'
end.
Definition sat C := ∃ alpha, satis' alpha C.
Lemma satis_iff alpha C :
satis' alpha C ↔ ∀ S, S el C → satis alpha (uns S).
Lemma satis_in alpha C S :
satis' alpha C → S el C → satis alpha (uns S).
Lemma satis_weak alpha C C' :
C <<= C' → satis' alpha C' → satis' alpha C.
Lemma sat_weak C C' :
C <<= C' → sat C' → sat C.
Entailment of clauses
Definition cent C D : Prop :=
∀ alpha, satis' alpha C → satis' alpha D.
Lemma cent_weak C D D' :
D <<= D' → cent C D' → cent C D.
Lemma cent_sat C D :
cent C D → sat C → sat D.
Definition svar S : Prop :=
match S with
| +Var _ | -Var _ ⇒ True
| _ ⇒ False
end.
Definition solved C : Prop :=
(∀ S, S el C → svar S) ∧ ∀ x, +Var x el C → ¬ -Var x el C.
Definition phi C x := if decision (+Var x el C) then true else false.
Lemma solved_phi C :
solved C → satis' (phi C) C.
Lemma solved_sat C :
solved C → sat C.
Lemma solved_nil :
solved nil.
Lemma solved_pos_var x C :
solved C → ¬ -Var x el C → solved (+Var x :: C).
Lemma solved_neg_var x C :
solved C → ¬ +Var x el C → solved (-Var x :: C).
Lemma cent_solved_sat C D :
cent C D → solved C → sat D.
Record ref_pred (rho : clause → Prop) :=
{ ref_Fal : ∀ C, +Fal el C → rho C;
ref_weak : ∀ C C', C <<= C' → rho C → rho C';
ref_clash : ∀ x C, +Var x el C → -Var x el C → rho C;
ref_pos_imp : ∀ s t C, rho (-s::C) → rho (+t::C) → rho (+Imp s t::C);
ref_neg_imp : ∀ s t C, rho (+s::-t::C) → rho (-Imp s t::C);
ref_sound : ∀ C, rho C → ¬ sat C }.
Lemma ref_unsat :
ref_pred (fun C ⇒ ¬ sat C).
Lemma ref_ndc :
ref_pred (fun C ⇒ ndc (map uns C) Fal).
Inductive rec C : clause → Type :=
| recNil : rec C nil
| recPF D : rec C (+Fal :: D)
| recNF D : rec C D → rec C (-Fal ::D)
| recPV D x : -Var x el C → rec C (+Var x :: D)
| recPV' D x : ¬ -Var x el C → rec (+Var x :: C) D → rec C (+Var x :: D)
| recNV D x : +Var x el C → rec C (-Var x :: D)
| recNV' D x : ¬ +Var x el C → rec (-Var x :: C) D → rec C (-Var x :: D)
| recPI D s t : rec C (-s :: D) → rec C (+t :: D) → rec C (+Imp s t :: D)
| recNI D s t : rec C (+s :: -t :: D) → rec C (-Imp s t :: D).
Fixpoint sizeF s : nat :=
match s with
| Imp s1 s2 ⇒ 1 + sizeF s1 + sizeF s2
| _ ⇒ 1
end.
Fixpoint size C : nat :=
match C with
| nil ⇒ 0
| +s::C' ⇒ sizeF s + size C'
| -s::C' ⇒ sizeF s + size C'
end.
Definition provider C D : rec C D.
Section RL.
Variable rho : clause → Prop.
Variable Rho : ref_pred rho.
Definition decider C D :
rec C D → solved C →
{E | solved E ∧ cent E (D ++ C)} + {rho (D ++ C)}.
Lemma solved_ref C :
{D| solved D ∧ cent D C} + {rho C}.
Lemma refutation C :
{sat C} + {rho C}.
Lemma ref_iff_unsat C :
rho C ↔ ¬ sat C.
Lemma ref_dec C :
dec (rho C).
End RL.