blob: 94fa05e1a87c7a857d872ef4ab21b593884cc3a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
Require Import Coq.ZArith.ZArith Coq.micromega.Lia Coq.omega.Omega.
Require Import Crypto.Util.ZUtil.Hints.Core.
Local Open Scope Z_scope.
Module Z.
Lemma pow_1_l_Zpos a : 1^Zpos a = 1.
Proof. apply Z.pow_1_l; lia. Qed.
Hint Rewrite pow_1_l_Zpos : zsimplify_fast zsimplify_const zsimplify.
Lemma pow_1_l_0 : 1^Z0 = 1. Proof. reflexivity. Qed.
Hint Rewrite pow_1_l_0 : zsimplify_fast zsimplify_const zsimplify.
Lemma pow_r_Zneg a b : a^Zneg b = 0. Proof. reflexivity. Qed.
Hint Rewrite pow_r_Zneg : zsimplify_fast zsimplify_const zsimplify.
Lemma pow_1_l_Zof_nat a : 1^Z.of_nat a = 1.
Proof. apply Z.pow_1_l; lia. Qed.
Hint Rewrite pow_1_l_Zof_nat : zsimplify_fast zsimplify_const zsimplify.
Lemma sub_same_minus (x y : Z) : x - (x - y) = y.
Proof. lia. Qed.
Hint Rewrite sub_same_minus : zsimplify.
Lemma sub_same_plus (x y : Z) : x - (x + y) = -y.
Proof. lia. Qed.
Hint Rewrite sub_same_plus : zsimplify.
Lemma sub_same_minus_plus (x y z : Z) : x - (x - y + z) = y - z.
Proof. lia. Qed.
Hint Rewrite sub_same_minus_plus : zsimplify.
Lemma sub_same_plus_plus (x y z : Z) : x - (x + y + z) = -y - z.
Proof. lia. Qed.
Hint Rewrite sub_same_plus_plus : zsimplify.
Lemma sub_same_minus_minus (x y z : Z) : x - (x - y - z) = y + z.
Proof. lia. Qed.
Hint Rewrite sub_same_minus_minus : zsimplify.
Lemma sub_same_plus_minus (x y z : Z) : x - (x + y - z) = z - y.
Proof. lia. Qed.
Hint Rewrite sub_same_plus_minus : zsimplify.
Lemma sub_same_minus_then_plus (x y w : Z) : x - (x - y) + w = y + w.
Proof. lia. Qed.
Hint Rewrite sub_same_minus_then_plus : zsimplify.
Lemma sub_same_plus_then_plus (x y w : Z) : x - (x + y) + w = w - y.
Proof. lia. Qed.
Hint Rewrite sub_same_plus_then_plus : zsimplify.
Lemma sub_same_minus_plus_then_plus (x y z w : Z) : x - (x - y + z) + w = y - z + w.
Proof. lia. Qed.
Hint Rewrite sub_same_minus_plus_then_plus : zsimplify.
Lemma sub_same_plus_plus_then_plus (x y z w : Z) : x - (x + y + z) + w = w - y - z.
Proof. lia. Qed.
Hint Rewrite sub_same_plus_plus_then_plus : zsimplify.
Lemma sub_same_minus_minus_then_plus (x y z w : Z) : x - (x - y - z) + w = y + z + w.
Proof. lia. Qed.
Hint Rewrite sub_same_minus_minus : zsimplify.
Lemma sub_same_plus_minus_then_plus (x y z w : Z) : x - (x + y - z) + w = z - y + w.
Proof. lia. Qed.
Hint Rewrite sub_same_plus_minus_then_plus : zsimplify.
Lemma simplify_twice_sub_sub x y : 2 * x - (x - y) = x + y.
Proof. lia. Qed.
Hint Rewrite simplify_twice_sub_sub : zsimplify.
Lemma simplify_twice_sub_add x y : 2 * x - (x + y) = x - y.
Proof. lia. Qed.
Hint Rewrite simplify_twice_sub_add : zsimplify.
Lemma simplify_2XmX X : 2 * X - X = X.
Proof. omega. Qed.
Hint Rewrite simplify_2XmX : zsimplify.
Lemma simplify_add_pos x y : Z.pos x + Z.pos y = Z.pos (x + y).
Proof. reflexivity. Qed.
Hint Rewrite simplify_add_pos : zsimplify_Z_to_pos.
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.
Hint Rewrite simplify_add_pos10 : zsimplify_Z_to_pos.
Lemma simplify_mul_pos x y : Z.pos x * Z.pos y = Z.pos (x * y).
Proof. reflexivity. Qed.
Hint Rewrite simplify_mul_pos : zsimplify_Z_to_pos.
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.
Hint Rewrite simplify_mul_pos10 : zsimplify_Z_to_pos.
Lemma simplify_sub_pos x y : Z.pos x - Z.pos y = Z.pos_sub x y.
Proof. reflexivity. Qed.
Hint Rewrite simplify_sub_pos : zsimplify_Z_to_pos.
Lemma two_sub_sub_inner_sub x y z : 2 * x - y - (x - z) = x - y + z.
Proof. clear; lia. Qed.
Hint Rewrite two_sub_sub_inner_sub : zsimplify.
Lemma minus_minus_one : - -1 = 1.
Proof. reflexivity. Qed.
Hint Rewrite minus_minus_one : zsimplify zsimplify_fast zsimplify_const.
End Z.
|
