coq.drv 4.12 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 8
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"

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

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

transformation "eliminate_builtin"
transformation "eliminate_recursion"

19 20
transformation "eliminate_if"

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


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

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

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

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

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

39
  syntax logic True  "true"
MARCHE Claude's avatar
MARCHE Claude committed
40 41
  syntax logic False "false"

42 43 44 45
  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
46 47 48

end

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

theory int.Int

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

55 56 57 58
  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
59

60 61 62 63
  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
64 65 66 67 68 69 70 71 72

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

MARCHE Claude's avatar
MARCHE Claude committed
81 82
end

MARCHE Claude's avatar
MARCHE Claude committed
83 84 85 86 87 88
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

89 90 91 92 93 94 95
theory int.MinMax

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

end

96 97
theory int.EuclideanDivision

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

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

end

theory int.ComputerDivision

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

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

end


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

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

120 121 122 123 124
  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
125 126
  syntax logic inv  "(Rinv %1)"

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

  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
141 142 143
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
MARCHE Claude's avatar
MARCHE Claude committed
144 145 146

end

MARCHE Claude's avatar
MARCHE Claude committed
147 148 149 150 151 152 153 154 155 156 157 158 159 160
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
161 162 163 164 165 166 167 168 169

theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end

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

  syntax logic from_int "(IZR %1)"

end

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

  prelude "Require Import R_sqrt."

180
  syntax logic sqr  "(Rsqr %1)"
MARCHE Claude's avatar
MARCHE Claude committed
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
  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


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

  prelude "Require Import Rpower."

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

theory real.Trigonometry

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

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

  syntax logic pi "PI"

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

end