Julian
August 22, 2019, 12:58pm
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?
Julian
August 22, 2019, 1:29pm
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” )?
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.
lthery
August 22, 2019, 3:57pm
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
Julian
August 23, 2019, 2:39pm
5
Z.mul_succ_div_gt really is the point. Thanks!