Shiftr and bound

Using Rocq
1

Dear coq users,

In proving a lemma

Lemma simple_shift: forall (x:Z), Z.shiftr x 16 = to_Z “0x4004” → to_Z “0x40040000” <= x <= to_Z “0x4004ffff” .

I have the following steps:
First, rewrite Z.shiftr x 16 to (x / 2 ^ 16 = to_Z “0x4004”) using rewrite → Z.shiftr_div_pow2.

then prove

2 ^ 16 * x / 2 ^ 16 = 2 ^ 16 *to_Z “0x4004”

change the right to

2 ^ 16 * x / 2 ^ 16 = to_Z “0x40040000” ***

and use

Z.mul_div_le: forall a b : Z, 0 < b → b * (a / b) <= a

to reach a temporary goal

2 ^ 16 * x / 2 ^ 16 <= x

Last, rewrite the left using *** , then get

to_Z “0x40040000” <= x.

Am I making things complecated?

2

Here is the proof for the lower bound.

Proof.
intros.
rewrite → Z.shiftr_div_pow2 in H.
split.
assert ((to_Z “0x40040000” (x / to_Z “0x40040000”)) <= x).
apply Z.mul_div_le. unfold to_Z. simpl. intuition.
assert ( 2^16 * (x / 2^16) = 2^16 * to_Z “0x4004” ).
rewrite → H.
reflexivity.
change (2 ^ 16 * to_Z “0x4004”) with (to_Z “0x40040000”) in H1.
rewrite ← H1.
apply Z.mul_div_le.
simpl. unfold Z.pow_pos. simpl. intuition.
( the left part is proved *)

How to prove the upper bound ( x <= to_Z “0x4004ffff” )?

3

I would try to prove a more generic lemma, say:

Lemma simple_shift: forall (x y s:Z), 
  0<=s -> Z.shiftr x s = y -> Z.shiftl y s <= x <= Z.shiftl y s + Z.ones s.

and apply this to the specific case. The proof of the generic lemma is likely shorter than the proof for the specific lemma and then you can use it for similar cases.

4

You can use lia for more automation :

Require Import ZArith String HexString Lia.

Open Scope string_scope.
Open Scope Z_scope.

Lemma simple_shift: forall (x:Z), Z.shiftr x 16 = to_Z "0x4004" -> to_Z "0x40040000"%string <= x <= to_Z "0x4004ffff".
Proof.
intros x.
(* remove shiftr *)
rewrite Z.shiftr_div_pow2; [ | lia].
(* compute to_Z *)
repeat (set (u := to_Z _); compute in u; unfold u; clear u).
(* add inequalities for div *)
assert (H := Z.mul_div_le x (2 ^ 16)).
assert (H1 := Z.mul_succ_div_gt x (2 ^ 16)).
(* automation *)
lia.
Qed.
1 Like
5

Z.mul_succ_div_gt really is the point. Thanks!