coq-common.gen 7.1 KB
Newer Older
1 2 3 4 5 6 7 8

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

transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
Clément Fumex's avatar
Clément Fumex committed
9
transformation "eliminate_literal"
10
transformation "eliminate_non_lambda_set_epsilon"
11

12 13
transformation "eliminate_projections"

14 15 16 17 18 19
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)


theory BuiltIn

20
  prelude "Require Import BuiltIn."
21

22 23
  syntax type int "Numbers.BinNums.Z"
  syntax type real "Reals.Rdefinitions.R"
24 25 26
  syntax predicate  (=)   "(%1 = %2)"
end

27 28

theory Unit
29
  syntax type unit "Init.Datatypes.unit"
30 31
end

32
theory Bool
33

34
  syntax type bool "Init.Datatypes.bool"
35

36 37
  syntax function True  "Init.Datatypes.true"
  syntax function False "Init.Datatypes.false"
38 39 40
end

theory bool.Bool
41

42 43 44 45 46
  syntax function andb  "Init.Datatypes.andb"
  syntax function orb   "Init.Datatypes.orb"
  syntax function xorb  "Init.Datatypes.xorb"
  syntax function notb  "Init.Datatypes.negb"
  syntax function implb "Init.Datatypes.implb"
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
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
73 74
  remove prop Mul_distr_l
  remove prop Mul_distr_r
75
  remove prop Comm
76 77 78 79 80 81 82 83
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
84
  remove prop ZeroLessOne
85 86 87 88 89

end

theory int.Abs

90
  syntax function abs "ZArith.BinInt.Z.abs"
91 92 93 94 95 96 97

  remove prop Abs_pos

end

theory int.MinMax

98 99
  syntax function min "ZArith.BinInt.Z.min"
  syntax function max "ZArith.BinInt.Z.max"
100 101 102 103 104

end

(* removed: Coq Zdiv is NOT true Euclidean division:
   Zmod can be negative, in fact (Zmod x y) has the same sign as y,
105
   which is not the usual convention of programming language either.
106 107 108

theory int.EuclideanDivision

109 110
  syntax function div "ZArith.BinInt.Z.div"
  syntax function mod "ZArith.BinInt.Z.modulo"
111 112 113 114 115 116 117 118 119 120 121 122

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

end
*)

theory int.ComputerDivision

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

127 128
  syntax function div "ZArith.BinInt.Z.quot"
  syntax function mod "ZArith.BinInt.Z.rem"
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

  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"
157
  syntax function (/)  "(%1 / %2)%R"
158
  syntax function inv  "(/ %1)%R"
159 160

  syntax predicate (<=) "(%1 <= %2)%R"
161
  syntax predicate (<)  "(%1 < %2)%R"
162
  syntax predicate (>=) "(%1 >= %2)%R"
163
  syntax predicate (>)  "(%1 > %2)%R"
164

165 166 167 168 169 170 171
  remove prop MulComm.Comm
  remove prop MulAssoc.Assoc
  remove prop Unit_def_l
  remove prop Unit_def_r
  remove prop Inv_def_l
  remove prop Inv_def_r
  remove prop Assoc
172 173
  remove prop Mul_distr_l
  remove prop Mul_distr_r
174
  remove prop Comm
175 176 177 178 179
  remove prop Unitary
  remove prop Inverse
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
180
  remove prop ZeroLessOne
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
  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

208
  prelude "Require Reals.Rbasic_fun."
209

210
  syntax function abs "Reals.Rbasic_fun.Rabs"
211 212 213 214 215 216

  remove prop Abs_le
  remove prop Abs_pos

end

217 218
theory real.MinMax

219 220
  syntax function min "Reals.Rbasic_fun.Rmin"
  syntax function max "Reals.Rbasic_fun.Rmax"
221 222 223

end

224 225
theory real.FromInt

226
  syntax function from_int "BuiltIn.IZR"
227 228 229 230 231 232 233 234 235 236 237 238

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

end

theory real.Square

239
  prelude "Require Reals.R_sqrt."
240

241 242
  syntax function sqr  "Reals.RIneq.Rsqr"
  syntax function sqrt "Reals.R_sqrt.sqrt"  (* and not Rsqrt *)
243 244 245 246 247 248 249 250 251

  remove prop Sqrt_positive
  remove prop Sqrt_square
  remove prop Square_sqrt

end

theory real.ExpLog

252 253
  prelude "Require Reals.Rtrigo_def."
  prelude "Require Reals.Rpower."
254

255 256
  syntax function exp "Reals.Rtrigo_def.exp"
  syntax function log "Reals.Rpower.ln"
257 258 259 260 261 262 263 264 265 266

  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

267
theory real.PowerInt
268

269
  prelude "Require Reals.Rfunctions."
270

271
  syntax function power "Reals.Rfunctions.powerRZ"
272 273 274 275 276 277 278

  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 *)

279 280
end

Guillaume Melquiond's avatar
Guillaume Melquiond committed
281 282
theory real.PowerReal

283
  syntax function pow "Reals.Rpower.Rpower"
Guillaume Melquiond's avatar
Guillaume Melquiond committed
284 285 286

end

287 288 289 290 291 292
theory real.Trigonometry

  prelude "Require Reals.Rtrigo_def."
  prelude "Require Reals.Rtrigo1."
  prelude "Require Reals.Ratan."

293 294
  syntax function cos "Reals.Rtrigo_def.cos"
  syntax function sin "Reals.Rtrigo_def.sin"
295 296 297

  syntax function pi "Reals.Rtrigo1.PI"

298
  syntax function tan "Reals.Rtrigo1.tan"
299

300
  syntax function atan "Reals.Ratan.atan"
301 302 303 304 305 306 307 308 309 310 311 312 313

  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

314 315
theory list.List

316
  syntax type list "Init.Datatypes.list"
317
  syntax function Nil "Init.Datatypes.nil"
318
  syntax function Cons "Init.Datatypes.cons"
319 320 321

end

322 323
theory list.Append

324
  syntax function (++) "Init.Datatypes.app"
325 326 327

end

328 329
theory list.Reverse

330
  syntax function reverse "Lists.List.rev"
331 332 333

end

334 335
theory list.RevAppend

336
  syntax function rev_append "Lists.List.rev_append"
337 338 339

end

340 341
theory list.Combine

342
  syntax function combine "Lists.List.combine"
343 344 345

end

346 347
theory option.Option

348
  syntax type option "Init.Datatypes.option"
349
  syntax function None "Init.Datatypes.None"
350
  syntax function Some "Init.Datatypes.Some"
351 352 353

end

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