Library Asm.Util.ArithUtil
Require Import Coq.Arith.Arith ZArith.
Require Import Asm.Util.Tactics.
Fixpoint pow2 (n : nat) : nat :=
match n with
| O => 1
| S n => 2 * pow2 n
end.
Lemma rewrite_plus_0 : forall e, e + 0 = e.
Lemma rewrite_minus_0 : forall e, e - 0 = e.
Lemma Z_rewrite_plus_0 : forall e, (e + 0 = e)%Z.
Lemma Z_rewrite_times_0 : forall e, (0 * e = 0)%Z.
Lemma rewrite_times_2 : forall e, e + e = 2 * e.
Lemma rewrite_undistrib : forall x y z, x * y + x * z = x * (y + z).
Lemma rewrite_undistrib_minus : forall x y z,
x * y - x * z = x * (y - z).
Lemma rewrite_minus_plus : forall x y z,
x - (y + z) = x - y - z.
Hint Rewrite rewrite_plus_0 rewrite_minus_0 rewrite_times_2
rewrite_undistrib rewrite_undistrib_minus : asm.
Hint Rewrite Z_rewrite_plus_0 Z_rewrite_times_0 : asm.
Lemma rewrite_undistrib_minus_const : forall x y,
x * y - x = x * (y - 1).
Hint Rewrite rewrite_undistrib_minus_const : asm.
Lemma sub_one_S : forall n m,
n - 1 - S m = n - 2 - m.
Hint Rewrite sub_one_S : asm.
Lemma double_minus : forall n,
2 * S n - 1 = 2 * (S n - 1) + 1.
Lemma double_minus' : forall n,
n > 0
-> 2 * n - 1 = 2 * (n - 1) + 1.
Hint Rewrite double_minus : asm.
Hint Rewrite double_minus' using (myauto; fail) : asm.
Lemma sub_one : forall k n,
S k * S n - 1 = S k * (S n - 1) + k.
Lemma pow2_pos : forall n, pow2 n > 0.
Lemma sub_one_pow2 : forall k n,
S k * pow2 n - 1 = S k * (pow2 n - 1) + k.
Lemma minus_S_1 : forall n m,
n - S m - 1 = n - m - 2.
Hint Rewrite sub_one sub_one_pow2 minus_S_1 : asm.
Lemma S_minus_1 : forall n, S (S n) - 1 = S (S n - 1).
Lemma percolate_minus_1 : forall n m,
n - 1 - m = n - m - 1.
Hint Rewrite S_minus_1 percolate_minus_1 : asm.
Ltac Z_of_nat_tac :=
match goal with
| [ H : ?X = ?Y |- _] =>
let H' := fresh in
(assert (H' : Z_of_nat X = Z_of_nat Y);
[ congruence | clear H; rename H' into H])
| [ H : ?X > ?Y |- _] =>
let H' := fresh in
(assert (H' : (Z_of_nat X > Z_of_nat Y)%Z);
[ apply inj_gt; trivial | clear H; rename H' into H])
end.
Lemma Z_of_nat_bit : forall n,
2 > n
-> Z_of_nat n = 0%Z \/ Z_of_nat n = 1%Z.
Lemma Psucc_inj : forall n m,
Psucc n = Psucc m
-> n = m.
Lemma P_of_succ_nat_inj : forall n m,
P_of_succ_nat n = P_of_succ_nat m
-> n = m.
Lemma Z_of_nat_inj : forall n m,
Z_of_nat n = Z_of_nat m
-> n = m.
Lemma S_times_two : forall n,
S (S (2 * n)) = 2 * (S n).
Hint Rewrite S_times_two : asm.
Lemma pow2_times2 : forall n,
pow2 (2 * n) = pow2 n * pow2 n.
Theorem pow2_plus : forall n m,
pow2 n * pow2 m = pow2 (n + m).
Theorem demult : forall k n m,
k >= 1
-> n * k < m * k
-> n < m.
Theorem rewrite_S : forall n,
S n = n + 1.
Lemma plus_minus : forall n m k,
k <= m
-> n + (m - k) = n + m - k.
Lemma minus_plus' : forall n m k,
n - (m + k) = n - k - m.
Index
This page has been generated by coqdoc