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

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

(* À discuter *)
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
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 "Z"
  syntax type real "R"
24 25 26
  syntax predicate  (=)   "(%1 = %2)"
end

27
theory Bool
28 29 30 31 32

  syntax type bool   "bool"

  syntax function True  "true"
  syntax function False "false"
33 34 35
end

theory bool.Bool
36

37 38 39 40 41
  syntax function andb  "(Init.Datatypes.andb %1 %2)"
  syntax function orb   "(Init.Datatypes.orb %1 %2)"
  syntax function xorb  "(Init.Datatypes.xorb %1 %2)"
  syntax function notb  "(Init.Datatypes.negb %1)"
  syntax function implb "(Init.Datatypes.implb %1 %2)"
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56

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"
57
  syntax predicate (<)  "(%1 < %2)%Z"
58
  syntax predicate (>=) "(%1 >= %2)%Z"
59
  syntax predicate (>)  "(%1 > %2)%Z"
60 61

  remove prop CommutativeGroup.Comm.Comm
62 63 64 65 66
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
67
  remove prop Assoc.Assoc
68 69
  remove prop Mul_distr_l
  remove prop Mul_distr_r
70 71 72 73 74 75 76 77 78
  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
79
  remove prop ZeroLessOne
80 81 82 83 84

end

theory int.Abs

85
  syntax function abs "(ZArith.BinInt.Z.abs %1)"
86 87 88 89 90 91 92

  remove prop Abs_pos

end

theory int.MinMax

93 94
  syntax function min "(ZArith.BinInt.Z.min %1 %2)"
  syntax function max "(ZArith.BinInt.Z.max %1 %2)"
95 96 97 98 99

end

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

theory int.EuclideanDivision

104 105
  syntax function div "(ZArith.BinInt.Z.div %1 %2)"
  syntax function mod "(ZArith.BinInt.Z.modulo %1 %2)"
106 107 108 109 110 111 112 113 114 115 116 117

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

end
*)

theory int.ComputerDivision

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

122 123
  syntax function div "(ZArith.BinInt.Z.quot %1 %2)"
  syntax function mod "(ZArith.BinInt.Z.rem %1 %2)"
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

  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"
152 153
  syntax function (/)  "(%1 / %2)%R"
  syntax function inv  "(Reals.Rdefinitions.Rinv %1)"
154 155

  syntax predicate (<=) "(%1 <= %2)%R"
156
  syntax predicate (<)  "(%1 < %2)%R"
157
  syntax predicate (>=) "(%1 >= %2)%R"
158
  syntax predicate (>)  "(%1 > %2)%R"
159 160

  remove prop CommutativeGroup.Comm.Comm
161 162 163 164 165
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
166
  remove prop Assoc.Assoc
167 168
  remove prop Mul_distr_l
  remove prop Mul_distr_r
169 170 171 172 173 174
  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
175
  remove prop ZeroLessOne
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
  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

203
  prelude "Require Reals.Rbasic_fun."
204

205
  syntax function abs "(Reals.Rbasic_fun.Rabs %1)"
206 207 208 209 210 211

  remove prop Abs_le
  remove prop Abs_pos

end

212 213 214 215 216 217 218
theory real.MinMax

  syntax function min "(Reals.Rbasic_fun.Rmin %1 %2)"
  syntax function max "(Reals.Rbasic_fun.Rmax %1 %2)"

end

219 220
theory real.FromInt

221
  syntax function from_int "(Reals.Raxioms.IZR %1)"
222 223 224 225 226 227 228 229 230 231 232 233

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

end

theory real.Square

234
  prelude "Require Reals.R_sqrt."
235

236 237
  syntax function sqr  "(Reals.RIneq.Rsqr %1)"
  syntax function sqrt "(Reals.R_sqrt.sqrt %1)"  (* and not Rsqrt *)
238 239 240 241 242 243 244 245 246

  remove prop Sqrt_positive
  remove prop Sqrt_square
  remove prop Square_sqrt

end

theory real.ExpLog

247 248
  prelude "Require Reals.Rtrigo_def."
  prelude "Require Reals.Rpower."
249

250 251
  syntax function exp "(Reals.Rtrigo_def.exp %1)"
  syntax function log "(Reals.Rpower.ln %1)"
252 253 254 255 256 257 258 259 260 261

  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

262
theory real.PowerInt
263

264
  prelude "Require Reals.Rfunctions."
265

266
  syntax function power "(Reals.Rfunctions.powerRZ %1 %2)"
267 268 269 270 271 272 273

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

274 275
end

276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
theory real.Trigonometry

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

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

  syntax function pi "Reals.Rtrigo1.PI"

  syntax function tan "(Reals.Rtrigo1.tan %1)"

  syntax function atan "(Reals.Ratan.atan %1)"

  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

303 304
theory list.List

305
  syntax type list "(list %1)"
306 307
  syntax function Nil "Init.Datatypes.nil"
  syntax function Cons "(Init.Datatypes.cons %1 %2)"
308 309 310

end

311 312
theory list.Append

313
  syntax function (++) "(Init.Datatypes.app %1 %2)"
314 315 316

end

317 318
theory list.Reverse

319
  syntax function reverse "(Lists.List.rev %1)"
320 321 322

end

323 324 325 326 327 328
theory list.RevAppend

  syntax function rev_append "(Lists.List.rev_append %1 %2)"

end

329 330 331 332 333 334
theory list.Combine

  syntax function combine "(Lists.List.combine %1 %2)"

end

335 336
theory option.Option

337
  syntax type option "(option %1)"
338 339
  syntax function None "Init.Datatypes.None"
  syntax function Some "(Init.Datatypes.Some %1)"
340 341 342

end

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