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
|
(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
The tests in this file remain but now call the `lia` tactic. *)
Require Import ZArith Lia.
(* Submitted by Yegor Bryukhov (BZ#922) *)
Open Scope Z_scope.
(* First a simplified version used during debug of romega on Test46 *)
Lemma Test46_simplified :
forall v1 v2 v5 : Z,
0 = v2 + v5 ->
0 < v5 ->
0 < v2 ->
4*v2 <> 5*v1.
intros.
lia.
Qed.
(* The complete problem *)
Lemma Test46 :
forall v1 v2 v3 v4 v5 : Z,
((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) ->
((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 ->
0 > 6 * v1 ->
(0 * v3) + (6 * v2) <> 2 ->
(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) ->
7 * v3 > 5 * v5 ->
0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) ->
7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) ->
0 * v3 > 7 * v1 ->
9 * v2 < 9 * v5 ->
(2 * v3) + (8 * v1) <= 5 * v4 ->
5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) ->
0 * v5 <= 9 * v2 ->
((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
-> False.
intros.
lia.
Qed.
|
