drivers/coq-common.gen

   1
   2 valid 0
   3 unknown "Error: \\(.*\\)$" "\\1"
   4 fail "Syntax error: \\(.*\\)$" "\\1"
   5 time "why3cpulimit time : %s s"
   6
   7 transformation "eliminate_non_struct_recursion"
   8 transformation "eliminate_if"
   9 transformation "eliminate_literal"
  10 transformation "eliminate_non_lambda_set_epsilon"
  11
  12 transformation "eliminate_projections"
  13
  14 transformation "simplify_formula"
  15 (*transformation "simplify_trivial_quantification_in_goal"*)
  16
  17
  18 theory BuiltIn
  19
  20   prelude "Require Import BuiltIn."
  21
  22   syntax type int "Numbers.BinNums.Z"
  23   syntax type real "Reals.Rdefinitions.R"
  24   syntax predicate  (=)   "(%1 = %2)"
  25 end
  26
  27 theory Ignore
  28   syntax predicate ignore'term  "true"
  29 end
  30
  31 theory Unit
  32   syntax type unit "Init.Datatypes.unit"
  33 end
  34
  35 theory Bool
  36
  37   syntax type bool "Init.Datatypes.bool"
  38
  39   syntax function True  "Init.Datatypes.true"
  40   syntax function False "Init.Datatypes.false"
  41 end
  42
  43 theory bool.Bool
  44
  45   syntax function andb  "Init.Datatypes.andb"
  46   syntax function orb   "Init.Datatypes.orb"
  47   syntax function xorb  "Init.Datatypes.xorb"
  48   syntax function notb  "Init.Datatypes.negb"
  49   syntax function implb "Init.Datatypes.implb"
  50
  51 end
  52
  53
  54 theory int.Int
  55
  56   syntax function zero "0%Z"
  57   syntax function one  "1%Z"
  58
  59   syntax function (+)  "(%1 + %2)%Z"
  60   syntax function (-)  "(%1 - %2)%Z"
  61   syntax function (*)  "(%1 * %2)%Z"
  62   syntax function (-_) "(-%1)%Z"
  63
  64   syntax predicate (<=) "(%1 <= %2)%Z"
  65   syntax predicate (<)  "(%1 < %2)%Z"
  66   syntax predicate (>=) "(%1 >= %2)%Z"
  67   syntax predicate (>)  "(%1 > %2)%Z"
  68
  69   remove prop MulComm.Comm
  70   remove prop MulAssoc.Assoc
  71   remove prop Unit_def_l
  72   remove prop Unit_def_r
  73   remove prop Inv_def_l
  74   remove prop Inv_def_r
  75   remove prop Assoc
  76   remove prop Mul_distr_l
  77   remove prop Mul_distr_r
  78   remove prop Comm
  79   remove prop Unitary
  80   remove prop Refl
  81   remove prop Trans
  82   remove prop Antisymm
  83   remove prop Total
  84   remove prop NonTrivialRing
  85   remove prop CompatOrderAdd
  86   remove prop CompatOrderMult
  87   remove prop ZeroLessOne
  88
  89 end
  90
  91 theory int.Abs
  92
  93   syntax function abs "ZArith.BinInt.Z.abs"
  94
  95   remove prop Abs_pos
  96
  97 end
  98
  99 theory int.MinMax
 100
 101   syntax function min "ZArith.BinInt.Z.min"
 102   syntax function max "ZArith.BinInt.Z.max"
 103
 104 end
 105
 106 (* removed: Coq Zdiv is NOT true Euclidean division:
 107    Zmod can be negative, in fact (Zmod x y) has the same sign as y,
 108    which is not the usual convention of programming language either.
 109
 110 theory int.EuclideanDivision
 111
 112   syntax function div "ZArith.BinInt.Z.div"
 113   syntax function mod "ZArith.BinInt.Z.modulo"
 114
 115   remove prop Div_mod
 116   remove prop Div_bound
 117   remove prop Mod_bound
 118   remove prop Mod_1
 119   remove prop Div_1
 120
 121 end
 122 *)
 123
 124 theory int.ComputerDivision
 125
 126   (* Coq provides the division and modulo operators
 127      with the same convention as mainstream programming language
 128      such C, Java, OCaml *)
 129
 130   syntax function div "ZArith.BinInt.Z.quot"
 131   syntax function mod "ZArith.BinInt.Z.rem"
 132
 133   remove prop Div_mod
 134   remove prop Div_bound
 135   remove prop Mod_bound
 136   remove prop Div_sign_pos
 137   remove prop Div_sign_neg
 138   remove prop Mod_sign_pos
 139   remove prop Mod_sign_neg
 140   remove prop Rounds_toward_zero
 141   remove prop Div_1
 142   remove prop Mod_1
 143   remove prop Div_inf
 144   remove prop Mod_inf
 145   remove prop Div_mult
 146   remove prop Mod_mult
 147
 148 end
 149
 150
 151 theory real.Real
 152
 153   syntax function zero "0%R"
 154   syntax function one  "1%R"
 155
 156   syntax function (+)  "(%1 + %2)%R"
 157   syntax function (-)  "(%1 - %2)%R"
 158   syntax function (-_) "(-%1)%R"
 159   syntax function (*)  "(%1 * %2)%R"
 160   syntax function (/)  "(%1 / %2)%R"
 161   syntax function inv  "(/ %1)%R"
 162
 163   syntax predicate (<=) "(%1 <= %2)%R"
 164   syntax predicate (<)  "(%1 < %2)%R"
 165   syntax predicate (>=) "(%1 >= %2)%R"
 166   syntax predicate (>)  "(%1 > %2)%R"
 167
 168   remove prop MulComm.Comm
 169   remove prop MulAssoc.Assoc
 170   remove prop Unit_def_l
 171   remove prop Unit_def_r
 172   remove prop Inv_def_l
 173   remove prop Inv_def_r
 174   remove prop Assoc
 175   remove prop Mul_distr_l
 176   remove prop Mul_distr_r
 177   remove prop Comm
 178   remove prop Unitary
 179   remove prop Inverse
 180   remove prop NonTrivialRing
 181   remove prop CompatOrderAdd
 182   remove prop CompatOrderMult
 183   remove prop ZeroLessOne
 184   remove prop Refl
 185   remove prop Trans
 186   remove prop Antisymm
 187   remove prop Total
 188   remove prop assoc_mul_div
 189   remove prop assoc_div_mul
 190   remove prop assoc_div_div
 191
 192 end
 193
 194 theory real.RealInfix
 195
 196   syntax function (+.)  "(%1 + %2)%R"
 197   syntax function (-.)  "(%1 - %2)%R"
 198   syntax function (-._) "(-%1)%R"
 199   syntax function ( *.) "(%1 * %2)%R"
 200   syntax function (/.)  "(%1 / %2)%R"
 201
 202   syntax predicate (<=.) "(%1 <= %2)%R"
 203   syntax predicate (<.)  "(%1 <  %2)%R"
 204   syntax predicate (>=.) "(%1 >= %2)%R"
 205   syntax predicate (>.)  "(%1 >  %2)%R"
 206
 207 end
 208
 209 theory real.Abs
 210
 211   prelude "Require Reals.Rbasic_fun."
 212
 213   syntax function abs "Reals.Rbasic_fun.Rabs"
 214
 215   remove prop Abs_le
 216   remove prop Abs_pos
 217
 218 end
 219
 220 theory real.MinMax
 221
 222   syntax function min "Reals.Rbasic_fun.Rmin"
 223   syntax function max "Reals.Rbasic_fun.Rmax"
 224
 225 end
 226
 227 theory real.FromInt
 228
 229   syntax function from_int "BuiltIn.IZR"
 230
 231   remove prop Zero
 232   remove prop One
 233   remove prop Add
 234   remove prop Sub
 235   remove prop Mul
 236   remove prop Neg
 237
 238 end
 239
 240 theory real.Square
 241
 242   prelude "Require Reals.R_sqrt."
 243
 244   syntax function sqr  "Reals.RIneq.Rsqr"
 245   syntax function sqrt "Reals.R_sqrt.sqrt"  (* and not Rsqrt *)
 246
 247   remove prop Sqrt_positive
 248   remove prop Sqrt_square
 249   remove prop Square_sqrt
 250
 251 end
 252
 253 theory real.ExpLog
 254
 255   prelude "Require Reals.Rtrigo_def."
 256   prelude "Require Reals.Rpower."
 257
 258   syntax function exp "Reals.Rtrigo_def.exp"
 259   syntax function log "Reals.Rpower.ln"
 260
 261   remove prop Exp_zero
 262   remove prop Exp_sum
 263   remove prop Log_one
 264   remove prop Log_mul
 265   remove prop Log_exp
 266   remove prop Exp_log
 267
 268 end
 269
 270 theory real.PowerInt
 271
 272   prelude "Require Reals.Rfunctions."
 273
 274   syntax function power "Reals.Rfunctions.powerRZ"
 275
 276   remove prop Power_0 (* already as powerRZ_O *)
 277   (* remove prop Power_s *)
 278   remove prop Power_1 (* already as powerRZ_1 *)
 279   (* remove prop Power_sum *) (* not the same as powerRZ_add *)
 280   (* remove prop Power_mult *)
 281
 282 end
 283
 284 theory real.PowerReal
 285
 286   syntax function pow "Reals.Rpower.Rpower"
 287
 288 end
 289
 290 theory real.Trigonometry
 291
 292   prelude "Require Reals.Rtrigo_def."
 293   prelude "Require Reals.Rtrigo1."
 294   prelude "Require Reals.Ratan."
 295
 296   syntax function cos "Reals.Rtrigo_def.cos"
 297   syntax function sin "Reals.Rtrigo_def.sin"
 298
 299   syntax function pi "Reals.Rtrigo1.PI"
 300
 301   syntax function tan "Reals.Rtrigo1.tan"
 302
 303   syntax function atan "Reals.Ratan.atan"
 304
 305   remove prop Pythagorean_identity
 306   remove prop Cos_le_one
 307   remove prop Sin_le_one
 308   remove prop Cos_0
 309   remove prop Sin_0
 310   remove prop Cos_pi
 311   remove prop Sin_pi
 312   remove prop Cos_pi2
 313   remove prop Sin_pi2
 314
 315 end
 316
 317 theory list.List
 318
 319   syntax type list "Init.Datatypes.list"
 320   syntax function Nil "Init.Datatypes.nil"
 321   syntax function Cons "Init.Datatypes.cons"
 322
 323 end
 324
 325 theory list.Append
 326
 327   syntax function (++) "Init.Datatypes.app"
 328
 329 end
 330
 331 theory list.Reverse
 332
 333   syntax function reverse "Lists.List.rev"
 334
 335 end
 336
 337 theory list.RevAppend
 338
 339   syntax function rev_append "Lists.List.rev_append"
 340
 341 end
 342
 343 theory list.Combine
 344
 345   syntax function combine "Lists.List.combine"
 346
 347 end
 348
 349 theory option.Option
 350
 351   syntax type option "Init.Datatypes.option"
 352   syntax function None "Init.Datatypes.None"
 353   syntax function Some "Init.Datatypes.Some"
 354
 355 end
 356
 357 (* this file has an extension .aux rather than .gen since it should not be distributed *)
 358 import "coq-realizations.aux"