Library CNF

Require Export Basic.
Require Export Even.
Require Export Bool.

Definition Valuation := positive -> bool.

Section Literal.

Inductive Literal : Type :=
  | pos : positive -> Literal
  | neg : positive -> Literal.

Definition negate (l:Literal) : Literal :=
  match l with
  | pos n => neg n
  | neg n => pos n
  end.

Lemma literal_eq_dec : forall l l':Literal, {l = l'} + {l <> l'}.

Fixpoint L_satisfies (v:Valuation) (l:Literal) : Prop :=
  match l with
  | pos x => if (v x) then True else False
  | neg x => if (v x) then False else True
  end.

Lemma L_satisfies_neg : forall v l, L_satisfies v l <-> ~ L_satisfies v (negate l).

Lemma L_satisfies_neg_neg : forall v l, L_satisfies v l <-> L_satisfies v (negate (negate l)).

Lemma L_satisfies_dec : forall v l, {L_satisfies v l}+{~(L_satisfies v l)}.

Section Compare.

Definition Literal_compare (l l':Literal) : comparison :=
  match l, l' with
  | pos n, pos n' => Pos.compare n n'
  | neg n, neg n' => Pos.compare n n'
  | neg n, pos n' => Lt
  | pos n, neg n' => Gt
  end.

Lemma eq_Lit_compare : forall l l', Literal_compare l l' = Eq -> l = l'.

Lemma Lit_compare_eq : forall l, Literal_compare l l = Eq.

Lemma Lit_compare_trans : forall l l' l'', Literal_compare l l' = Lt -> Literal_compare l' l'' = Lt ->
                                           Literal_compare l l'' = Lt.

Lemma Lit_compare_sym_Gt : forall l l', Literal_compare l l' = Gt -> Literal_compare l' l = Lt.

Lemma Lit_compare_sym_Lt : forall l l', Literal_compare l l' = Lt -> Literal_compare l' l = Gt.

End Compare.

End Literal.

Section Clauses.

Definition Clause := list Literal.

Fixpoint C_satisfies (v:Valuation) (c:Clause) : Prop :=
  match c with
  | nil => False
  | l :: c' => (L_satisfies v l) \/ (C_satisfies v c')
  end.

Lemma C_satisfies_exists : forall v c, C_satisfies v c ->
  exists l, In l c /\ L_satisfies v l.

Lemma exists_C_satisfies : forall v c l, In l c -> L_satisfies v l ->
  C_satisfies v c.

Lemma C_satisfies_dec : forall v c, {C_satisfies v c}+{~C_satisfies v c}.


Definition C_unsat (c:Clause) : Prop := forall v:Valuation, ~(C_satisfies v c).

Lemma C_unsat_empty : C_unsat nil.

Definition true_C : Clause := (pos 1::neg 1::nil).

Lemma true_C_true : forall v:Valuation, C_satisfies v true_C.

Lemma C_sat_clause : forall c:Clause, c <> nil -> ~(C_unsat c).

Lemma clause_eq_dec : forall c c':Clause, {c = c'} + {c <> c'}.

Lemma clause_eq_nil_cons : forall c: Clause, {c = nil} + {exists l c', c = l :: c'} .

Section Compare.

Fixpoint Clause_compare (cl cl':Clause) : comparison :=
  match cl, cl' with
  | nil, nil => Eq
  | nil, _::_ => Lt
  | _::_, nil => Gt
  | l::c, l'::c' => match (Literal_compare l l') with
                    | Lt => Lt
                    | Gt => Gt
                    | Eq => Clause_compare c c'
  end end.

Lemma eq_Clause_compare : forall cl cl', Clause_compare cl cl' = Eq -> cl = cl'.

Lemma Clause_compare_eq : forall cl, Clause_compare cl cl = Eq.

Lemma Clause_compare_trans : forall cl cl' cl'', Clause_compare cl cl' = Lt -> Clause_compare cl' cl'' = Lt ->
                                           Clause_compare cl cl'' = Lt.

Lemma Clause_compare_sym_Gt : forall cl cl', Clause_compare cl cl' = Gt -> Clause_compare cl' cl = Lt.

Lemma Clause_compare_sym_Lt : forall cl cl', Clause_compare cl cl' = Lt -> Clause_compare cl' cl = Gt.

End Compare.

End Clauses.

Section CNF.

Definition CNF := list Clause.

Lemma CNF_eq_dec : forall c c':CNF, {c = c'} + {c <> c'}.

Fixpoint satisfies (v:Valuation) (c:CNF) : Prop :=
  match c with
  | nil => True
  | cl :: c' => (C_satisfies v cl) /\ (satisfies v c')
  end.

Lemma satisfies_for_all : forall v c, satisfies v c ->
  forall cl, In cl c -> C_satisfies v cl.

Lemma for_all_satisfies : forall v c, (forall cl, In cl c -> C_satisfies v cl) ->
  satisfies v c.

Lemma satisfies_remove : forall c:CNF, forall c':Clause, forall v,
  satisfies v c -> satisfies v (remove clause_eq_dec c' c).

Definition entails (c:CNF) (c':Clause) : Prop :=
  forall v:Valuation, satisfies v c -> C_satisfies v c'.

Definition unsat (c:CNF) : Prop := forall v:Valuation, ~(satisfies v c).

Lemma unsat_remove : forall c:CNF, forall c':Clause,
  unsat (remove clause_eq_dec c' c) -> unsat c.

Lemma unsat_subset : forall (c c':CNF),
  (forall cl, In cl c -> In cl c') -> unsat c -> unsat c'.

Lemma CNF_empty : forall c, entails c nil -> unsat c.


Definition CNF_equiv (c c':CNF) :=
  forall (cl:Clause), In cl c <-> In cl c'.

End CNF.