diff options
| -rw-r--r-- | src/State.v | 7 | ||||
| -rw-r--r-- | src/cnf/Cnf.v | 7 |
2 files changed, 9 insertions, 5 deletions
diff --git a/src/State.v b/src/State.v index a3af611..4b0db6d 100644 --- a/src/State.v +++ b/src/State.v @@ -424,6 +424,13 @@ Module C. unfold valid, interp;destruct c;simpl; auto;discriminate. Qed. + Lemma Cinterp_neg rho cl : + interp rho (List.map Lit.neg cl) = negb (List.forallb (Lit.interp rho) cl). + Proof. + induction cl as [ |l cl IHcl]; auto. + simpl. now rewrite negb_andb, IHcl, Lit.interp_neg. + Qed. + End C. diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index 23aa979..cc956b3 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -345,9 +345,6 @@ Section CHECKER. match goal with |- context [Lit.interp rho ?x] => destruct (Lit.interp rho x);trivial end. - Axiom Cinterp_neg : forall cl, - C.interp rho (map Lit.neg cl) = negb (forallb (Lit.interp rho) cl). - Lemma valid_check_BuildDef : forall l, C.valid rho (check_BuildDef l). Proof. unfold check_BuildDef,C.valid;intros l. @@ -355,7 +352,7 @@ Section CHECKER. case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; try (unfold Lit.interp at 1;rewrite Heq;unfold Var.interp; rewrite rho_interp, H;simpl; tauto_check). - - rewrite afold_left_and, Cinterp_neg;apply orb_negb_r. + - rewrite afold_left_and, C.Cinterp_neg;apply orb_negb_r. - rewrite afold_left_or, orb_comm;apply orb_negb_r. - case_eq (PArray.length a == 0); auto using C.interp_true. intro Hl; simpl. @@ -445,7 +442,7 @@ Section CHECKER. destruct (t_form.[Lit.blit l]);auto using C.interp_true; case_eq (Lit.is_pos l);intros Heq;auto using C.interp_true;simpl; tauto_check. - - rewrite afold_left_and, Cinterp_neg, orb_false_r;trivial. + - rewrite afold_left_and, C.Cinterp_neg, orb_false_r;trivial. - rewrite afold_left_or, orb_false_r;trivial. - case_eq (PArray.length a == 0); auto using C.interp_true. intro Hl. now rewrite orb_false_r, (afold_right_impb (Lit.interp_neg _) Hl). |