From d0825b7a3caa1a16cace6691806f708df02f2fac Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 5 Apr 2019 16:38:01 -0400 Subject: Add some bool eqb lemmas --- src/Util/Bool.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src') 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. -- cgit v1.2.3