path: root/src/hls/Sat.v

(**
#<a href="http://www.cs.berkeley.edu/~adamc/itp/">#Interactive Computer Theorem
Proving#</a><br>#
CS294-9, Fall 2006#<br>#
UC Berkeley *)

Require Import Arith Bool List.
Require Import Coq.funind.Recdef.
Require Coq.MSets.MSetPositive.
Require Coq.MSets.MSetProperties.
Require Import Coq.Structures.OrderedTypeEx.
Require Import Coq.Structures.OrdersAlt.
Require Import Coq.Program.Wf.
Require Import Vericertlib.

Module PSet := MSetPositive.PositiveSet.
Module PSetProp := MSetProperties.OrdProperties(PSet).

#[local] Open Scope positive.

(** * Problem Definition *)

Definition var := positive.
(** We identify propositional variables with natural numbers. *)

Definition lit := (bool * var)%type.
(** A literal is a combination of a truth value and a variable. *)

Definition clause := list lit.
(** A clause is a list (disjunction) of literals. *)

Definition formula := list clause.
(** A formula is a list (conjunction) of clauses. *)

Definition asgn := var -> bool.
(** An assignment is a function from variables to their truth values. *)

Definition satLit (l : lit) (a : asgn) :=
  a (snd l) = fst l.
(** An assignment satisfies a literal if it maps it to true. *)

Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop :=
  match cl with
  | nil => False
  | l :: cl' => satLit l a \/ satClause cl' a
  end.
(** An assignment satisfies a clause if it satisfies at least one of its
  literals.
 *)

Fixpoint satFormula (fm: formula) (a: asgn) {struct fm} : Prop :=
  match fm with
  | nil => True
  | cl :: fm' => satClause cl a /\ satFormula fm' a
  end.
(** An assignment satisfies a formula if it satisfies all of its clauses. *)

(** * Subroutines *)

(** You'll probably want to compare booleans for equality at some point. *)
Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
  decide equality.
Defined.

(** You'll probably want to compare booleans for equality at some point. *)
Definition boolpositive_eq_dec : forall (x y : (bool * positive)), {x = y} + {x <> y}.
  pose proof bool_eq_dec.
  pose proof peq.
  decide equality.
Defined.

(** A literal and its negation can't be true simultaneously. *)
Lemma contradictory_assignment : forall s l cl a,
    s <> fst l
    -> satLit l a
    -> satLit (s, snd l) a
    -> satClause cl a.
  intros.
  red in H0, H1.
  simpl in H1.
  subst.
  tauto.
Qed.

#[local] Hint Resolve contradictory_assignment : core.

(** Augment an assignment with a new mapping. *)
Definition upd (a : asgn) (l : lit) : asgn :=
  fun v : var =>
    if peq v (snd l)
    then fst l
    else a v.

(** Some lemmas about [upd] *)

Lemma satLit_upd_eq : forall l a,
    satLit l (upd a l).
  unfold satLit, upd; simpl; intros.
  destruct (peq (snd l) (snd l)); tauto.
Qed.

#[local] Hint Resolve satLit_upd_eq : core.

Lemma satLit_upd_neq : forall v l s a,
    v <> snd l
    -> satLit (s, v) (upd a l)
    -> satLit (s, v) a.
  unfold satLit, upd; simpl; intros.
  destruct (peq v (snd l)); tauto.
Qed.

#[local] Hint Resolve satLit_upd_neq : core.

Lemma satLit_upd_neq2 : forall v l s a,
    v <> snd l
    -> satLit (s, v) a
    -> satLit (s, v) (upd a l).
  unfold satLit, upd; simpl; intros.
  destruct (peq v (snd l)); tauto.
Qed.

#[local] Hint Resolve satLit_upd_neq2 : core.

Lemma satLit_contra : forall s l a cl,
    s <> fst l
    -> satLit (s, snd l) (upd a l)
    -> satClause cl a.
  unfold satLit, upd; simpl; intros.
  destruct (peq (snd l) (snd l)); intuition.
Qed.

#[local] Hint Resolve satLit_contra : core.

Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder;
                     match goal with
                     | [ H1 : satLit ?l ?a, H2 : satClause ?cl ?a |- _ ] =>
                       assert (satClause cl (upd a l)); firstorder
                     end.

(** Strongly-specified function to update a clause to reflect the effect of making a particular
  literal true.  *)
Definition setClause : forall (cl : clause) (l : lit),
    {cl' : clause |
      forall a, satClause cl (upd a l) <-> satClause cl' a}
    + {forall a, satLit l a -> satClause cl a}.
  refine (fix setClause (cl: clause) (l: lit) {struct cl} :=
            match cl with
            | nil => inleft (exist _ nil _)
            | x :: xs =>
              match setClause xs l with
              | inright p => inright _
              | inleft (exist _ cl' H) =>
                match peq (snd x) (snd l), bool_eq_dec (fst x) (fst l) with
                | left p_eq, left bool_eq => inright _
                | left eq, right ne => inleft (exist _ cl' _)
                | right neq, _ => inleft (exist _ (x :: cl') _)
                end
              end
            end); clear setClause; try magic_solver.
  - intros; simpl; left; apply injective_projections in bool_eq; subst; auto.
  - split; intros. simpl in H0. inversion H0. eapply satLit_contra; eauto.
    destruct x; simpl in *; subst. auto.
    apply H. eauto.
    simpl. right. apply H; eauto.
  - split; intros; simpl in *. inversion H0. destruct x; simpl in *; subst.
    left. eauto.
    right. apply H. eauto.
    inversion H0. left. apply satLit_upd_neq2. auto. auto.
    right. apply H. auto.
Defined.

(** For testing purposes, we define a weakly-specified function as a thin
  wrapper around [setClause].
 *)
Definition setClauseSimple (cl : clause) (l : lit) :=
  match setClause cl l with
  | inleft (exist _ cl' _) => Some cl'
  | inright _ => None
  end.

(*Eval compute in setClauseSimple ((false, 1%nat) :: nil) (true, 1%nat).*)
(*Eval compute in setClauseSimple nil (true, 0).
Eval compute in setClauseSimple ((true, 0) :: nil) (true, 0).
Eval compute in setClauseSimple ((true, 0) :: nil) (false, 0).
Eval compute in setClauseSimple ((true, 0) :: nil) (true, 1).
Eval compute in setClauseSimple ((true, 0) :: nil) (false, 1).
Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (true, 1).
Eval compute in setClauseSimple ((true, 0) :: (true, 1) :: nil) (false, 1).
Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (true, 1).
Eval compute in setClauseSimple ((true, 0) :: (false, 1) :: nil) (false, 1).*)

(** It's useful to have this strongly-specified nilness check. *)
Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {ls <> nil}.
  destruct ls; [left|right]; [auto|]; unfold not; intros; inversion H.
Defined.
Arguments isNil [A].

(** Some more lemmas that I found helpful.... *)

Lemma satLit_idem_lit : forall l a l',
    satLit l a
    -> satLit l' a
    -> satLit l' (upd a l).
  unfold satLit, upd; simpl; intros.
  destruct (peq (snd l') (snd l)); congruence.
Qed.

#[local] Hint Resolve satLit_idem_lit : core.

Lemma satLit_idem_clause : forall l a cl,
    satLit l a
    -> satClause cl a
    -> satClause cl (upd a l).
  induction cl; simpl; intuition.
Qed.

#[local] Hint Resolve satLit_idem_clause : core.

Lemma satLit_idem_formula : forall l a fm,
    satLit l a
    -> satFormula fm a
    -> satFormula fm (upd a l).
  induction fm; simpl; intuition.
Qed.

#[local] Hint Resolve satLit_idem_formula : core.

(** Function that updates an entire formula to reflect setting a literal to true.  *)
Definition setFormula : forall (fm : formula) (l : lit),
    {fm' : formula |
      forall a, satFormula fm (upd a l) <-> satFormula fm' a}
    + {forall a, satLit l a -> ~satFormula fm a}.
  refine (fix setFormula (fm: formula) (l: lit) {struct fm} :=
            match fm with
            | nil => inleft (exist _ nil _)
            | cl' :: fm' =>
              match setFormula fm' l with
              | inright p => inright _
              | inleft (exist _ fm'' H) =>
                match setClause cl' l with
                | inright H' => inleft (exist _ fm'' _)
                | inleft (exist _ cl'' _) =>
                  if isNil cl''
                  then inright _
                  else inleft (exist _ (cl'' :: fm'') _)
                end
              end
            end); clear setFormula; magic_solver.
Defined.

Definition setFormulaSimple (fm : formula) (l : lit) :=
  match setFormula fm l with
  | inleft (exist _ fm' _) => Some fm'
  | inright _ => None
  end.

(* Eval compute in setFormulaSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil) (true, 1%nat). *)
(* Eval compute in setFormulaSimple nil (true, 0). *)
(* Eval compute in setFormulaSimple (((true, 0) :: nil) :: nil) (true, 0). *)
(* Eval compute in setFormulaSimple (((false, 0) :: nil) :: nil) (true, 0). *)
(* Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0). *)
(* Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). *)
(* Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0). *)

#[local] Hint Extern 1 False => discriminate : core.

Local Hint Extern 1 False =>
match goal with
| [ H : In _ (_ :: _) |- _ ] => inversion H; clear H; subst
end : core.

(** Code that either finds a unit clause in a formula or declares that there are none.  *)
Definition findUnitClause : forall (fm: formula),
    {l : lit | In (l :: nil) fm}
    + {forall l, ~In (l :: nil) fm}.
  refine (fix findUnitClause (fm: formula) {struct fm} :=
            match fm with
            | nil => inright _
            | (l :: nil) :: fm' => inleft (exist _ l _)
            | _ :: fm' =>
              match findUnitClause fm' with
              | inleft (exist _ l _) => inleft (exist _ l _)
              | inright H => inright _
              end
            end
         ); clear findUnitClause; magic_solver.
Defined.

(** The literal in a unit clause must always be true in a satisfying assignment.  *)
Lemma unitClauseTrue : forall l a fm,
    In (l :: nil) fm
    -> satFormula fm a
    -> satLit l a.
  induction fm; intuition.
  inversion H.
  inversion H; subst; simpl in H0; intuition.
  apply IHfm; eauto. inv H0. eauto.
Qed.

#[local] Hint Resolve unitClauseTrue : core.

(** Unit propagation.  The return type of [unitPropagate] signifies that three results are possible:
  - [None]: There are no unit clauses.
  - [Some (inleft _)]: There is a unit clause, and here is a formula reflecting
    setting its literal to true.
  - [Some (inright _)]: There is a unit clause, and propagating it reveals that
    the formula is unsatisfiable.
 *)
Definition unitPropagate : forall (fm : formula), option (sigT (fun fm' : formula =>
                                                                  {l : lit |
                                                                    (forall a, satFormula fm a -> satLit l a)
                                                                    /\ forall a, satFormula fm (upd a l) <-> satFormula fm' a})
                                                          + {forall a, ~satFormula fm a}).
  refine (fix unitPropagate (fm: formula) {struct fm} :=
            match findUnitClause fm with
            | inright H => None
            | inleft (exist _ l _) =>
              match setFormula fm l with
              | inright _ => Some (inright _)
              | inleft (exist _ fm' _) =>
                Some (inleft (existT _ fm' (exist _ l _)))
              end
            end
         ); clear unitPropagate; magic_solver.
Defined.


Definition unitPropagateSimple (fm : formula) :=
  match unitPropagate fm with
  | None => None
  | Some (inleft (existT _ fm' (exist _ l _))) => Some (Some (fm', l))
  | Some (inright _) => Some None
  end.

(*Eval compute in unitPropagateSimple (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
Eval compute in unitPropagateSimple nil.
Eval compute in unitPropagateSimple (((true, 0) :: nil) :: nil).
Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil).
Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 1) :: nil) :: nil).
Eval compute in unitPropagateSimple (((true, 0) :: nil) :: ((false, 0) :: (false, 1) :: nil) :: nil).
Eval compute in unitPropagateSimple (((false, 0) :: (false, 1) :: nil) :: ((true, 0) :: nil) :: nil).*)


(** * The SAT Solver *)

(** This section defines a DPLL SAT solver in terms of the subroutines.  *)

(** An arbitrary heuristic to choose the next variable to split on *)
Definition chooseSplit (fm : formula) :=
  match fm with
  | ((l :: _) :: _) => l
  | _ => (true, 1)
  end.

Definition negate (l : lit) := (negb (fst l), snd l).

#[local] Hint Unfold satFormula : core.

Lemma satLit_dec : forall l a,
    {satLit l a} + {satLit (negate l) a}.
  destruct l.
  unfold satLit; simpl; intro.
  destruct b; destruct (a v); simpl; auto.
Qed.

(** We'll represent assignments as lists of literals instead of functions. *)
Definition alist := list lit.

Fixpoint interp_alist (al : alist) : asgn :=
  match al with
  | nil => fun _ => true
  | l :: al' => upd (interp_alist al') l
  end.

(** Here's the final definition!

  This implementation isn't #<i>#quite#</i># what you would expect, since it
  takes an extra parameter expressing a search tree depth.  Writing the function
  without that parameter would be trickier when it came to proving termination.
  In practice, you can just seed the bound with one plus the number of variables
  in the input, but the function's return type still indicates a possibility for
  a "time-out" by returning [None].
 *)
Definition boundedSat: forall (bound : nat) (fm : formula),
    option ({al : alist | satFormula fm (interp_alist al)}
            + {forall a, ~satFormula fm a}).
  refine (fix boundedSat (bound : nat) (fm : formula) {struct bound}
          : option ({al : alist | satFormula fm (interp_alist al)}
                    + {forall a, ~satFormula fm a}) :=
            match bound with
            | O => None
            | S bound' =>
              if isNil fm
              then Some (inleft _ (exist _ nil _))
              else match unitPropagate fm with
                   | Some (inleft (existT _ fm' (exist _ l _))) =>
                     match boundedSat bound' fm' with
                     | None => None
                     | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
                     | Some (inright _) => Some (inright _ _)
                     end
                   | Some (inright _) => Some (inright _ _)
                   | None =>
                     let l := chooseSplit fm in
                     match setFormula fm l with
                     | inleft (exist _ fm' _) =>
                       match boundedSat bound' fm' with
                       | None => None
                       | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
                       | Some (inright _) =>
                         match setFormula fm (negate l) with
                         | inleft (exist _ fm' _) =>
                           match boundedSat bound' fm' with
                           | None => None
                           | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                           | Some (inright _) => Some (inright _ _)
                           end
                         | inright _ => Some (inright _ _)
                         end
                       end
                     | inright _ =>
                       match setFormula fm (negate l) with
                       | inleft (exist _ fm' _) =>
                         match boundedSat bound' fm' with
                         | None => None
                         | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
                         | Some (inright _) => Some (inright _ _)
                         end
                       | inright _ => Some (inright _ _)
                       end
                     end
                   end
            end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  assert (satFormula fm (upd a0 l)); firstorder.
  assert (satFormula fm (upd a0 l)); firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a l)); firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a l)); firstorder.
  firstorder.
  firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a (negate l))); firstorder.
  destruct (satLit_dec l a); intuition eauto;
    assert (satFormula fm (upd a (negate l))); firstorder.
  destruct (satLit_dec l a);
    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
Defined.

Definition boundedSatSimple (bound : nat) (fm : formula) :=
  match boundedSat bound fm with
  | None => None
  | Some (inleft (exist _ a _)) => Some (Some a)
  | Some (inright _) => Some None
  end.

(*Eval compute in boundedSatSimple 100 nil.
Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: ((false, 0) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((true, 1) :: (false, 0) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((true, 0) :: (false, 1) :: nil) :: ((false, 0) :: (false, 0) :: nil) :: ((true, 1) :: nil) :: nil).
Eval compute in boundedSatSimple 100 (((false, 0) :: (true, 1) :: nil) :: ((false, 1) :: (true, 0) :: nil) :: nil).*)

Definition lit_set_cl (cl: clause) :=
  fold_right PSet.add PSet.empty (map snd cl).

Lemma lit_set_cl_in_set :
  forall cl v,
    In v (map snd cl) ->
    PSet.In v (lit_set_cl cl).
Proof.
  induction cl; crush.
  destruct a; cbn [snd] in *; inv H.
  - cbn. apply PSetProp.P.FM.add_1; auto.
  - cbn. apply PSetProp.P.FM.add_2.
    now apply IHcl.
Qed.

Lemma lit_set_cl_not_in_set :
  forall cl v,
    ~ In v (map snd cl) ->
    ~ PSet.In v (lit_set_cl cl).
Proof.
  induction cl; crush.
  destruct a; cbn [snd] in *.
  assert (p <> v /\ ~ In v (map snd cl))
    by (split; unfold not; intros; apply H; tauto).
  inv H0. cbn. unfold not; intros. 
  eapply IHcl; eauto.
  unfold lit_set_cl.
  eapply PSetProp.P.Dec.F.add_3; eassumption.
Qed.

Definition lit_set (fm: formula) :=
  fold_right PSet.union PSet.empty (map lit_set_cl fm).

(* Compute NSet.cardinal (lit_set (((true, 1)::(true, 1)::(true, 1)::nil)::nil)). *)

Definition sat_measure_cl (cl: clause) := PSet.cardinal (lit_set_cl cl).

Definition sat_measure (fm: formula) := PSet.cardinal (lit_set fm).

Lemma elim_clause :
  forall (cl: clause) l, In l cl -> exists H, setClause cl l = inright H.
Proof.
  induction cl; intros; simpl in *; try contradiction.
  destruct (setClause cl l) eqn:?; [|econstructor; eauto].
  destruct s. inversion H; subst. clear H.
  destruct (peq (snd l) (snd l)); [| contradiction].
  destruct (bool_eq_dec (fst l) (fst l)); [| contradiction].
  econstructor. eauto. apply IHcl in H0.
  inversion H0. rewrite H1 in Heqs. discriminate.
Qed.

Lemma sat_measure_setClause' :
  forall cl cl' l A,
    setClause cl l = inleft (exist _ cl' A) ->
    ~ In (snd l) (map snd cl').
Proof.
  induction cl; intros.
  { simpl in *. inv H. unfold not in *. intros. inv H. }
  simpl in H.
  repeat (destruct_match; crush; []). destruct_match.
  repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto.
  inv H. unfold not. intros. inv H. contradiction. eapply IHcl; eauto.
Qed.

Lemma sat_measure_setClause'' :
  forall cl cl' l A,
    setClause cl l = inleft (exist _ cl' A) ->
    forall l',
      l' <> snd l ->
      In l' (map snd cl) ->
      In l' (map snd cl').
Proof.
  induction cl; intros.
  { inversion H1. }
  { inversion H1. subst. simpl in H.
    repeat (destruct_match; crush; []). inv H. simpl.
    inv H1. eauto. right. eapply IHcl; eauto.
    simpl in H. repeat (destruct_match; crush; []). destruct_match.
    repeat (destruct_match; crush; []). inv H. eapply IHcl; eauto.
    inv H1; crush. inv H. simplify. auto.
    inv H. simpl. right. eapply IHcl; eauto.
  }
Qed.

Lemma sat_measure_setClause2'' :
  forall cl cl' l A,
    setClause cl l = inleft (exist _ cl' A) ->
    forall l',
      l' <> snd l ->
      In l' (map snd cl') ->
      In l' (map snd cl).
Proof.
  induction cl; intros.
  { cbn in *. inv H. cbn in *. auto. }
  exploit IHcl; eauto.
  Abort.

Lemma sat_measure_setClause :
  forall cl cl' l A,
    In (snd l) (map snd cl) ->
    setClause cl l = inleft (exist _ cl' A) ->
    (PSet.cardinal (lit_set_cl cl') < PSet.cardinal (lit_set_cl cl))%nat.
Proof.
  intros. pose proof H0. apply sat_measure_setClause' in H0.
  pose proof (sat_measure_setClause'' _ _ _ _ H1).
Abort.

Definition InFm l (fm: formula) := exists cl b, In cl fm /\ In (b, l) cl.

Lemma satFormulaHasEmpty :
  forall fm,
    In nil fm ->
    forall a, ~ satFormula fm a.
Proof.
  induction fm; crush.
  unfold not; intros. inv H0. inv H; auto.
  eapply IHfm; eauto.
Qed.

Lemma InFm_chooseSplit :
  forall l b c,
    InFm (snd (chooseSplit ((l :: b) :: c))) ((l :: b) :: c).
Proof.
  simpl; intros. destruct l; cbn.
  exists ((b0, v) :: b). exists b0.
  split; constructor; auto.
Qed.

Lemma InFm_negated_chooseSplit :
  forall l b c,
    InFm (snd (negate (chooseSplit ((l :: b) :: c)))) ((l :: b) :: c).
Proof.
  simpl; intros. destruct l; cbn.
  exists ((b0, v) :: b). exists b0.
  split; constructor; auto.
Qed.

Definition hasNoNil : forall fm: formula, {In nil fm} + {~ In nil fm}.
  refine (fix hasNoNil (fm: formula) {struct fm} :=
    match fm with
    | cl :: fm' =>
      match isNil cl with
      | left clIsNil => left _
      | right clIsNotNil =>
        match hasNoNil fm' with
        | left hasNilfm' => left _
        | right hasNoNilfm' => right _
        end
      end
    | nil => right _
    end
  ); auto.
  - subst. apply in_eq.
  - apply in_cons; assumption.
Defined.

Lemma sat_measure_setClause :
  forall cl cl' l b A,
    (forall b', ~ In (b', l) cl) ->
    setClause cl (b, l) = inleft (exist _ cl' A) ->
    lit_set_cl cl = lit_set_cl cl'.
Proof.
  induction cl; intros.
  - inv H0. auto.
  - cbn in H0. repeat (destruct_match; try discriminate; []).
    destruct_match.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *.
      exfalso.
      eapply H. econstructor. auto.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *.
      assert (forall b', ~ In (b', l) cl).
      { unfold not; intros. eapply H. apply in_cons. eassumption. }
      eapply IHcl in Heqs; [|assumption].
      unfold sat_measure_cl. cbn -[PSet.cardinal].
      unfold sat_measure_cl in Heqs.
      replace (fold_right PSet.add PSet.empty (map snd cl))
        with (lit_set_cl cl); auto.
      rewrite Heqs. auto.
Qed.

Lemma in_map_snd_forall :
  forall A B (cl: list (A * B)) l,
    ~ In l (map snd cl) ->
    (forall b', ~ In (b', l) cl).
Proof.
  unfold not; intros; apply H.
  replace l with (snd (b', l)) by auto.
  now apply in_map.
Qed.

Lemma sat_measure_setClause_In_neq :
  forall cl cl' l v b A,
    In v (map snd cl) ->
    setClause cl (b, l) = inleft (exist _ cl' A) ->
    v <> l ->
    In v (map snd cl').
Proof.
    induction cl; intros.
  - inv H0. auto.
  - cbn in H0. repeat (destruct_match; try discriminate; []).
    destruct_match.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *. eapply IHcl; eauto.
      inv H; auto. contradiction.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *.
      destruct (peq v v0); subst.
      { now constructor. }
      cbn. right. eapply IHcl; eauto. inv H; auto.
      contradiction.
Qed.

Lemma sat_measure_setClause_In :
  forall cl cl' l b A,
    In l (map snd cl) ->
    setClause cl (b, l) = inleft (exist _ cl' A) ->
    (sat_measure_cl cl' < sat_measure_cl cl)%nat.
Proof.
  induction cl; intros.
  - crush.
  - cbn in H0. repeat (destruct_match; try discriminate; []).
    destruct_match.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *. clear Heqs2. clear Heqs1.
      inv H; cbn [snd fst] in *.
      * destruct (in_dec peq v (map snd cl)).
        -- exploit IHcl; eauto; intros. unfold sat_measure_cl in *.
           cbn -[PSet.cardinal]. apply lit_set_cl_in_set in i0.
           rewrite PSetProp.P.add_cardinal_1; auto.
        -- apply sat_measure_setClause in Heqs; [|now apply in_map_snd_forall].
           unfold sat_measure_cl in *. cbn -[PSet.cardinal].
           setoid_rewrite Heqs.
           apply lit_set_cl_not_in_set in n0.
           rewrite PSetProp.P.add_cardinal_2; auto.
           now rewrite <- Heqs.
      * exploit IHcl; eauto; intros. unfold sat_measure_cl in *.
        cbn. rewrite PSetProp.P.add_cardinal_1; auto.
        now apply lit_set_cl_in_set.
    + repeat (destruct_match; try discriminate; []). inv H0.
      cbn [snd fst] in *. cbn in H. inv H; [contradiction|].
      exploit IHcl; eauto; intros.
      unfold sat_measure_cl in *. cbn.
      destruct (in_dec peq v (map snd cl)); destruct (in_dec peq v (map snd x)).
      * apply lit_set_cl_in_set in i0. apply lit_set_cl_in_set in i1.
        repeat rewrite PSetProp.P.add_cardinal_1 by auto. auto.
      * exploit sat_measure_setClause_In_neq. eapply i0. eauto. auto. intros.
        contradiction.
      * apply lit_set_cl_in_set in i0. apply lit_set_cl_not_in_set in n0.
        rewrite PSetProp.P.add_cardinal_1 by auto.
        rewrite PSetProp.P.add_cardinal_2 by auto. unfold lit_set_cl in *; lia.
      * apply lit_set_cl_not_in_set in n0. apply lit_set_cl_not_in_set in n1.
        repeat rewrite PSetProp.P.add_cardinal_2 by auto.
        unfold lit_set_cl in *; lia.
Qed.

(* Lemma sat_measure_setFormula :
  forall cl cl' l b b' A,
    In (b', l) cl ->
    setClause cl (b, l) = inleft (exist _ cl' A) ->
    (sat_measure_cl cl' < sat_measure_cl cl)%nat.
Proof.
  induction cl; intros.
  - crush.
  - cbn in H0. repeat (destruct_match; try discriminate; []).
    destruct_match.
    + repeat (destruct_match; try discriminate; []).
      inv H0. cbn [snd fst] in *.*)

Lemma sat_measure_setFormula :
  forall fm fm' l b A,
    InFm l fm ->
    setFormula fm (b, l) = inleft (exist _ fm' A) ->
    (sat_measure fm' < sat_measure fm)%nat.
Proof.
  induction fm.
  - intros. inv H. inv H1. inv H. inv H1.
  - intros. unfold sat_measure, lit_set. cbn -[PSet.cardinal].
    Admitted.

Lemma sat_measure_propagate_unit :
  forall fm' fm H,
    unitPropagate fm = Some (inleft (existT _ fm' H)) ->
    (sat_measure fm' < sat_measure fm)%nat.
Proof.
  induction fm; crush.
  repeat (destruct_match; crush; []).
  destruct_match.
  repeat (destruct_match; crush; []).
  inv Heqs1.
  unfold sat_measure.
  Admitted.

Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }:
  {al : alist | satFormula fm (interp_alist al)} + {forall a, ~satFormula fm a} :=
  match isNil fm with
  | left fmIsNil => inleft _ (exist _ nil _)
  | right fmIsNotNil =>
    match hasNoNil fm with
    | left hasNilfm => inright _ _
    | right hasNoNilfm =>
      match unitPropagate fm with
      | Some (inleft (existT _ fm' (exist _ l _))) =>
        match satSolve fm' with
        | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
        | inright _ => inright _ _
        end
      | Some (inright _) => inright _ _
      | None =>
        let l := chooseSplit fm in
        match setFormula fm l with
        | inleft (exist _ fm' _) =>
          match satSolve fm' with
          | inleft (exist _ al _) => inleft _ (exist _ (l :: al) _)
          | inright _ =>
            match setFormula fm (negate l) with
            | inleft (exist _ fm' _) =>
              match satSolve fm' with
              | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
              | inright _ => inright _ _
              end
            | inright _ => inright _ _
            end
          end
        | inright _ =>
          match setFormula fm (negate l) with
          | inleft (exist _ fm' _) =>
            match satSolve fm' with
            | inleft (exist _ al _) => inleft _ (exist _ (negate l :: al) _)
            | inright _ => inright _ _
            end
          | inright _ => inright _ _
          end
        end
      end
    end
  end.
Next Obligation.
  apply satFormulaHasEmpty; assumption. Defined.
Next Obligation.
  eapply sat_measure_propagate_unit; eauto. Defined.
Next Obligation.
  apply i; auto. Defined.
Next Obligation.
  unfold not; intros; eapply wildcard'; apply i; eauto. Defined.
Next Obligation.
  intros. symmetry in Heq_anonymous.
  destruct (chooseSplit fm) eqn:?.
  apply sat_measure_setFormula in Heq_anonymous; auto. unfold isNil in *.
  destruct fm; try discriminate.
  assert (c <> nil).
  { unfold not; intros. apply hasNoNilfm. constructor; auto. }
  destruct c; try discriminate.
  replace p with (snd (b, p)) by auto. rewrite <- Heqp.
  apply InFm_chooseSplit. Defined.
Next Obligation.
  apply wildcard'0; auto. Defined.
Next Obligation.
  eapply sat_measure_setFormula; eauto.
  destruct fm; try discriminate. destruct c; try discriminate.
  apply InFm_chooseSplit. Defined.
Next Obligation.
  apply wildcard'2; auto. Defined.
Next Obligation.
  unfold not in *; intros.
  destruct (satLit_dec (chooseSplit fm) a);
  [assert (satFormula fm (upd a (chooseSplit fm)))
  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
  { eapply wildcard'1. apply wildcard'0; eauto. }
  { eapply wildcard'. apply wildcard'2; eauto. }
Defined.
Next Obligation.
  unfold not in *; intros.
  destruct (satLit_dec (chooseSplit fm) a);
  [assert (satFormula fm (upd a (chooseSplit fm)))
  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
  { eapply wildcard'1. eapply wildcard'0. eauto. }
  { eapply wildcard'; eauto. }
Defined.
Next Obligation.
  eapply sat_measure_setFormula; eauto.
  destruct fm; try discriminate. destruct c; try discriminate.
  apply InFm_chooseSplit. Defined.
Next Obligation.
  apply wildcard'1; auto. Defined.
Next Obligation.
  unfold not in *; intros.
  destruct (satLit_dec (chooseSplit fm) a);
  [assert (satFormula fm (upd a (chooseSplit fm)))
  | assert (satFormula fm (upd a (negate (chooseSplit fm))))]; firstorder.
  { eapply wildcard'0; eauto. }
  { eapply wildcard'; apply wildcard'1; eauto. }
Defined.
Next Obligation.
  unfold not in *; intros.
  destruct (satLit_dec (chooseSplit fm) a).
  { eapply wildcard'0; eauto. }
  { eapply wildcard'; eauto. }
Defined.

Definition satSolveSimple (fm : formula) :=
  match satSolve fm with
  | inleft (exist _ a _) => Some a
  | inright _ => None
  end.

(* Eval compute in satSolveSimple nil. *)