Library SetChecker

Require Export Basic.
Require Export Even.
Require Export Bool.
Require Export Recdef.
Require Import Allmaps.
Require Export BinaryTrees.
Require Export BinPos.
Require Export CNF.

Section SetClauses.

Definition SetClause := BinaryTree Literal.

Definition SC_add := BT_add Literal_compare.
Definition SC_in := BT_In (T := Literal).
Definition SC_diff := BT_diff Literal_compare.
Definition SC_wf := BT_wf Literal_compare.

Fixpoint Clause_to_SetClause (cl:Clause) : SetClause :=
  match cl with
  | nil => nought
  | l :: cl' => SC_add l (Clause_to_SetClause cl')
  end.

Lemma C_to_SC_wf : forall (cl:Clause), SC_wf (Clause_to_SetClause cl).

Fixpoint SetClause_to_Clause (cl:SetClause) : Clause :=
  match cl with
  | nought => nil
  | node l cl' cl'' => l :: (SetClause_to_Clause cl') ++ (SetClause_to_Clause cl'')
  end.

Lemma list_append_split : forall A, forall P : A -> Prop,
  forall (l1 l2 w1 w2 : list A),
  (forall x, In x l1 -> P x) /\ (forall x, In x w1 -> P x) /\
  (forall x, In x l2 -> ~P x) /\ (forall x, In x w2 -> ~P x)
  -> (l1 ++ l2) = (w1 ++ w2) -> l1 = w1 /\ l2 = w2.

Coercion SetClause_to_Clause : SetClause >-> Clause.

Lemma C_to_SC_In_1 : forall l c, In l c -> SC_in l (Clause_to_SetClause c).

Lemma SC_to_C_In_1 : forall l c, In l (SetClause_to_Clause c) -> SC_in l c.

Lemma C_to_SC_In_2 : forall l c, SC_in l (Clause_to_SetClause c) -> In l c.

Lemma SC_to_C_In_2 : forall l c, SC_in l c -> In l (SetClause_to_Clause c).

Lemma SetClause_to_Clause_inv : forall cl cl', SC_wf cl -> SC_wf cl' ->
  SetClause_to_Clause cl = SetClause_to_Clause cl' -> cl = cl'.

Lemma SC_satisfies_exists : forall (v:Valuation) (c:SetClause), C_satisfies v c ->
  exists l, SC_in l c /\ L_satisfies v l.

Lemma exists_SC_satisfies : forall (v:Valuation) (c:SetClause) l,
  SC_in l c -> L_satisfies v l -> C_satisfies v c.

Lemma C_to_C_satisfies_1 : forall (v:Valuation) (c:Clause),
  C_satisfies v c -> C_satisfies v (SetClause_to_Clause (Clause_to_SetClause c)).

Lemma C_to_C_satisfies_2 : forall (v:Valuation) (c:Clause),
  C_satisfies v (SetClause_to_Clause (Clause_to_SetClause c)) -> C_satisfies v c.

Definition true_SC : SetClause := (node (pos 1) (node (neg 1) nought nought) nought).

Lemma SetClause_eq_dec : forall c c':SetClause, {c = c'} + {c <> c'}.

Lemma SetClause_eq_nil_cons : forall c: SetClause, {l:Literal & {c':SetClause & {c'':SetClause | c = node l c' c''}}} + {c = nought}.

End SetClauses.

Section TreeCNF.

Definition TreeCNF := BinaryTree Clause.

Definition TCNF_in := BT_In (T := Clause).
Definition TCNF_remove := BT_remove Clause_compare : Clause -> TreeCNF -> TreeCNF.
Definition TCNF_wf := BT_wf Clause_compare.
Definition TCNF_join := BT_add_all _ Clause_compare : TreeCNF -> TreeCNF -> TreeCNF.
Definition TCNF_add := BT_add Clause_compare : Clause -> TreeCNF -> TreeCNF.

Lemma TCNF_eq_dec : forall c c':TreeCNF, {c = c'} + {c <> c'}.

Fixpoint T_satisfies (v:Valuation) (c:TreeCNF) : Prop :=
  match c with
  | nought => True
  | node cl c' c'' => (C_satisfies v cl) /\ (T_satisfies v c') /\ (T_satisfies v c'')
  end.

Fixpoint make_TCNF (c:CNF) : TreeCNF :=
  match c with
  | nil => nought
  | cl :: c' => TCNF_add cl (make_TCNF c')
  end.

Lemma make_TCNF_wf : forall c, TCNF_wf (make_TCNF c).

Lemma satisfies_to_T_satisfies : forall v c,
  satisfies v c -> T_satisfies v (make_TCNF c).

Lemma T_satisfies_to_satisfies : forall v c,
  T_satisfies v (make_TCNF c) -> satisfies v c.

Fixpoint TCNF_to_CNF (c:TreeCNF) : CNF :=
  match c with
  | nought => nil
  | node cl c1 c2 => TCNF_to_CNF c1 ++ (cl :: TCNF_to_CNF c2)
  end.

Lemma satisfies_to_T_satisfies' : forall v c,
  satisfies v (TCNF_to_CNF c) -> T_satisfies v c.

Lemma T_satisfies_to_satisfies' : forall v c,
  T_satisfies v c -> satisfies v (TCNF_to_CNF c).

Lemma In_TCNF' : forall cl (c:CNF), In cl c -> TCNF_in cl (make_TCNF c).

Lemma TCNF_In' : forall cl (c:CNF), TCNF_in cl (make_TCNF c) -> In cl c.

Lemma TCNF_In : forall cl c, TCNF_in cl c -> In cl (TCNF_to_CNF c).

Lemma In_TCNF : forall cl c, In cl (TCNF_to_CNF c) -> TCNF_in cl c.

Coercion TCNF_to_CNF : TreeCNF >-> CNF.

End TreeCNF.

Section ICNF.

Definition ICNF := Map {cl:SetClause | SC_wf cl}.

Definition empty_ICNF : ICNF := M0 _.

Fixpoint ICNF_to_TCNF (c:ICNF) : TreeCNF :=
  match c with
  | M0 _ => nought
  | M1 _ _ cl => let (c,_) := cl in node (SetClause_to_Clause c) nought nought
  | M2 _ c' c'' => BT_add_all _ Clause_compare (ICNF_to_TCNF c') (ICNF_to_TCNF c'')
  end.

Coercion ICNF_to_TCNF : ICNF >-> TreeCNF.

Lemma ICNF_to_TCNF_wf : forall (c:ICNF), TCNF_wf (c:TreeCNF).

Lemma ICNF_get_in : forall c (cl:SetClause) i Hc,
  MapGet _ c i = Some (exist SC_wf cl Hc) -> TCNF_in cl (ICNF_to_TCNF c).

Lemma in_ICNF_get : forall c (cl:SetClause), SC_wf cl ->
  TCNF_in cl (ICNF_to_TCNF c) -> exists i Hc, MapGet _ c i = Some (exist SC_wf cl Hc).

Lemma in_ICNF_get' : forall c (cl:Clause), TCNF_in cl (ICNF_to_TCNF c) ->
  exists i sc Hsc, MapGet _ c i = Some (exist SC_wf sc Hsc) /\ cl = SetClause_to_Clause sc.

Definition get_ICNF (c:ICNF) i : SetClause :=
  match (MapGet _ c i) with
  | None => true_SC
  | Some cl => let (c,_) := cl in c
  end.

Lemma get_ICNF_in_or_default : forall c i,
  {TCNF_in (get_ICNF c i) (ICNF_to_TCNF c)} + {get_ICNF c i = true_SC}.

Definition del_ICNF i (c:ICNF) : ICNF :=
  MapRemove _ c i.

Lemma ICNF_get_del : forall T c (cl:T) i j,
  MapGet _ (MapRemove _ c j) i = Some cl -> MapGet _ c i = Some cl.

Lemma MapRemove_in : forall c (cl:Clause) j,
  TCNF_in cl (ICNF_to_TCNF (MapRemove _ c j)) -> TCNF_in cl (ICNF_to_TCNF c).

Lemma del_ICNF_in : forall (i:ad) (c:ICNF) (cl:Clause),
  TCNF_in cl ((del_ICNF i c):TreeCNF) -> TCNF_in cl (c:TreeCNF).

Definition add_ICNF i (cl:SetClause) Hcl (c:ICNF) :=
  MapPut _ c i (exist _ cl Hcl).

Lemma MapPut1_in : forall p i j (ci cj:SetClause) (cl:Clause) Hci Hcj,
  TCNF_in cl (ICNF_to_TCNF (MapPut1 _ i (exist _ ci Hci) j (exist _ cj Hcj) p)) -> cl = ci \/ cl = cj.

Lemma MapPut_in : forall c (cl:Clause) (cl':SetClause) Hcl' j,
  TCNF_in cl (ICNF_to_TCNF (MapPut _ c j (exist _ cl' Hcl'))) -> cl = cl' \/ TCNF_in cl (ICNF_to_TCNF c).

Lemma add_ICNF_unsat : forall i (cl:SetClause) Hcl, forall c:ICNF,
  unsat ((add_ICNF i cl Hcl c):ICNF) -> entails c cl -> unsat c.

End ICNF.

Section Propagation.

Lemma SC_in_add : forall (l l':Literal) (cl:SetClause),
  In l (SetClause_to_Clause (SC_add l' cl)) -> l = l' \/ In l (SetClause_to_Clause cl).

Lemma propagate_singleton : forall (cs:TreeCNF) (c c':SetClause), forall l,
  SC_diff c c' = (node l nought nought) ->
  entails cs (SetClause_to_Clause (SC_add (negate l) c')) -> entails (TCNF_add c cs) c'.

Lemma propagate_empty : forall (cs:TreeCNF) (c c':SetClause),
  SC_diff c c' = nought -> entails (TCNF_add c cs) c'.

Lemma propagate_entails : forall (cs:TreeCNF) (c c':SetClause), TCNF_in c cs ->
  entails (TCNF_add c cs) c' -> entails cs c'.

Lemma propagate_true : forall (cs:TreeCNF) (c:SetClause),
  entails (TCNF_add true_SC cs) c -> entails cs c.

Fixpoint propagate (cs: ICNF) (c: SetClause) (is:list ad) : bool :=
  match is with
  | nil => false
  | (i::is) => match SetClause_eq_nil_cons (SC_diff (get_ICNF cs i) c) with
    | inright _ => true
    | inleft H => let (l,Hl) := H in let (c',Hc) := Hl in
                  match SetClause_eq_nil_cons c' with
                  | inleft _ => false
                  | inright _ => let (c'',_) := Hc in
                                 match SetClause_eq_nil_cons c'' with
                                 | inleft _ => false
                                 | inright _ => propagate cs (SC_add (negate l) c) is
  end end end end.

Lemma propagate_sound : forall is cs c, propagate cs c is = true -> entails cs c.

End Propagation.

Section Refutation.

Inductive Action : Type :=
  | D : list ad -> Action
  | O : ad -> Clause -> Action
  | R : ad -> Clause -> list ad -> Action.

Definition LazyT := id (A:=Type).

Inductive lazy_list (A:Type) :=
    lnil : lazy_list A
  | lcons : A -> LazyT (lazy_list A) -> lazy_list A.

Definition Oracle := LazyT (lazy_list Action).


Fixpoint Oracle_size (O:Oracle) : nat :=
  match O with
  | lnil _ => 0
  | lcons (D is) O' => length is + 1 + Oracle_size O'
  | lcons _ O' => 1 + Oracle_size O'
  end.

Definition Answer := bool.

Definition force := id (A := Oracle).
Definition fromVal := id (A := Oracle).

Function refute_work (w:ICNF) (c:TreeCNF) (Hc:TCNF_wf c) (O:Oracle)
  {measure Oracle_size O} : Answer :=
  match (force O) with
  | lnil _ => false
  | lcons (D nil) O' => refute_work w c Hc O'
  | lcons (D (i::is)) O' => refute_work (del_ICNF i w) c Hc (fromVal (lcons (D is) O'))
  | lcons (O i cl) O' => if (BT_in_dec _ _ eq_Clause_compare Clause_compare_eq cl c Hc) then (refute_work (add_ICNF i _ (C_to_SC_wf cl) w) c Hc O') else false
  | lcons (R i nil is) O' => propagate w nought is
  | lcons (R i cl is) O' => andb (propagate w (Clause_to_SetClause cl) is) (refute_work (add_ICNF i _ (C_to_SC_wf cl) w) c Hc O')
  end.
Defined.

Lemma refute_work_correct : forall w c Hc O, refute_work w c Hc O = true -> unsat (TCNF_join c (w:TreeCNF)).

Definition refute (c:CNF) (O:Oracle) : Answer :=
  refute_work empty_ICNF (make_TCNF c) (make_TCNF_wf c) O.

Theorem refute_correct : forall c O, refute c O = true -> unsat c.

End Refutation.