coq-common.gen 6.38 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"

10
transformation "eliminate_epsilon"
11 12
transformation "eliminate_if"

13 14
transformation "eliminate_projections"

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


theory BuiltIn

21
  prelude "Require Import BuiltIn."
22

23 24
  syntax type int "Z"
  syntax type real "R"
25 26 27
  syntax predicate  (=)   "(%1 = %2)"
end

28
theory Bool
29 30 31 32 33

  syntax type bool   "bool"

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

theory bool.Bool
37

38 39 40 41 42
  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)"
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57

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

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

end

theory int.Abs

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

  remove prop Abs_pos

end

theory int.MinMax

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

end

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

theory int.EuclideanDivision

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

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

end
*)

theory int.ComputerDivision

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

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

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

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

  remove prop CommutativeGroup.Comm.Comm
162 163 164 165 166
  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
167
  remove prop Assoc.Assoc
168 169
  remove prop Mul_distr_l
  remove prop Mul_distr_r
170 171 172 173 174 175
  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
176
  remove prop ZeroLessOne
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 203
  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

204
  prelude "Require Reals.Rbasic_fun."
205

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

  remove prop Abs_le
  remove prop Abs_pos

end

theory real.FromInt

215
  syntax function from_int "(Reals.Raxioms.IZR %1)"
216 217 218 219 220 221 222 223 224 225 226 227

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

end

theory real.Square

228
  prelude "Require Reals.R_sqrt."
229

230 231
  syntax function sqr  "(Reals.RIneq.Rsqr %1)"
  syntax function sqrt "(Reals.R_sqrt.sqrt %1)"  (* and not Rsqrt *)
232 233 234 235 236 237 238 239 240

  remove prop Sqrt_positive
  remove prop Sqrt_square
  remove prop Square_sqrt

end

theory real.ExpLog

241 242
  prelude "Require Reals.Rtrigo_def."
  prelude "Require Reals.Rpower."
243

244 245
  syntax function exp "(Reals.Rtrigo_def.exp %1)"
  syntax function log "(Reals.Rpower.ln %1)"
246 247 248 249 250 251 252 253 254 255

  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

256
theory real.PowerInt
257

258
  prelude "Require Reals.Rfunctions."
259

260
  syntax function power "(Reals.Rfunctions.powerRZ %1 %2)"
261 262 263 264 265 266 267

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

268 269
end

270 271
theory list.List

272
  syntax type list "(list %1)"
273 274
  syntax function Nil "Init.Datatypes.nil"
  syntax function Cons "(Init.Datatypes.cons %1 %2)"
275 276 277

end

278 279 280 281 282 283
theory list.Append

  syntax function (++) "(List.app %1 %2)"

end

284 285 286 287 288 289
theory list.Reverse

  syntax function reverse "(List.rev %1)"

end

290 291
theory option.Option

292
  syntax type option "(option %1)"
293 294
  syntax function None "Init.Datatypes.None"
  syntax function Some "(Init.Datatypes.Some %1)"
295 296 297

end

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