diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-13 00:09:51 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-05-13 18:42:29 -0400 |
| commit | 309e71d4bf766257960c176ce7bdb44df80758e7 (patch) | |
| tree | f5ceeb40ecf8d1c49d3fe6c80a6268f9671ea362 /src | |
| parent | 20de5e544ff04340c1c2f6e471d8549f6fea0986 (diff) | |
Add proper lemma for add_with_carry
Diffstat (limited to 'src')
| -rw-r--r-- | src/Util/ZUtil/Morphisms.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index bb708ab8a..e0ab179a8 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -2,6 +2,8 @@ Require Import Coq.omega.Omega. Require Import Coq.ZArith.ZArith. Require Import Coq.Classes.Morphisms. +Require Import Coq.Classes.RelationPairs. +Require Import Crypto.Util.ZUtil.Definitions. Local Open Scope Z_scope. Module Z. @@ -42,4 +44,6 @@ Module Z. Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. Lemma pow_Zpos_le_Proper_flip x : Proper (Basics.flip Z.le ==> Basics.flip Z.le) (Z.pow (Z.pos x)). Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. + Lemma add_with_carry_le_Proper : Proper (Z.le ==> Z.le ==> Z.le ==> Z.le) Z.add_with_carry. + Proof. unfold Z.add_with_carry; repeat (omega || intro). Qed. End Z. |