metitarski.drv 6.26 KB
Newer Older
1
(* Why driver for MetiTarski *)
MARCHE Claude's avatar
MARCHE Claude committed
2
(* main author: Piotr Trojanek <piotr.trojanek@gmail.com> *)
3

4
5
6
7
8
9
10
11
(* TODO:
 * real.FromInt
 * real.Truncate
 * real.PowerInt    (incomplete)
 * real.Hyperbolic
 * real.Polar       (should work as is)
 *)

12
printer "metitarski"
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
filename "%f-%t-%g.tptp"

valid   "^SZS status Theorem"
valid   "^SZS status Unsatisfiable"
unknown "^SZS status CounterSatisfiable" ""
unknown "^SZS status Satisfiable" ""
timeout "^SZS status Timeout"
unknown "^SZS status GaveUp" ""
fail    "^SZS status Error" ""

time "why3cpulimit time : %s s"

(* to be improved *)

transformation "inline_trivial"
transformation "eliminate_builtin"
MARCHE Claude's avatar
MARCHE Claude committed
29
transformation "inline_all"
30
31
32
transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
33
transformation "eliminate_epsilon"
34
35
36
37
38
39
40
41
transformation "eliminate_if"
transformation "eliminate_let"

transformation "simplify_unknown_lsymbols"
transformation "discriminate"
transformation "encoding_tptp"

theory BuiltIn
42
(* support for integers disabled because may be inconsistent
43
  meta "encoding : kept" type int
44
*)
45
  meta "encoding : base" type real
46
47
48
49
  syntax predicate (=)  "(%1 = %2)"
  meta "eliminate_algebraic" "no_index"
end

50
import "discrimination.gen"
51
52

theory real.Real
53

54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
  syntax function zero "0.0"
  syntax function one  "1.0"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (-_) "(-%1)"
  syntax function (*)  "(%1 * %2)"
  syntax function (/)  "(%1 / %2)"
  syntax function inv  "(1/ %1)"

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 < %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 > %2)"

  (* These follow from Metitarski's axioms. *)
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Inverse
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop ZeroLessOne

  remove prop add_div
  remove prop sub_div
  remove prop neg_div
  remove prop assoc_mul_div
  remove prop assoc_div_mul
  remove prop assoc_div_div
  remove prop CompatOrderMult
end

prelude "%%% this is a prelude for Metitarski"
prelude "include('Axioms/general.ax')."

theory real.Abs
  prelude "%%% this is a prelude for Metitarski absolute value"

  syntax function abs "abs(%1)"

  prelude "include('Axioms/abs.ax')."
  prelude "include('Axioms/abs2.ax')."

  (* These follow from Metitarski's axioms. *)
  remove prop Abs_le
  remove prop Abs_pos
  remove prop Abs_sum
  remove prop Abs_prod
  remove prop triangular_inequality
end

theory real.Square
  prelude "%%% this is a prelude for Metitarski square"

  prelude "include('Axioms/sqrt-general.ax')."

  syntax function sqr  "(%1)^2"
MARCHE Claude's avatar
MARCHE Claude committed
124
  syntax function sqrt "sqrt(%1)"
125
126
127
128
129
130
131
132
133
134
135
136

  (* This follows from Metitarski's general axioms. *)
  remove prop Sqrt_positive
  remove prop Sqrt_le
end

theory real.Trigonometry
  prelude "%%% this is a prelude for Metitarski trigonometry"

  prelude "include('Axioms/pi.ax')."

  remove prop Pi_interval
MARCHE Claude's avatar
MARCHE Claude committed
137
138
139
140
141
142
143
144
145
146
147
  remove prop Cos_pi
  remove prop Sin_pi

  remove prop Cos_pi2
  remove prop Sin_pi2

  remove prop Cos_plus_pi
  remove prop Sin_plus_pi

  remove prop Cos_plus_pi2
  remove prop Sin_plus_pi2
148
149
150
151
152

  prelude "include('Axioms/tan.ax')."
  prelude "include('Axioms/arctan-lower.ax')."
  prelude "include('Axioms/arctan-upper.ax')."

153
  syntax function atan "arctan(%1)"
154
155
156
157
158
  syntax function tan  "tan(%1)"

  prelude "include('Axioms/cos.ax')."
  prelude "include('Axioms/sin.ax')."

MARCHE Claude's avatar
MARCHE Claude committed
159
160
161
162
  syntax function cos  "cos(%1)"
  syntax function sin  "sin(%1)"

  (* These follow from Metitarski's base axioms. *)
163
164
165
  remove prop Cos_0
  remove prop Sin_0

166
167
168
  (* The following files "greatly increase the search space" and thus
     cause failures. Do not include them! *)
  (*
169
170
  prelude "include('Axioms/cos-constant.ax')."
  prelude "include('Axioms/sin-constant.ax')."
171
  *)
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190

  remove prop Cos_le_one
  remove prop Sin_le_one
end

theory real.MinMax
  prelude "%%% this is a prelude for Metitarski min-max"

  prelude "include('Axioms/minmax.ax')."

  syntax function min "min(%1,%2)"
  syntax function max "max(%1,%2)"

  remove prop Max_is_ge
  remove prop Max_is_some
  remove prop Min_is_le
  remove prop Min_is_some
end

191
(* support for integers disabled because may be inconsistent
192
193
194
195
196
197
198
199
200
theory real.PowerInt
  syntax function power "%1^%2"

  prelude "%%% this is a prelude for Metitarski power function"

  prelude "include('Axioms/pow.ax')."

  (* These follow from Metitarski's axioms. *)
end
201
*)
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226

theory real.ExpLog
  syntax function exp "exp(%1)"
  syntax function log "ln(%1)"

  prelude "%%% this is a prelude for Metitarski exp/log"

  prelude "include('Axioms/exp-general.ax')."
  prelude "include('Axioms/ln-general.ax')."

  (* These follow from Metitarski's axioms. *)
  remove prop Log_one
  remove prop Exp_zero
end

theory real.PowerReal
  syntax function pow "pow(%1,%2)"

  prelude "include('Axioms/pow.ax')."

  (* These follow from Metitarski's axioms. *)
  remove prop Pow_one_y
  remove prop Pow_exp_log
end

227
(* support for integers disabled because may be inconsistent
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
theory int.Int

  syntax function zero "0"
  syntax function one  "1"

  syntax function (+)  "(%1 + %2)"
  syntax function (-)  "(%1 - %2)"
  syntax function (*)  "(%1 * %2)"
  syntax function (-_) "(-%1)"

  syntax predicate (<=) "(%1 <= %2)"
  syntax predicate (<)  "(%1 < %2)"
  syntax predicate (>=) "(%1 >= %2)"
  syntax predicate (>)  "(%1 > %2)"

  (* These follow from Metitarski's axioms. *)
  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc
  remove prop CommutativeGroup.Unit_def_l
  remove prop CommutativeGroup.Unit_def_r
  remove prop CommutativeGroup.Inv_def_l
  remove prop CommutativeGroup.Inv_def_r
  remove prop Assoc.Assoc
  remove prop Mul_distr_l
  remove prop Mul_distr_r
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
  remove prop ZeroLessOne

end
265
*)