Library CubeAndConquer

Require Export CNF.

Definition Cube := list Literal.

Fixpoint Cubed_CNF (F:CNF) (C:Cube) : CNF :=
  match C with
  | nil => F
  | l :: c => (l :: nil) :: (Cubed_CNF F c)
  end.

Lemma Cubed_CNF_satisfies : forall V F C,
  satisfies V (Cubed_CNF F C) -> satisfies V F.

Lemma satisfies_Cubed_CNF : forall V (F:CNF) (C:Cube),
  satisfies V F -> (forall c, In c C -> L_satisfies V c) ->
  satisfies V (Cubed_CNF F C).

Definition neg_cube (C:Cube) : Clause := map negate C.

Fixpoint noCube (C:list Cube) : CNF :=
  match C with
  | nil => nil
  | (c :: C') => (neg_cube c) :: (noCube C')
  end.

Lemma Literal_neg_neg : forall l, negate (negate l) = l.

Lemma CubeAndConquer_lemma : forall Formula Cubes,
  (forall c, In c Cubes -> unsat (Cubed_CNF Formula c)) ->
  unsat (noCube Cubes) -> unsat Formula.