coq.drv 4.58 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

end

90 91
theory int.MinMax

92 93
  syntax function min "(Zmin %1 %2)"
  syntax function max "(Zmax %1 %2)"
94 95 96

end

97 98
theory int.EuclideanDivision

MARCHE Claude's avatar
MARCHE Claude committed
99
  prelude "Require Import Zdiv."
100

101 102
  syntax function div "(Zdiv %1 %2)"
  syntax function mod "(Zmod %1 %2)"
103 104 105 106 107

end

theory int.ComputerDivision

MARCHE Claude's avatar
MARCHE Claude committed
108
  prelude "Require Import ZOdiv."
109

110 111
  syntax function div "(ZOdiv %1 %2)"
  syntax function mod "(ZOmod %1 %2)"
112 113 114 115

end


MARCHE Claude's avatar
MARCHE Claude committed
116 117
theory real.Real

118 119
  syntax function zero "0%R"
  syntax function one  "1%R"
MARCHE Claude's avatar
MARCHE Claude committed
120

121 122 123 124 125 126
  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
127

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

  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
142 143 144
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
145 146 147 148
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
MARCHE Claude's avatar
MARCHE Claude committed
149 150 151

end

MARCHE Claude's avatar
MARCHE Claude committed
152 153
theory real.RealInfix

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 (/.)  "(%1 / %2)%R"
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

end
MARCHE Claude's avatar
MARCHE Claude committed
166 167 168 169 170

theory real.Abs

  prelude "Require Import Rbasic_fun."

171
  syntax function abs "(Rabs %1)"
MARCHE Claude's avatar
MARCHE Claude committed
172

173 174
  remove prop Abs_pos

MARCHE Claude's avatar
MARCHE Claude committed
175 176
end

MARCHE Claude's avatar
MARCHE Claude committed
177 178
theory real.FromInt

179
  syntax function from_int "(IZR %1)"
MARCHE Claude's avatar
MARCHE Claude committed
180 181 182

end

MARCHE Claude's avatar
MARCHE Claude committed
183 184 185 186
theory real.Square

  prelude "Require Import R_sqrt."

187 188
  syntax function sqr  "(Rsqr %1)"
  syntax function sqrt "(sqrt %1)"  (* and not Rsqrt *)
MARCHE Claude's avatar
MARCHE Claude committed
189 190 191 192 193 194 195 196 197

end


theory real.ExpLog

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

198 199
  syntax function exp "(exp %1)"
  syntax function log "(ln %1)"
MARCHE Claude's avatar
MARCHE Claude committed
200

201 202 203 204 205 206 207
  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
208 209 210
end


211
theory real.Power
MARCHE Claude's avatar
MARCHE Claude committed
212 213 214 215 216 217 218 219

  prelude "Require Import Rpower."

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

theory real.Trigonometry

220 221
  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"
MARCHE Claude's avatar
MARCHE Claude committed
222

223 224
  syntax function cos "(Rtrigo_def.cos %1)"
  syntax function sin "(Rtrigo_def.sin %1)"
MARCHE Claude's avatar
MARCHE Claude committed
225

226
  syntax function pi "PI"
MARCHE Claude's avatar
MARCHE Claude committed
227

228 229
  syntax function tan "(Rtrigo.tan %1)"
  (* syntax function atan "atan not defined in Coq ?" *)
MARCHE Claude's avatar
MARCHE Claude committed
230 231

end