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.

Boolean satisfaction

Fixpoint eval alpha s : bool :=
  match s with
    | Var xalpha x
    | Imp s tif eval alpha s then eval alpha t else true
    | Falfalse

Fixpoint satis alpha s : Prop :=
  match s with
    | Var xif alpha x then True else False
    | Imp s1 s2satis alpha s1satis alpha s2
    | FalFalse

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.

Validity and boolean entailment

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 Asatis alpha t) → satis alpha s.

Lemma ndc_bent A s :
  ndc A sbent A s.

Signed formulas and clauses

Inductive sform : Type :=
| Pos : formsform
| Neg : formsform.

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 +ss | -sNot s end.

Fixpoint satis' alpha C : Prop :=
  match C with
    | nilTrue
    | T::C'satis alpha (uns T) satis' alpha C'

Definition sat C := alpha, satis' alpha C.

Lemma satis_iff alpha C :
  satis' alpha C S, S el Csatis alpha (uns S).

Lemma satis_in alpha C S :
  satis' alpha CS el Csatis 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 Csatis' alpha D.

Lemma cent_weak C D D' :
  D <<= D'cent C D'cent C D.

Lemma cent_sat C D :
  cent C Dsat Csat D.

Solved Clauses

Definition svar S : Prop :=
  match S with
    | +Var _ | -Var _True
    | _False

Definition solved C : Prop :=
  ( S, S el Csvar 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 Csatis' (phi C) C.

Lemma solved_sat C :
  solved Csat C.

Lemma solved_nil :
  solved nil.

Lemma solved_pos_var x C :
  solved C¬ -Var x el Csolved (+Var x :: C).

Lemma solved_neg_var x C :
  solved C¬ +Var x el Csolved (-Var x :: C).

Lemma cent_solved_sat C D :
  cent C Dsolved Csat D.

Refutation predicates

Record ref_pred (rho : clauseProp) :=
  { ref_Fal : C, +Fal el Crho C;
    ref_weak : C C', C <<= C'rho Crho C';
    ref_clash : x C, +Var x el C-Var x el Crho 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 Cndc (map uns C) Fal).

Decision trees

Inductive rec C : clauseType :=
| recNil : rec C nil
| recPF D : rec C (+Fal :: D)
| recNF D : rec C Drec C (-Fal ::D)
| recPV D x : -Var x el Crec C (+Var x :: D)
| recPV' D x : ¬ -Var x el Crec (+Var x :: C) Drec C (+Var x :: D)
| recNV D x : +Var x el Crec C (-Var x :: D)
| recNV' D x : ¬ +Var x el Crec (-Var x :: C) Drec 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

Fixpoint size C : nat :=
  match C with
    | nil ⇒ 0
    | +s::C'sizeF s + size C'
    | -s::C'sizeF s + size C'

Definition provider C D : rec C D.

Refutation lemma

Section RL.
  Variable rho : clauseProp.
  Variable Rho : ref_pred rho.

  Definition decider C D :
    rec C Dsolved 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.

Decidability of classical ND entailment

Lemma satis_pos f A :
  satis' f (map Pos A) s, s el Asatis f s.

Lemma uns_pos A :
  map uns (map Pos A) = A.

Lemma ndc_dec A s :
  dec (ndc A s).

Agreement of classical ND entailment with boolean entailment

Lemma bent_iff_unsat A s :
  bent A s ¬ sat (-s :: map Pos A).

Lemma ndc_iff_sem A s :
  ndc A s bent A s.