diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-10-26 20:24:12 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-10-26 20:24:12 +0100 |
| commit | e51e42283ac9f1f0a80c989ebca7d52eb35f08d3 (patch) | |
| tree | e4e9615be7869348d6c3b1cbbc00bc92cfb7675c /src/hls/Predicate.v | |
| parent | b1ca2f1a6159a313e259a697826380962d7cfa48 (diff) | |
| download | vericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.tar.gz vericert-e51e42283ac9f1f0a80c989ebca7d52eb35f08d3.zip | |
Work more on equivalence of SAT
Diffstat (limited to 'src/hls/Predicate.v')
| -rw-r--r-- | src/hls/Predicate.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/hls/Predicate.v b/src/hls/Predicate.v index 0ab7e77..ec558c6 100644 --- a/src/hls/Predicate.v +++ b/src/hls/Predicate.v @@ -399,6 +399,21 @@ Proof. apply equiv_check_dec in H. crush. Qed. +Lemma equiv_check_decidable2 : + forall p1 p2, {p1 == p2} + {p1 =/= p2}. +Proof. + intros. destruct (equiv_check p1 p2) eqn:?. + unfold decidable. + left. apply equiv_check_dec; auto. + unfold decidable, not; right; intros. + simpl. unfold complement. intros. + apply not_true_iff_false in Heqb. apply Heqb. + apply equiv_check_dec. eauto. +Qed. + #[global] Instance DecidableSATSetoid : DecidableSetoid SATSetoid := { setoid_decidable := equiv_check_decidable }. + +#[global] +Instance SATSetoidEqDec : EqDec SATSetoid := equiv_check_decidable2. |