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.

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.

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.

Lemma satis_pos f A :
  satis' f (map Pos A) ↔ ∀ s, s el A → satis f s.

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

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

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.