(** Homework Assignment 6#
#
##Interactive Computer Theorem
Proving#
#
CS294-9, Fall 2006#
#
UC Berkeley *)
Require Import Arith Bool List.
Definition var := nat.
Definition lit := (bool * var)%type.
Definition clause := list lit.
Definition formula := list clause.
Definition asgn := var -> bool.
Definition satLit (l : lit) (a : asgn) :=
a (snd l) = fst l.
Fixpoint satClause (cl : clause) (a : asgn) {struct cl} : Prop :=
match cl with
| nil => False
| l :: cl' => satLit l a \/ satClause cl' a
end.
Fixpoint satFormula (fm : formula) (a : asgn) {struct fm} : Prop :=
match fm with
| nil => True
| cl :: fm' => satClause cl a /\ satFormula fm' a
end.
Definition bool_eq_dec : forall (x y : bool), {x = y} + {x <> y}.
decide equality.
Defined.
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.
Hint Resolve contradictory_assignment.
Definition upd (a : asgn) (l : lit) : asgn :=
fun v : var =>
if eq_nat_dec v (snd l)
then fst l
else a v.
Lemma satLit_upd_eq : forall l a,
satLit l (upd a l).
unfold satLit, upd; simpl; intros.
destruct (eq_nat_dec (snd l) (snd l)); tauto.
Qed.
Hint Resolve satLit_upd_eq.
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 (eq_nat_dec v (snd l)); tauto.
Qed.
Hint Resolve satLit_upd_neq.
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 (eq_nat_dec v (snd l)); tauto.
Qed.
Hint Resolve satLit_upd_neq2.
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 (eq_nat_dec (snd l) (snd l)); intuition.
assert False; intuition.
Qed.
Hint Resolve satLit_contra.
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.
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}
: {cl' : clause |
forall a, satClause cl (upd a l) <-> satClause cl' a}
+ {forall a, satLit l a -> satClause cl a} :=
match cl return {cl' : clause |
forall a, satClause cl (upd a l) <-> satClause cl' a}
+ {forall a, satLit l a -> satClause cl a} with
| nil => inleft _ (exist _ nil _)
| (s, v) :: cl' =>
if eq_nat_dec v (snd l)
then if bool_eq_dec s (fst l)
then inright _ _
else match setClause cl' l with
| inleft (exist cl'' _) => inleft _ (exist _ cl'' _)
| inright _ => inright _ _
end
else match setClause cl' l with
| inleft (exist cl'' _) => inleft _ (exist _ ((s, v) :: cl'') _)
| inright _ => inright _ _
end
end); clear setClause; magic_solver.
Defined.
Definition setClauseSimple (cl : clause) (l : lit) :=
match setClause cl l with
| inleft (exist cl' _) => Some cl'
| inright _ => None
end.
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).
Definition isNil : forall (A : Set) (ls : list A), {ls = nil} + {True}.
destruct ls; eauto.
Defined.
Implicit Arguments isNil [A].
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 (eq_nat_dec (snd l') (snd l)); congruence.
Qed.
Hint Resolve satLit_idem_lit.
Lemma satLit_idem_clause : forall l a cl,
satLit l a
-> satClause cl a
-> satClause cl (upd a l).
induction cl; simpl; intuition.
Qed.
Hint Resolve satLit_idem_clause.
Lemma satLit_idem_formula : forall l a fm,
satLit l a
-> satFormula fm a
-> satFormula fm (upd a l).
induction fm; simpl; intuition.
Qed.
Hint Resolve satLit_idem_formula.
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}
: {fm' : formula |
forall a, satFormula fm (upd a l) <-> satFormula fm' a}
+ {forall a, satLit l a -> ~satFormula fm a} :=
match fm return {fm' : formula |
forall a, satFormula fm (upd a l) <-> satFormula fm' a}
+ {forall a, satLit l a -> ~satFormula fm a} with
| nil => inleft _ (exist _ nil _)
| cl :: fm' =>
match setClause cl l with
| inleft (exist cl' _) =>
if isNil cl'
then inright _ _
else match setFormula fm' l with
| inleft (exist fm'' _) => inleft _ (exist _ (cl' :: fm'') _)
| inright _ => inright _ _
end
| inright _ =>
match setFormula fm' l with
| inleft (exist fm'' _) => inleft _ (exist _ fm'' _)
| inright _ => inright _ _
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 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).
Hint Extern 1 False => discriminate.
Hint Extern 1 False =>
match goal with
| [ H : In _ (_ :: _) |- _ ] => inversion H; clear H; subst
end.
Definition findUnitClause : forall (fm : formula),
{l : lit | In (l :: nil) fm}
+ {forall l, ~In (l :: nil) fm}.
refine (fix findUnitClause (fm : formula)
: {l : lit | In (l :: nil) fm}
+ {forall l, ~In (l :: nil) fm} :=
match fm return {l : lit | In (l :: nil) fm}
+ {forall l, ~In (l :: nil) fm} with
| nil => inright _ _
| (l :: nil) :: _ => inleft _ (exist _ l _)
| _ :: fm' =>
match findUnitClause fm' with
| inleft (exist l _) => inleft _ (exist _ l _)
| inright _ => inright _ _
end
end); clear findUnitClause; magic_solver.
Defined.
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.
Qed.
Hint Resolve unitClauseTrue.
Definition unitPropagate : forall (fm : formula), option (sigS (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}).
intro fm.
refine (match findUnitClause fm with
| inleft (exist l _) =>
match setFormula fm l with
| inleft (exist fm' _) =>
Some (inleft _ (existS (fun fm' : formula =>
{l : lit |
(forall a, satFormula fm a -> satLit l a)
/\ forall a, satFormula fm (upd a l) <-> satFormula fm' a})
fm' (exist _ l _)))
| inright _ => Some (inright _ _)
end
| inright _ => None
end); magic_solver.
Defined.
Definition unitPropagateSimple (fm : formula) :=
match unitPropagate fm with
| None => None
| Some (inleft (existS fm' (exist l _))) => Some (Some (fm', l))
| Some (inright _) => Some None
end.
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).
Definition chooseSplit (fm : formula) :=
match fm with
| ((l :: _) :: _) => l
| _ => (true, 0)
end.
Definition negate (l : lit) := (negb (fst l), snd l).
Hint Unfold satFormula.
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.
Definition alist := list lit.
Fixpoint interp_alist (al : alist) : asgn :=
match al with
| nil => fun _ => true
| l :: al' => upd (interp_alist al') l
end.
Definition boundedSat (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 (existS 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, 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).
Recursive Extraction boundedSat.