diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-08-04 13:07:16 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 13:07:16 -0400 |
commit | d6770f633286d3292ad3a700c9af89e2704901d0 (patch) | |
tree | 3ee75fa83e238156c11b4cb910a3e67c20b04aa3 /src/Util | |
parent | 391fd7661eb7a48cd436c2375a4fa99978ebecd3 (diff) |
address code review comments
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Decidable.v | 10 | ||||
-rw-r--r-- | src/Util/NumTheoryUtil.v | 7 |
2 files changed, 17 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index e19e23ca4..7b412caf0 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -1,6 +1,7 @@ (** Typeclass for decidable propositions *) Require Import Coq.Logic.Eqdep_dec. +Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Equality. @@ -97,6 +98,15 @@ Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. Global Instance dec_eq_N : DecidableRel (@eq N) | 10 := N.eq_dec. Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec. +Lemma not_not P {d:Decidable P} : not (not P) <-> P. +Proof. destruct (dec P); intuition. Qed. + +Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b). +Proof. + destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right]; + [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ]. +Defined. + Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' : (exist (fun x => f x = g x) x pf) = (exist (fun x => f x = g x) x' pf') <-> (x = x'). Proof. apply path_sig_hprop_iff; auto using UIP_dec, Udec. Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 8b8595bb7..f89eb6996 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -298,3 +298,10 @@ Proof. + prime_bound. + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. Qed. + + +Lemma odd_as_div a : Z.odd a = true -> a = (2*(a/2) + 1)%Z. +Proof. + rewrite Zodd_mod, <-Zeq_is_eq_bool; intro H_1; rewrite <-H_1. + apply Z_div_mod_eq; reflexivity. +Qed.
\ No newline at end of file |