coq-common.gen 6.28 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"

(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_non_struct_recursion"

transformation "eliminate_if"

16
17
transformation "eliminate_projections"

18
19
20
21
22
23
24
25
26
27
28
29
30
31
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)


theory BuiltIn

  prelude "Require Import ZArith."
  prelude "Require Import Rbase."

  syntax type   int   "Z"
  syntax type   real  "R"
  syntax predicate  (=)   "(%1 = %2)"
end

32
theory Bool
33
34
35
36
37

  syntax type bool   "bool"

  syntax function True  "true"
  syntax function False "false"
38
39
40
end

theory bool.Bool
41
42
43
44
45

  syntax function andb  "(andb %1 %2)"
  syntax function orb   "(orb %1 %2)"
  syntax function xorb  "(xorb %1 %2)"
  syntax function notb  "(negb %1)"
46
  syntax function implb "(implb %1)"
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61

end


theory int.Int

  syntax function zero "0%Z"
  syntax function one  "1%Z"

  syntax function (+)  "(%1 + %2)%Z"
  syntax function (-)  "(%1 - %2)%Z"
  syntax function (*)  "(%1 * %2)%Z"
  syntax function (-_) "(-%1)%Z"

  syntax predicate (<=) "(%1 <= %2)%Z"
62
  syntax predicate (<)  "(%1 < %2)%Z"
63
  syntax predicate (>=) "(%1 >= %2)%Z"
64
  syntax predicate (>)  "(%1 > %2)%Z"
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
Andrei Paskevich's avatar
Andrei Paskevich committed
81
  remove prop ZeroLessOne
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

end

theory int.Abs

  syntax function abs "(Zabs %1)"

  remove prop Abs_pos

end

theory int.MinMax

  syntax function min "(Zmin %1 %2)"
  syntax function max "(Zmax %1 %2)"

end

(* removed: Coq Zdiv is NOT true Euclidean division:
   Zmod can be negative, in fact (Zmod x y) has the same sign as y,
102
   which is not the usual convention of programming language either.
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

theory int.EuclideanDivision

  prelude "Require Import Zdiv."

  syntax function div "(Zdiv %1 %2)"
  syntax function mod "(Zmod %1 %2)"

  remove prop Div_mod
  remove prop Div_bound
  remove prop Mod_bound
  remove prop Mod_1
  remove prop Div_1

end
*)

theory int.ComputerDivision

  (* Coq Z0div provides the division and modulo operators
     with the same convention as mainstream programming language
     such C, Java, OCaml *)

  prelude "Require Import ZOdiv."

  syntax function div "(ZOdiv %1 %2)"
  syntax function mod "(ZOmod %1 %2)"

  remove prop Div_mod
  remove prop Div_bound
  remove prop Mod_bound
  remove prop Div_sign_pos
  remove prop Div_sign_neg
  remove prop Mod_sign_pos
  remove prop Mod_sign_neg
  remove prop Rounds_toward_zero
  remove prop Div_1
  remove prop Mod_1
  remove prop Div_inf
  remove prop Mod_inf
  remove prop Div_mult
  remove prop Mod_mult

end


theory real.Real

  syntax function zero "0%R"
  syntax function one  "1%R"

  syntax function (+)  "(%1 + %2)%R"
  syntax function (-)  "(%1 - %2)%R"
  syntax function (-_) "(-%1)%R"
  syntax function (*)  "(%1 * %2)%R"
  syntax function (/)  "(Rdiv %1 %2)%R"
  syntax function inv  "(Rinv %1)"

  syntax predicate (<=) "(%1 <= %2)%R"
162
  syntax predicate (<)  "(%1 < %2)%R"
163
  syntax predicate (>=) "(%1 >= %2)%R"
164
  syntax predicate (>)  "(%1 > %2)%R"
165
166
167
168
169
170
171
172
173
174
175
176
177

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
Andrei Paskevich's avatar
Andrei Paskevich committed
178
  remove prop ZeroLessOne
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div

end

theory real.RealInfix

  syntax function (+.)  "(%1 + %2)%R"
  syntax function (-.)  "(%1 - %2)%R"
  syntax function (-._) "(-%1)%R"
  syntax function ( *.) "(%1 * %2)%R"
  syntax function (/.)  "(%1 / %2)%R"

  syntax predicate (<=.) "(%1 <= %2)%R"
  syntax predicate (<.)  "(%1 <  %2)%R"
  syntax predicate (>=.) "(%1 >= %2)%R"
  syntax predicate (>.)  "(%1 >  %2)%R"

end

theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax function abs "(Rabs %1)"

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

  syntax function from_int "(IZR %1)"

  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

end

theory real.Square

  prelude "Require Import R_sqrt."

  syntax function sqr  "(Rsqr %1)"
  syntax function sqrt "(sqrt %1)"  (* and not Rsqrt *)

  remove prop Sqrt_positive
  remove prop Sqrt_square
  remove prop Square_sqrt

end


theory real.ExpLog

  prelude "Require Import Rtrigo_def."
  prelude "Require Import Rpower."

  syntax function exp "(exp %1)"
  syntax function log "(ln %1)"

  remove prop Exp_zero
  remove prop Exp_sum
  remove prop Log_one
  remove prop Log_mul
  remove prop Log_exp
  remove prop Exp_log

end


260
theory real.PowerInt
261

262
  prelude "Require Import Rfunctions."
263

264
265
266
267
268
269
270
271
  syntax function power "(powerRZ %1 %2)"

  remove prop Power_0 (* already as powerRZ_O *)
  (* remove prop Power_s *)
  remove prop Power_1 (* already as powerRZ_1 *)
  (* remove prop Power_sum *) (* not the same as powerRZ_add *)
  (* remove prop Power_mult *)

272
273
274
275
276
277
278

end

theory real.PowerReal

  prelude "Require Import Rpower."

279
  syntax function pow "(Rpower %1 %2)"
280

281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
end

theory real.Trigonometry

  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"

  syntax function cos "(Rtrigo_def.cos %1)"
  syntax function sin "(Rtrigo_def.sin %1)"

  syntax function pi "PI"

  syntax function tan "(Rtrigo.tan %1)"
  (* syntax function atan "atan not defined in Coq ?" *)

  remove prop Pythagorean_identity
  remove prop Cos_le_one
  remove prop Sin_le_one
  remove prop Cos_0
  remove prop Sin_0
  remove prop Cos_pi
  remove prop Sin_pi
  remove prop Cos_pi2
  remove prop Sin_pi2

end
307
308
309

(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "coq-realizations.aux"