coq.drv 5.88 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2

printer "coq"
3
filename "%f_%t_%g.v"
MARCHE Claude's avatar
MARCHE Claude committed
4

MARCHE Claude's avatar
MARCHE Claude committed
5
valid 0
6 7
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
8
time "why3cpulimit time : %s s"
9

10
prelude "(* This file is generated by Why3's Coq driver *)"
11
prelude "(* Beware! Only edit allowed sections below    *)"
MARCHE Claude's avatar
MARCHE Claude committed
12

MARCHE Claude's avatar
MARCHE Claude committed
13
(* À discuter *)
14
(*transformation "simplify_recursive_definition"*)
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17
transformation "inline_trivial"

transformation "eliminate_builtin"
18
transformation "eliminate_non_struct_recursion"
MARCHE Claude's avatar
MARCHE Claude committed
19

20 21
transformation "eliminate_if"

MARCHE Claude's avatar
MARCHE Claude committed
22
transformation "simplify_formula"
23
(*transformation "simplify_trivial_quantification_in_goal"*)
MARCHE Claude's avatar
MARCHE Claude committed
24 25


MARCHE Claude's avatar
MARCHE Claude committed
26
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30

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

31 32
  syntax type   int   "Z"
  syntax type   real  "R"
33
  syntax predicate  (=)   "(%1 = %2)"
MARCHE Claude's avatar
MARCHE Claude committed
34 35
end

MARCHE Claude's avatar
MARCHE Claude committed
36 37
theory bool.Bool

38
  syntax type bool   "bool"
MARCHE Claude's avatar
MARCHE Claude committed
39

40 41
  syntax function True  "true"
  syntax function False "false"
MARCHE Claude's avatar
MARCHE Claude committed
42

43 44 45 46
  syntax function andb  "(andb %1 %2)"
  syntax function orb   "(orb %1 %2)"
  syntax function xorb  "(xorb %1 %2)"
  syntax function notb  "(negb %1)"
MARCHE Claude's avatar
MARCHE Claude committed
47 48 49

end

MARCHE Claude's avatar
MARCHE Claude committed
50 51 52

theory int.Int

53 54
  syntax function zero "0%Z"
  syntax function one  "1%Z"
MARCHE Claude's avatar
MARCHE Claude committed
55

56 57 58 59
  syntax function (+)  "(%1 + %2)%Z"
  syntax function (-)  "(%1 - %2)%Z"
  syntax function (*)  "(%1 * %2)%Z"
  syntax function (-_) "(-%1)%Z"
MARCHE Claude's avatar
MARCHE Claude committed
60

61 62 63 64
  syntax predicate (<=) "(%1 <= %2)%Z"
  syntax predicate (<)  "(%1 <  %2)%Z"
  syntax predicate (>=) "(%1 >= %2)%Z"
  syntax predicate (>)  "(%1 >  %2)%Z"
MARCHE Claude's avatar
MARCHE Claude committed
65 66 67 68 69 70 71 72 73

  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
74 75 76 77
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
78 79 80 81
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult

MARCHE Claude's avatar
MARCHE Claude committed
82 83
end

MARCHE Claude's avatar
MARCHE Claude committed
84 85
theory int.Abs

86
  syntax function abs "(Zabs %1)"
MARCHE Claude's avatar
MARCHE Claude committed
87

88 89
  remove prop Abs_pos

MARCHE Claude's avatar
MARCHE Claude committed
90 91
end

92 93
theory int.MinMax

94 95
  syntax function min "(Zmin %1 %2)"
  syntax function max "(Zmax %1 %2)"
96 97 98

end

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

103 104
theory int.EuclideanDivision

MARCHE Claude's avatar
MARCHE Claude committed
105
  prelude "Require Import Zdiv."
106

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

110 111 112 113 114 115
  remove prop Div_mod
  remove prop Div_bound
  remove prop Mod_bound
  remove prop Mod_1
  remove prop Div_1

116
end
117
*)
118 119 120

theory int.ComputerDivision

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

MARCHE Claude's avatar
MARCHE Claude committed
125
  prelude "Require Import ZOdiv."
126

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

130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
  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

145 146 147
end


MARCHE Claude's avatar
MARCHE Claude committed
148 149
theory real.Real

150 151
  syntax function zero "0%R"
  syntax function one  "1%R"
MARCHE Claude's avatar
MARCHE Claude committed
152

153 154 155 156 157 158
  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)"
MARCHE Claude's avatar
MARCHE Claude committed
159

160 161 162 163
  syntax predicate (<=) "(%1 <= %2)%R"
  syntax predicate (<)  "(%1 <  %2)%R"
  syntax predicate (>=) "(%1 >= %2)%R"
  syntax predicate (>)  "(%1 >  %2)%R"
MARCHE Claude's avatar
MARCHE Claude committed
164 165 166 167 168 169 170 171 172 173

  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
174 175 176
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
177 178 179 180
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
181 182 183
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div
MARCHE Claude's avatar
MARCHE Claude committed
184 185 186

end

MARCHE Claude's avatar
MARCHE Claude committed
187 188
theory real.RealInfix

189 190 191 192 193
  syntax function (+.)  "(%1 + %2)%R"
  syntax function (-.)  "(%1 - %2)%R"
  syntax function (-._) "(-%1)%R"
  syntax function ( *.) "(%1 * %2)%R"
  syntax function (/.)  "(%1 / %2)%R"
MARCHE Claude's avatar
MARCHE Claude committed
194

195 196 197 198
  syntax predicate (<=.) "(%1 <= %2)%R"
  syntax predicate (<.)  "(%1 <  %2)%R"
  syntax predicate (>=.) "(%1 >= %2)%R"
  syntax predicate (>.)  "(%1 >  %2)%R"
MARCHE Claude's avatar
MARCHE Claude committed
199 200

end
MARCHE Claude's avatar
MARCHE Claude committed
201 202 203 204 205

theory real.Abs

  prelude "Require Import Rbasic_fun."

206
  syntax function abs "(Rabs %1)"
MARCHE Claude's avatar
MARCHE Claude committed
207

208
  remove prop Abs_le
209 210
  remove prop Abs_pos

MARCHE Claude's avatar
MARCHE Claude committed
211 212
end

MARCHE Claude's avatar
MARCHE Claude committed
213 214
theory real.FromInt

215
  syntax function from_int "(IZR %1)"
MARCHE Claude's avatar
MARCHE Claude committed
216

217 218 219 220 221 222 223
  remove prop Zero
  remove prop One
  remove prop Add
  remove prop Sub
  remove prop Mul
  remove prop Neg

MARCHE Claude's avatar
MARCHE Claude committed
224 225
end

MARCHE Claude's avatar
MARCHE Claude committed
226 227 228 229
theory real.Square

  prelude "Require Import R_sqrt."

230 231
  syntax function sqr  "(Rsqr %1)"
  syntax function sqrt "(sqrt %1)"  (* and not Rsqrt *)
MARCHE Claude's avatar
MARCHE Claude committed
232

233 234 235 236
  remove prop Sqrt_positive
  remove prop Sqrt_square
  remove prop Square_sqrt

MARCHE Claude's avatar
MARCHE Claude committed
237 238 239 240 241 242 243 244
end


theory real.ExpLog

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

245 246
  syntax function exp "(exp %1)"
  syntax function log "(ln %1)"
MARCHE Claude's avatar
MARCHE Claude committed
247

248 249 250 251 252 253 254
  remove prop Exp_zero
  remove prop Exp_sum
  remove prop Log_one
  remove prop Log_mul
  remove prop Log_exp
  remove prop Exp_log

MARCHE Claude's avatar
MARCHE Claude committed
255 256 257
end


258
theory real.Power
MARCHE Claude's avatar
MARCHE Claude committed
259 260 261 262 263 264 265 266

  prelude "Require Import Rpower."

  (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
end

theory real.Trigonometry

267 268
  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"
MARCHE Claude's avatar
MARCHE Claude committed
269

270 271
  syntax function cos "(Rtrigo_def.cos %1)"
  syntax function sin "(Rtrigo_def.sin %1)"
MARCHE Claude's avatar
MARCHE Claude committed
272

273
  syntax function pi "PI"
MARCHE Claude's avatar
MARCHE Claude committed
274

275 276
  syntax function tan "(Rtrigo.tan %1)"
  (* syntax function atan "atan not defined in Coq ?" *)
MARCHE Claude's avatar
MARCHE Claude committed
277

278 279 280 281 282 283 284 285 286 287
  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

MARCHE Claude's avatar
MARCHE Claude committed
288
end