diff options
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/CaseUtil.v | 6 | ||||
-rw-r--r-- | src/Util/IterAssocOp.v | 4 | ||||
-rw-r--r-- | src/Util/NatUtil.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 8 |
4 files changed, 11 insertions, 9 deletions
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v index cf3ebf29c..2d1ab6c58 100644 --- a/src/Util/CaseUtil.v +++ b/src/Util/CaseUtil.v @@ -1,12 +1,12 @@ -Require Import Coq.Arith.Arith. +Require Import Coq.Arith.Arith Coq.Arith.Max. Ltac case_max := match goal with [ |- context[max ?x ?y] ] => destruct (le_dec x y); match goal with - | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by + | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_r by (exact H) - | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_l by + | [ H : ~ (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite max_l by (exact (le_Sn_le _ _ (not_le _ _ H))) end end. diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 6116312e1..82d22046d 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -1,5 +1,7 @@ Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.NArith.NArith Coq.PArith.BinPosDef. +Require Import Coq.Numbers.Natural.Peano.NPeano. + Local Open Scope equiv_scope. Generalizable All Variables. @@ -147,7 +149,7 @@ Section IterAssocOp. destruct (funexp (test_and_op n a) (x, acc) y) as [i acc']. simpl in IHy. unfold test_and_op. - destruct i; rewrite NPeano.Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. + destruct i; rewrite Nat.sub_succ_r; subst; rewrite <- IHy; simpl; reflexivity. Qed. Lemma iter_op_termination : forall sc a bound, diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index 1f69b04d2..f86ecee2e 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -1,4 +1,5 @@ Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega. +Import Nat. Local Open Scope nat_scope. @@ -66,4 +67,3 @@ Proof. [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ]. Qed. - diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 1b7cfafdc..3ffc69fc5 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2,6 +2,7 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil. Require Import Coq.Lists.List. +Import Nat. Local Open Scope Z. Lemma gt_lt_symmetry: forall n m, n > m <-> m < n. @@ -208,7 +209,7 @@ Proof. rewrite (le_plus_minus n m) at 1 by assumption. rewrite Nat2Z.inj_add. rewrite Z.pow_add_r by apply Nat2Z.is_nonneg. - rewrite <- Z.div_div by first + rewrite <- Z.div_div by first [ pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega | apply Z.pow_pos_nonneg; omega ]. rewrite Z.div_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat n)); omega). @@ -345,7 +346,7 @@ Qed. + unfold Z.ones. rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. omega. - + intros. + + intros. destruct (Z_lt_le_dec x n); try omega. intuition. left. @@ -360,7 +361,7 @@ Qed. Z.shiftr a i <= Z.ones (n - i) . Proof. intros a n i G G0 G1. - destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_le_lt_eq_dec i n G1). + destruct (Z_shiftr_ones' a n G i G0); omega. + subst; rewrite Z.sub_diag. destruct (Z_eq_dec a 0). @@ -415,4 +416,3 @@ Ltac zero_bounds := try omega; try prime_bound; zero_bounds'. zero_bounds. apply Z.pow_nonneg; omega. Qed. - |