diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-04-05 16:38:01 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2019-04-05 16:38:01 -0400 |
| commit | d0825b7a3caa1a16cace6691806f708df02f2fac (patch) | |
| tree | f99c95ba3ac424aecf83424299794b29c508c461 /src | |
| parent | 72133a0e4359aa318da7897955412aa1f901d6c1 (diff) | |
Add some bool eqb lemmas
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/Bool.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Bool.v b/src/Util/Bool.v index fb2038de5..0866ab7aa 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -108,3 +108,9 @@ Lemma ex_bool_iff_or P : @ex bool P <-> (or (P true) (P false)). Proof. split; [ intros [ [] ? ] | intros [?|?]; eexists ]; eauto. Qed. + +Lemma eqb_true_l x : Bool.eqb x true = x. Proof. now destruct x. Qed. +Lemma eqb_true_r x : Bool.eqb true x = x. Proof. now destruct x. Qed. +Lemma eqb_false_l x : Bool.eqb x false = negb x. Proof. now destruct x. Qed. +Lemma eqb_false_r x : Bool.eqb false x = negb x. Proof. now destruct x. Qed. +Hint Rewrite eqb_true_l eqb_true_r eqb_false_l eqb_false_r : boolsimplify. |