coq.drv 3.97 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
10
prelude "(* This file is generated by Why3's Coq driver *)"
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
19
20
21
22
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"

transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal"


MARCHE Claude's avatar
MARCHE Claude committed
23
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
24
25
26
27

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

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

MARCHE Claude's avatar
MARCHE Claude committed
33
34
theory bool.Bool

35
  syntax type bool   "bool"
MARCHE Claude's avatar
MARCHE Claude committed
36

37
  syntax logic True  "true"
MARCHE Claude's avatar
MARCHE Claude committed
38
39
  syntax logic False "false"

40
41
42
43
  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
44
45
46

end

MARCHE Claude's avatar
MARCHE Claude committed
47
48
49
50

theory int.Int

  syntax logic zero "0%Z"
51
  syntax logic one  "1%Z"
MARCHE Claude's avatar
MARCHE Claude committed
52

53
54
55
56
  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
57

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

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

MARCHE Claude's avatar
MARCHE Claude committed
79
80
end

MARCHE Claude's avatar
MARCHE Claude committed
81
82
83
84
85
86
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

87
88
theory int.EuclideanDivision

MARCHE Claude's avatar
MARCHE Claude committed
89
  prelude "Require Import Zdiv."
90
91
92
93
94
95
96
97

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

end

theory int.ComputerDivision

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

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

end


MARCHE Claude's avatar
MARCHE Claude committed
106
107
108
theory real.Real

  syntax logic zero "0%R"
109
  syntax logic one  "1%R"
MARCHE Claude's avatar
MARCHE Claude committed
110

111
112
113
114
115
  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
116
117
  syntax logic inv  "(Rinv %1)"

118
119
120
121
  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
122
123
124
125
126
127
128
129
130
131

  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
132
133
134
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
MARCHE Claude's avatar
MARCHE Claude committed
135
136
137

end

MARCHE Claude's avatar
MARCHE Claude committed
138
139
140
141
142
143
144
145
146
147
148
149
150
151
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
152
153
154
155
156
157
158
159
160

theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
161
162
163
164
165
166
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
167
168
169
170
theory real.Square

  prelude "Require Import R_sqrt."

171
  syntax logic sqr  "(Rsqr %1)"
MARCHE Claude's avatar
MARCHE Claude committed
172
173
174
175
176
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
204
205
206
207
208
  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


theory real.Power 

  prelude "Require Import Rpower."

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

theory real.Trigonometry

  prelude "Require Import Rtrigo." 
  prelude "Require Import AltSeries." (* for def of pi *)

  syntax logic cos "(cos %1)"
  syntax logic sin "(sin %1)"

  syntax logic pi "PI"

  syntax logic tan "(tan %1)"
  (* syntax logic atan "atan not defined in Coq ?" *)

end