From 651a3f29878214e9c33ce8bb103dc8c40191c950 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 24 Apr 2023 19:01:22 +0100 Subject: Added lemmas about decidability of Sat --- src/hls/Sat.v | 146 +++++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 104 insertions(+), 42 deletions(-) (limited to 'src/hls/Sat.v') diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 960be8e..9c73bee 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -182,8 +182,8 @@ 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} + {True}. - destruct ls; [left|right]; eauto. +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]. @@ -555,12 +555,59 @@ Proof. pose proof (sat_measure_setClause'' _ _ _ _ H1). Admitted. -Definition InFm l (fm: formula) := exists cl, In cl fm /\ In l cl. +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_setFormula : - forall fm fm' l A, + forall fm fm' l b A, InFm l fm -> - setFormula fm l = inleft (exist _ fm' A) -> + setFormula fm (b, l) = inleft (exist _ fm' A) -> sat_measure fm' < sat_measure fm. Proof. Admitted. @@ -579,42 +626,50 @@ Proof. Program Fixpoint satSolve (fm: formula) { measure (sat_measure fm) }: {al : alist | satFormula fm (interp_alist al)} + {forall a, ~satFormula fm a} := - if isNil fm - then inleft _ (exist _ nil _) - else 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. + 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. @@ -622,11 +677,18 @@ Next Obligation. 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. Admitted. Next Obligation. apply wildcard'0; auto. Defined. Next Obligation. - Admitted. + eapply sat_measure_setFormula. admit. symmetry. eauto. Admitted. Next Obligation. apply wildcard'2; auto. Defined. Next Obligation. -- cgit