aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-11-08 13:10:35 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-11-08 13:10:35 -0500
commitb103fcc6f1d130cc4c6d9200851f62a392c1d798 (patch)
treeaf025f9d535ab908e10abae60e789444f23a2f78 /src
parentc89a77f3b6de068aaf1b8cd2adad73ef64c7fb13 (diff)
Prove things in ModularBaseSystemListZOperationsProofs
Diffstat (limited to 'src')
-rw-r--r--src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v13
-rw-r--r--src/Util/ZUtil.v2
2 files changed, 11 insertions, 4 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
index bb833507f..5d9e64901 100644
--- a/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListZOperationsProofs.v
@@ -5,9 +5,14 @@ Require Import Crypto.Util.ZUtil.
Local Open Scope Z_scope.
-Lemma neg_nonneg : forall x y, 0 <= ModularBaseSystemListZOperations.neg x y.
-Proof. Admitted.
+Lemma neg_nonneg : forall x y, 0 <= x -> 0 <= ModularBaseSystemListZOperations.neg x y.
+Proof.
+ unfold neg; intros; break_match; auto with zarith.
+Qed.
Hint Resolve neg_nonneg : zarith.
-Lemma neg_upperbound : forall x y, ModularBaseSystemListZOperations.neg x y <= Z.ones x.
-Proof. Admitted.
+
+Lemma neg_upperbound : forall x y, 0 <= x -> ModularBaseSystemListZOperations.neg x y <= Z.ones x.
+Proof.
+ unfold neg; intros; break_match; auto with zarith.
+Qed.
Hint Resolve neg_upperbound : zarith.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 17e8d62bf..9dc4eeb51 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -944,6 +944,7 @@ Module Z.
rewrite Z.ones_succ by assumption.
zero_bounds.
Qed.
+ Hint Resolve ones_nonneg : zarith.
Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i.
Proof.
@@ -953,6 +954,7 @@ Module Z.
apply Z.lt_succ_lt_pred.
apply Z.pow_gt_1; omega.
Qed.
+ Hint Resolve ones_pos_pos : zarith.
Lemma pow2_mod_id_iff : forall a n, 0 <= n ->
(Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n).