diff options
author | jadep <jade.philipoom@gmail.com> | 2016-06-14 15:29:36 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-06-14 15:29:36 -0400 |
commit | ff051043f926a15ed2575122791e1d7c57fe7ac1 (patch) | |
tree | 32796809b1b4397c9913fd504715c931a92c1df9 /src/Util | |
parent | 44a9f78bb082dbc5275f7d4ae07501dc7cba8a07 (diff) | |
parent | 656f38ab96e18740df46868f31ac20814ffd6658 (diff) |
Merge
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 | 9 |
4 files changed, 12 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 59898be7a..bc2c8425b 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. @@ -77,4 +78,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 536566312..a5716fca4 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). @@ -332,7 +333,7 @@ Qed. replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). rewrite Z.div_add_l by omega. reflexivity. - replace 2 with (2 ^ 1) at 2 by auto. + change 2 with (2 ^ 1) at 2. rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). f_equal. omega. Qed. @@ -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). |