Split off more of ZUtil

10 files changed, 427 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Tactics/CompareToSgn.v b/src/Util/ZUtil/Tactics/CompareToSgn.v
new file mode 100644
index 000000000..31588815b
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/CompareToSgn.v
@@ -0,0 +1,8 @@
+Require Import Coq.ZArith.ZArith.
+Module Z.
+  Ltac compare_to_sgn :=
+    repeat match goal with
+           | [ H : _ |- _ ] => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff in H
+           | _ => progress rewrite <- ?Z.sgn_neg_iff, <- ?Z.sgn_pos_iff, <- ?Z.sgn_null_iff
+           end.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/DivModToQuotRem.v b/src/Util/ZUtil/Tactics/DivModToQuotRem.v
new file mode 100644
index 000000000..b37047397
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/DivModToQuotRem.v
@@ -0,0 +1,40 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+Local Open Scope Z_scope.
+
+Module Z.
+  (** [div_mod_to_quot_rem] replaces [x / y] and [x mod y] with new
+      variables [q] and [r] while simultaneously adding facts that
+      uniquely specify [q] and [r] to the context (roughly, that [y *
+      q + r = x] and that [0 <= r < y]. *)
+  Ltac div_mod_to_quot_rem_inequality_solver :=
+    zutil_arith_more_inequalities.
+  Ltac generalize_div_eucl x y :=
+    let H := fresh in
+    let H' := fresh in
+    assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver;
+    generalize (Z.div_mod x y H'); clear H';
+    first [ assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver;
+            generalize (Z.mod_pos_bound x y H'); clear H'
+          | assert (H' : y < 0) by div_mod_to_quot_rem_inequality_solver;
+            generalize (Z.mod_neg_bound x y H'); clear H'
+          | assert (H' : y < 0 \/ 0 < y) by (apply Z.neg_pos_cases; div_mod_to_quot_rem_inequality_solver);
+            let H'' := fresh in
+            assert (H'' : y < x mod y <= 0 \/ 0 <= x mod y < y)
+              by (destruct H'; [ left; apply Z.mod_neg_bound; assumption
+                               | right; apply Z.mod_pos_bound; assumption ]);
+            clear H'; revert H'' ];
+    let q := fresh "q" in
+    let r := fresh "r" in
+    set (q := x / y);
+    set (r := x mod y);
+    clearbody q r.
+
+  Ltac div_mod_to_quot_rem_step :=
+    match goal with
+    | [ |- context[?x / ?y] ] => generalize_div_eucl x y
+    | [ |- context[?x mod ?y] ] => generalize_div_eucl x y
+    end.
+
+  Ltac div_mod_to_quot_rem := repeat div_mod_to_quot_rem_step; intros.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/DivideExistsMul.v b/src/Util/ZUtil/Tactics/DivideExistsMul.v
new file mode 100644
index 000000000..07cebc8f8
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/DivideExistsMul.v
@@ -0,0 +1,14 @@
+Require Import Coq.ZArith.ZArith Coq.omega.Omega.
+Local Open Scope Z_scope.
+
+Module Z.
+  Ltac divide_exists_mul := let k := fresh "k" in
+  match goal with
+  | [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H;
+                              match type of H with
+                              | ex _ => destruct H as [k H]
+                              | _ => destruct H
+                              end
+  | [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
+  end; (omega || auto).
+End Z.
diff --git a/src/Util/ZUtil/Tactics/LinearSubstitute.v b/src/Util/ZUtil/Tactics/LinearSubstitute.v
new file mode 100644
index 000000000..d03c9d196
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/LinearSubstitute.v
@@ -0,0 +1,66 @@
+Require Import Coq.omega.Omega Coq.ZArith.ZArith.
+Require Import Crypto.Util.Tactics.Contains.
+Require Import Crypto.Util.Tactics.Not.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma move_R_pX x y z : x + y = z -> x = z - y.
+  Proof. omega. Qed.
+  Lemma move_R_mX x y z : x - y = z -> x = z + y.
+  Proof. omega. Qed.
+  Lemma move_R_Xp x y z : y + x = z -> x = z - y.
+  Proof. omega. Qed.
+  Lemma move_R_Xm x y z : y - x = z -> x = y - z.
+  Proof. omega. Qed.
+  Lemma move_L_pX x y z : z = x + y -> z - y = x.
+  Proof. omega. Qed.
+  Lemma move_L_mX x y z : z = x - y -> z + y = x.
+  Proof. omega. Qed.
+  Lemma move_L_Xp x y z : z = y + x -> z - y = x.
+  Proof. omega. Qed.
+  Lemma move_L_Xm x y z : z = y - x -> y - z = x.
+  Proof. omega. Qed.
+
+  (** [linear_substitute x] attempts to maipulate equations using only
+      addition and subtraction to put [x] on the left, and then
+      eliminates [x].  Currently, it only handles equations where [x]
+      appears once; it does not yet handle equations like [x - x + x =
+      5]. *)
+  Ltac linear_solve_for_in_step for_var H :=
+    let LHS := match type of H with ?LHS = ?RHS => LHS end in
+    let RHS := match type of H with ?LHS = ?RHS => RHS end in
+    first [ match RHS with
+            | ?a + ?b
+              => first [ contains for_var b; apply move_L_pX in H
+                       | contains for_var a; apply move_L_Xp in H ]
+            | ?a - ?b
+              => first [ contains for_var b; apply move_L_mX in H
+                       | contains for_var a; apply move_L_Xm in H ]
+            | for_var
+              => progress symmetry in H
+            end
+          | match LHS with
+            | ?a + ?b
+              => first [ not contains for_var b; apply move_R_pX in H
+                       | not contains for_var a; apply move_R_Xp in H ]
+            | ?a - ?b
+              => first [ not contains for_var b; apply move_R_mX in H
+                       | not contains for_var a; apply move_R_Xm in H ]
+            end ].
+  Ltac linear_solve_for_in for_var H := repeat linear_solve_for_in_step for_var H.
+  Ltac linear_solve_for for_var :=
+    match goal with
+    | [ H : for_var = _ |- _ ] => idtac
+    | [ H : context[for_var] |- _ ]
+      => linear_solve_for_in for_var H;
+         lazymatch type of H with
+         | for_var = _ => idtac
+         | ?T => fail 0 "Could not fully solve for" for_var "in" T "(hypothesis" H ")"
+         end
+    end.
+  Ltac linear_substitute for_var := linear_solve_for for_var; subst for_var.
+  Ltac linear_substitute_all :=
+    repeat match goal with
+           | [ v : Z |- _ ] => linear_substitute v
+           end.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/LtbToLt.v b/src/Util/ZUtil/Tactics/LtbToLt.v
new file mode 100644
index 000000000..df6eae383
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/LtbToLt.v
@@ -0,0 +1,76 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Bool.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma eqb_cases x y : if x =? y then x = y else x <> y.
+  Proof.
+    pose proof (Z.eqb_spec x y) as H.
+    inversion H; trivial.
+  Qed.
+
+  Lemma geb_spec0 : forall x y : Z, Bool.reflect (x >= y) (x >=? y).
+  Proof.
+    intros x y; pose proof (Zge_cases x y) as H; destruct (Z.geb x y); constructor; omega.
+  Qed.
+  Lemma gtb_spec0 : forall x y : Z, Bool.reflect (x > y) (x >? y).
+  Proof.
+    intros x y; pose proof (Zgt_cases x y) as H; destruct (Z.gtb x y); constructor; omega.
+  Qed.
+
+  Ltac ltb_to_lt_with_hyp H lem :=
+    let H' := fresh in
+    rename H into H';
+    pose proof lem as H;
+    rewrite H' in H;
+    clear H'.
+
+  Ltac ltb_to_lt_in_goal b' lem :=
+    refine (proj1 (@reflect_iff_gen _ _ lem b') _);
+    cbv beta iota.
+
+  Ltac ltb_to_lt_hyps_step :=
+    match goal with
+    | [ H : (?x <? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zlt_cases x y)
+    | [ H : (?x <=? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zle_cases x y)
+    | [ H : (?x >? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zgt_cases x y)
+    | [ H : (?x >=? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (Zge_cases x y)
+    | [ H : (?x =? ?y) = ?b |- _ ]
+      => ltb_to_lt_with_hyp H (eqb_cases x y)
+    end.
+  Ltac ltb_to_lt_goal_step :=
+    match goal with
+    | [ |- (?x <? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.ltb_spec0 x y)
+    | [ |- (?x <=? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.leb_spec0 x y)
+    | [ |- (?x >? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.gtb_spec0 x y)
+    | [ |- (?x >=? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.geb_spec0 x y)
+    | [ |- (?x =? ?y) = ?b ]
+      => ltb_to_lt_in_goal b (Z.eqb_spec x y)
+    end.
+  Ltac ltb_to_lt_step :=
+    first [ ltb_to_lt_hyps_step
+          | ltb_to_lt_goal_step ].
+  Ltac ltb_to_lt := repeat ltb_to_lt_step.
+
+  Section R_Rb.
+    Local Ltac t := intros ? ? []; split; intro; ltb_to_lt; omega.
+    Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y).
+    Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed.
+    Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed.
+    Lemma gtb_gt_iff : R_Rb Z.gtb Z.gt Z.le. Proof. t. Qed.
+    Lemma geb_ge_iff : R_Rb Z.geb Z.ge Z.lt. Proof. t. Qed.
+    Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed.
+  End R_Rb.
+  Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt.
+  Ltac ltb_to_lt_in_context :=
+    repeat autorewrite with ltb_to_lt in *;
+    cbv beta iota in *.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/PrimeBound.v b/src/Util/ZUtil/Tactics/PrimeBound.v
new file mode 100644
index 000000000..f914ed7c8
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/PrimeBound.v
@@ -0,0 +1,7 @@
+Require Import Coq.omega.Omega Coq.ZArith.Znumtheory.
+
+Module Z.
+  Ltac prime_bound := match goal with
+  | [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
+  end.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
new file mode 100644
index 000000000..67b5397aa
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
@@ -0,0 +1,34 @@
+Require Import Coq.omega.Omega Coq.ZArith.ZArith.
+Local Open Scope Z_scope.
+
+Module Z.
+  Ltac clean_neg :=
+    repeat match goal with
+           | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H
+           | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H
+           | [ H : (-?x) <= 0 |- _ ] => assert (0 <= x) by omega; clear H
+           | [ H : 0 >= (-?x) |- _ ] => assert (0 <= x) by omega; clear H
+           | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H
+           | [ |- -?x <= -?y ] => apply Z.opp_le_mono
+           | _ => progress rewrite <- Z.opp_le_mono in *
+           | [ H : 0 <= ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x < ?y |- _ ] => clear H''
+           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+           end.
+  Ltac replace_with_neg x :=
+    assert (x = -(-x)) by (symmetry; apply Z.opp_involutive); generalize dependent (-x);
+    let x' := fresh in
+    rename x into x'; intro x; intros; subst x';
+    clean_neg.
+  Ltac replace_all_neg_with_pos :=
+    repeat match goal with
+           | [ H : ?x < 0 |- _ ] => replace_with_neg x
+           | [ H : 0 > ?x |- _ ] => replace_with_neg x
+           | [ H : ?x <= 0 |- _ ] => replace_with_neg x
+           | [ H : 0 >= ?x |- _ ] => replace_with_neg x
+           end.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v b/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
new file mode 100644
index 000000000..c5b024eca
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/SimplifyFractionsLe.v
@@ -0,0 +1,133 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds.
+Require Import Crypto.Util.ZUtil.Div.
+Local Open Scope Z_scope.
+
+Module Z.
+  (** * [Z.simplify_fractions_le] *)
+  (** The culmination of this series of tactics,
+      [Z.simplify_fractions_le], will use the fact that [a * (b / c) <=
+      (a * b) / c], and do some reasoning modulo associativity and
+      commutativity in [Z] to perform such a reduction.  It may leave
+      over goals if it cannot prove that some denominators are non-zero.
+      If the rewrite [a * (b / c)] → [(a * b) / c] is safe to do on the
+      LHS of the goal, this tactic should not turn a solvable goal into
+      an unsolvable one.
+
+      After running, the tactic does some basic rewriting to simplify
+      fractions, e.g., that [a * b / b = a]. *)
+  Ltac split_sums_step :=
+    match goal with
+    | [ |- _ + _ <= _ ]
+      => etransitivity; [ eapply Z.add_le_mono | ]
+    | [ |- _ - _ <= _ ]
+      => etransitivity; [ eapply Z.sub_le_mono | ]
+    end.
+  Ltac split_sums :=
+    try (split_sums_step; [ split_sums.. | ]).
+  Ltac pre_reorder_fractions_step :=
+    match goal with
+    | [ |- context[?x / ?y * ?z] ]
+      => lazymatch z with
+         | context[_ / _] => fail
+         | _ => idtac
+         end;
+         rewrite (Z.mul_comm (x / y) z)
+    | _ => let LHS := match goal with |- ?LHS <= ?RHS => LHS end in
+           match LHS with
+           | context G[?x * (?y / ?z)]
+             => let G' := context G[(x * y) / z] in
+                transitivity G'
+           end
+    end.
+  Ltac pre_reorder_fractions :=
+    try first [ split_sums_step; [ pre_reorder_fractions.. | ]
+              | pre_reorder_fractions_step; [ .. | pre_reorder_fractions ] ].
+  Ltac split_comparison :=
+    match goal with
+    | [ |- ?x <= ?x ] => reflexivity
+    | [ H : _ >= _ |- _ ]
+      => apply Z.ge_le_iff in H
+    | [ |- ?x * ?y <= ?z * ?w ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
+         end;
+         [ ..
+         | lazymatch goal with
+           | [ H : 0 <= y |- _ ] => idtac
+           | [ H : y < 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec y 0)
+           end;
+           [ ..
+           | apply Zmult_le_compat; [ | | assumption | assumption ] ] ]
+    | [ |- ?x / ?y <= ?z / ?y ]
+      => lazymatch goal with
+         | [ H : 0 < y |- _ ] => idtac
+         | [ H : y <= 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec 0 y)
+         end;
+         [ apply Z_div_le; [ apply Z.gt_lt_iff; assumption | ]
+         | .. ]
+    | [ |- ?x / ?y <= ?x / ?z ]
+      => lazymatch goal with
+         | [ H : 0 <= x |- _ ] => idtac
+         | [ H : x < 0 |- _ ] => fail
+         | _ => destruct (Z_lt_le_dec x 0)
+         end;
+         [ ..
+         | lazymatch goal with
+           | [ H : 0 < z |- _ ] => idtac
+           | [ H : z <= 0 |- _ ] => fail
+           | _ => destruct (Z_lt_le_dec 0 z)
+           end;
+           [ apply Z.div_le_compat_l; [ assumption | split; [ assumption | ] ]
+           | .. ] ]
+    | [ |- _ + _ <= _ + _ ]
+      => apply Z.add_le_mono
+    | [ |- _ - _ <= _ - _ ]
+      => apply Z.sub_le_mono
+    | [ |- ?x * (?y / ?z) <= (?x * ?y) / ?z ]
+      => apply Z.div_mul_le
+    end.
+  Ltac split_comparison_fin_step :=
+    match goal with
+    | _ => assumption
+    | _ => lia
+    | _ => progress subst
+    | [ H : ?n * ?m < 0 |- _ ]
+      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [ [??]|[??] ]
+    | [ H : ?n / ?m < 0 |- _ ]
+      => apply (proj1 (Z.lt_div_0 n m)) in H; destruct H as [ [ [??]|[??] ] ? ]
+    | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
+      => assert (0 <= x^y) by Z.zero_bounds; lia
+    | [ H : (?x^?y) < 0 |- _ ]
+      => assert (0 <= x^y) by Z.zero_bounds; lia
+    | [ H : (?x^?y) <= 0 |- _ ]
+      => let H' := fresh in
+         assert (H' : 0 <= x^y) by Z.zero_bounds;
+         assert (x^y = 0) by lia;
+         clear H H'
+    | [ H : _^_ = 0 |- _ ]
+      => apply Z.pow_eq_0_iff in H; destruct H as [ ?|[??] ]
+    | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
+      => assert (x = 0) by lia; clear H H'
+    | [ |- ?x <= ?y ] => is_evar x; reflexivity
+    | [ |- ?x <= ?y ] => is_evar y; reflexivity
+    end.
+  Ltac split_comparison_fin := repeat split_comparison_fin_step.
+  Ltac simplify_fractions_step :=
+    match goal with
+    | _ => rewrite Z.div_mul by (try apply Z.pow_nonzero; Z.zero_bounds)
+    | [ |- context[?x * ?y / ?x] ]
+      => rewrite (Z.mul_comm x y)
+    | [ |- ?x <= ?x ] => reflexivity
+    end.
+  Ltac simplify_fractions := repeat simplify_fractions_step.
+  Ltac simplify_fractions_le :=
+    pre_reorder_fractions;
+    [ repeat split_comparison; split_comparison_fin; Z.zero_bounds..
+    | simplify_fractions ].
+End Z.
diff --git a/src/Util/ZUtil/Tactics/ZeroBounds.v b/src/Util/ZUtil/Tactics/ZeroBounds.v
new file mode 100644
index 000000000..d10b6714c
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/ZeroBounds.v
@@ -0,0 +1,27 @@
+Require Import Coq.ZArith.ZArith Coq.omega.Omega.
+Require Import Crypto.Util.ZUtil.Tactics.PrimeBound.
+Local Open Scope Z_scope.
+
+Module Z.
+  (* prove that combinations of known positive/nonnegative numbers are positive/nonnegative *)
+  Ltac zero_bounds' :=
+    repeat match goal with
+    | [ |- 0 <= _ + _] => apply Z.add_nonneg_nonneg
+    | [ |- 0 <= _ - _] => apply Z.le_0_sub
+    | [ |- 0 <= _ * _] => apply Z.mul_nonneg_nonneg
+    | [ |- 0 <= _ / _] => apply Z.div_pos
+    | [ |- 0 <= _ ^ _ ] => apply Z.pow_nonneg
+    | [ |- 0 <= Z.shiftr _ _] => apply Z.shiftr_nonneg
+    | [ |- 0 <= _ mod _] => apply Z.mod_pos_bound
+    | [ |- 0 < _ + _] => try solve [apply Z.add_pos_nonneg; zero_bounds'];
+                         try solve [apply Z.add_nonneg_pos; zero_bounds']
+    | [ |- 0 < _ - _] => apply Z.lt_0_sub
+    | [ |- 0 < _ * _] => apply Z.lt_0_mul; left; split
+    | [ |- 0 < _ / _] => apply Z.div_str_pos
+    | [ |- 0 < _ ^ _ ] => apply Z.pow_pos_nonneg
+    end; try omega; try Z.prime_bound; auto.
+
+  Ltac zero_bounds := try omega; try Z.prime_bound; zero_bounds'.
+
+  Hint Extern 1 => progress zero_bounds : zero_bounds.
+End Z.
diff --git a/src/Util/ZUtil/Tactics/Ztestbit.v b/src/Util/ZUtil/Tactics/Ztestbit.v
new file mode 100644
index 000000000..d12de5330
--- /dev/null
+++ b/src/Util/ZUtil/Tactics/Ztestbit.v
@@ -0,0 +1,22 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Testbit.
+Require Import Crypto.Util.ZUtil.Hints.Core.
+
+Ltac Ztestbit_full_step :=
+  match goal with
+  | _ => progress autorewrite with Ztestbit_full
+  | [ |- context[Z.testbit ?x ?y] ]
+    => rewrite (Z.testbit_neg_r x y) by zutil_arith
+  | [ |- context[Z.testbit ?x ?y] ]
+    => rewrite (Z.bits_above_pow2 x y) by zutil_arith
+  | [ |- context[Z.testbit ?x ?y] ]
+    => rewrite (Z.bits_above_log2 x y) by zutil_arith
+  end.
+Ltac Ztestbit_full := repeat Ztestbit_full_step.
+
+Ltac Ztestbit_step :=
+  match goal with
+  | _ => progress autorewrite with Ztestbit
+  | _ => progress Ztestbit_full_step
+  end.
+Ltac Ztestbit := repeat Ztestbit_step.