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
|
Require Import Lia ZArith.
Open Scope Z_scope.
Unset Lia Cache.
(* Expected time < 1.00s *)
Goal forall (two64 right left : Z) (length_xs v : nat) (x2 x1 : Z)
(length_x : nat) (r3 r2 q r r1 q0 r0 q1 q2 q3 : Z),
two64 = 2 ^ 64 ->
r3 = 8 * Z.of_nat length_xs ->
r2 = 8 * Z.of_nat length_x ->
0 <= 8 * Z.of_nat length_x ->
8 * Z.of_nat length_x < two64 ->
r1 = 2 ^ 4 * q + r ->
0 < 2 ^ 4 ->
0 <= r ->
r < 2 ^ 4 ->
x1 + q * 2 ^ 3 - x1 = two64 * q0 + r0 ->
0 < two64 ->
0 <= r0 ->
r0 < two64 ->
8 * Z.of_nat length_x = two64 * q1 + r1 ->
0 <= r1 ->
r1 < two64 ->
x2 - x1 = two64 * q2 + r2 ->
0 <= r2 ->
r2 < two64 ->
right - left = two64 * q3 + r3 ->
0 <= r3 ->
r3 < two64 ->
Z.of_nat length_x = Z.of_nat v ->
0 <= Z.of_nat length_x ->
0 <= Z.of_nat length_xs ->
0 <= Z.of_nat v ->
(r2 = 0 -> False) ->
(2 ^ 4 = 0 -> False) ->
(2 ^ 4 < 0 -> False) ->
(two64 = 0 -> False) ->
(two64 < 0 -> False) ->
(r0 < 8 * Z.of_nat length_x -> False) ->
False.
Proof.
intros.
Time lia.
Qed.
|
