coq.drv 4.15 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 14 15 16 17 18 19
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"

20 21
transformation "eliminate_if"

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


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 logic  (=)   "(%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
  syntax logic True  "true"
MARCHE Claude's avatar
MARCHE Claude committed
41 42
  syntax logic False "false"

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

end

MARCHE Claude's avatar
MARCHE Claude committed
50 51 52 53

theory int.Int

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

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

61 62 63 64
  syntax logic (<=) "(%1 <= %2)%Z"
  syntax logic (<)  "(%1 <  %2)%Z"
  syntax logic (>=) "(%1 >= %2)%Z"
  syntax logic (>)  "(%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 86 87 88 89
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

90 91 92 93 94 95 96
theory int.MinMax

  syntax logic min "(Zmin %1 %2)"
  syntax logic max "(Zmax %1 %2)"

end

97 98
theory int.EuclideanDivision

MARCHE Claude's avatar
MARCHE Claude committed
99
  prelude "Require Import Zdiv."
100 101 102 103 104 105 106 107

  syntax logic div "(Zdiv %1 %2)"
  syntax logic mod "(Zmod %1 %2)"

end

theory int.ComputerDivision

MARCHE Claude's avatar
MARCHE Claude committed
108
  prelude "Require Import ZOdiv."
109 110 111 112 113 114 115

  syntax logic div "(ZOdiv %1 %2)"
  syntax logic mod "(ZOmod %1 %2)"

end


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

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

121 122 123 124 125
  syntax logic (+)  "(%1 + %2)%R"
  syntax logic (-)  "(%1 - %2)%R"
  syntax logic (-_) "(-%1)%R"
  syntax logic (*)  "(%1 * %2)%R"
  syntax logic (/)  "(Rdiv %1 %2)%R"
MARCHE Claude's avatar
MARCHE Claude committed
126 127
  syntax logic inv  "(Rinv %1)"

128 129 130 131
  syntax logic (<=) "(%1 <= %2)%R"
  syntax logic (<)  "(%1 <  %2)%R"
  syntax logic (>=) "(%1 >= %2)%R"
  syntax logic (>)  "(%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
MARCHE Claude's avatar
MARCHE Claude committed
145 146 147

end

MARCHE Claude's avatar
MARCHE Claude committed
148 149 150 151 152 153 154 155 156 157 158 159 160 161
theory real.RealInfix

  syntax logic (+.)  "(%1 + %2)%R"
  syntax logic (-.)  "(%1 - %2)%R"
  syntax logic (-._) "(-%1)%R"
  syntax logic ( *.)  "(%1 * %2)%R"
  syntax logic (/.)  "(Rdiv %1 %2)%R"

  syntax logic (<=.) "(%1 <= %2)%R"
  syntax logic (<.)  "(%1 <  %2)%R"
  syntax logic (>=.) "(%1 >= %2)%R"
  syntax logic (>.)  "(%1 >  %2)%R"

end
MARCHE Claude's avatar
MARCHE Claude committed
162 163 164 165 166 167 168 169 170

theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
171 172 173 174 175 176
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
177 178 179 180
theory real.Square

  prelude "Require Import R_sqrt."

181
  syntax logic sqr  "(Rsqr %1)"
MARCHE Claude's avatar
MARCHE Claude committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
  syntax logic sqrt "(sqrt %1)"  (* and not Rsqrt *)

end


theory real.ExpLog

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

  syntax logic exp "(exp %1)"
  syntax logic log "(ln %1)"

end


198
theory real.Power
MARCHE Claude's avatar
MARCHE Claude committed
199 200 201 202 203 204 205 206

  prelude "Require Import Rpower."

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

theory real.Trigonometry

207 208
  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"
MARCHE Claude's avatar
MARCHE Claude committed
209

210 211
  syntax logic cos "(Rtrigo_def.cos %1)"
  syntax logic sin "(Rtrigo_def.sin %1)"
MARCHE Claude's avatar
MARCHE Claude committed
212 213 214

  syntax logic pi "PI"

215
  syntax logic tan "(Rtrigo.tan %1)"
MARCHE Claude's avatar
MARCHE Claude committed
216 217 218
  (* syntax logic atan "atan not defined in Coq ?" *)

end