diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-17 15:20:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-17 15:20:26 -0400 |
| commit | 14001d95b2d6a9cc05b0ecc782afdf9709f97a38 (patch) | |
| tree | 6cfcf271b17f69e573835fcc6e2466f2b8afb065 /src/Util/ZUtil.v | |
| parent | 593093d4795fe497655f25ff26767d807e01bfea (diff) | |
Add more simplify lemmas to ZUtil
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index b61219480..739fbb255 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2024,6 +2024,18 @@ Module Z. Lemma simplify_add_pos x y : Z.pos x + Z.pos y = Z.pos (x + y). Proof. reflexivity. Qed. + Lemma simplify_add_pos10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 + : Z.pos x0 + (Z.pos x1 + (Z.pos x2 + (Z.pos x3 + (Z.pos x4 + (Z.pos x5 + (Z.pos x6 + (Z.pos x7 + (Z.pos x8 + Z.pos x9)))))))) + = Z.pos (x0 + (x1 + (x2 + (x3 + (x4 + (x5 + (x6 + (x7 + (x8 + x9))))))))). + Proof. reflexivity. Qed. + Lemma simplify_mul_pos x y : Z.pos x * Z.pos y = Z.pos (x * y). + Proof. reflexivity. Qed. + Lemma simplify_mul_pos10 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 + : Z.pos x0 * (Z.pos x1 * (Z.pos x2 * (Z.pos x3 * (Z.pos x4 * (Z.pos x5 * (Z.pos x6 * (Z.pos x7 * (Z.pos x8 * Z.pos x9)))))))) + = Z.pos (x0 * (x1 * (x2 * (x3 * (x4 * (x5 * (x6 * (x7 * (x8 * x9))))))))). + Proof. reflexivity. Qed. + Lemma simplify_sub_pos x y : Z.pos x - Z.pos y = Z.pos_sub x y. + Proof. reflexivity. Qed. Lemma move_R_pX x y z : x + y = z -> x = z - y. Proof. omega. Qed. |