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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
Require Import ZArith Nnat Lia.
Open Scope Z_scope.
(** Test of the zify preprocessor for (R)Omega *)
(* Starting from Coq 8.9 (late 2018), `romega` tactics are deprecated.
The tests in this file remain but now call the `lia` tactic. *)
(* More details in file PreOmega.v
*)
(* zify_op *)
Goal forall a:Z, Z.max a a = a.
intros.
lia.
Qed.
Goal forall a b:Z, Z.max a b = Z.max b a.
intros.
lia.
Qed.
Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
intros.
lia.
Qed.
Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
intros.
lia.
Qed.
Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
intros.
zify.
intuition; subst; lia. (* pure multiplication: omega alone can't do it *)
Qed.
Goal forall a:Z, Z.abs a = a -> a >= 0.
intros.
lia.
Qed.
Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
intros.
lia.
Qed.
(* zify_nat *)
Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
intros.
lia.
Qed.
Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
intros.
lia.
Qed.
Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
intros.
lia.
Qed.
(* 2000 instead of 200: works, but quite slow *)
Goal forall m: nat, (m*m>=0)%nat.
intros.
lia.
Qed.
(* zify_positive *)
Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
intros.
lia.
Qed.
Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
intros.
lia.
Qed.
Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
intros.
lia.
Qed.
Goal forall m: positive, (m*m>=1)%positive.
intros.
lia.
Qed.
(* zify_N *)
Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
intros.
lia.
Qed.
Goal forall m:N, (m<1)%N -> (m=0)%N.
intros.
lia.
Qed.
Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
intros.
lia.
Qed.
Goal forall m:N, (m*m>=0)%N.
intros.
lia.
Qed.
(* mix of datatypes *)
Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
intros.
lia.
Qed.
|
