diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-30 16:33:47 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2020-06-30 16:33:47 +0200 |
| commit | d7a33ad9b479317701eba7c787744599de134f78 (patch) | |
| tree | de5831e7b1b0fb79fe459a819bbe2590e14a1682 /src/cnf/Cnf.v | |
| parent | f492399d3673dfc1ce63eb5a81d2690a30dc745e (diff) | |
| parent | fa287eec3d57135ed1bd9285be0bc600449b13c1 (diff) | |
| download | smtcoq-d7a33ad9b479317701eba7c787744599de134f78.tar.gz smtcoq-d7a33ad9b479317701eba7c787744599de134f78.zip | |
Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10
Diffstat (limited to 'src/cnf/Cnf.v')
| -rw-r--r-- | src/cnf/Cnf.v | 7 |
1 files changed, 2 insertions, 5 deletions
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). |