drivers/metitarski.drv

   1 (* Why driver for MetiTarski *)
   2 (* main author: Piotr Trojanek <piotr.trojanek@gmail.com> *)
   3
   4 (* TODO:
   5  * real.FromInt
   6  * real.Truncate
   7  * real.PowerInt    (incomplete)
   8  * real.Hyperbolic
   9  * real.Polar       (should work as is)
  10  *)
  11
  12 printer "metitarski"
  13 filename "%f-%t-%g.tptp"
  14
  15 valid   "^SZS status Theorem"
  16 valid   "^SZS status Unsatisfiable"
  17 unknown "^SZS status CounterSatisfiable" ""
  18 unknown "^SZS status Satisfiable" ""
  19 timeout "^SZS status Timeout"
  20 unknown "^SZS status GaveUp" ""
  21 fail    "^SZS status Error" ""
  22
  23 time "why3cpulimit time : %s s"
  24
  25 (* to be improved *)
  26
  27 (* Performed introductions depending on whether counterexamples are
  28    requested, as said by the meta "get_counterexmp". When this meta
  29    set, this transformation introduces the model variables that are
  30    still embedded in the goal. When it is not set, it removes all
  31    these unused-ce-related variables, even in the context.  *)
  32 transformation "counterexamples_dependent_intros"
  33
  34 transformation "inline_trivial"
  35 transformation "eliminate_builtin"
  36 transformation "inline_all"
  37 transformation "eliminate_definition"
  38 transformation "eliminate_inductive"
  39 transformation "eliminate_if"
  40 transformation "eliminate_epsilon"
  41 transformation "eliminate_algebraic"
  42 transformation "eliminate_literal"
  43 transformation "eliminate_let"
  44 transformation "eliminate_negative_constants" (* due to integers, see below *)
  45
  46 transformation "simplify_formula"
  47 transformation "simplify_unknown_lsymbols"
  48 transformation "simplify_trivial_quantification"
  49 transformation "introduce_premises"
  50 transformation "instantiate_predicate"
  51 transformation "abstract_unknown_lsymbols"
  52
  53 transformation "discriminate"
  54 transformation "encoding_tptp"
  55
  56 theory BuiltIn
  57 (* support for integers disabled because may be inconsistent
  58   meta "encoding:kept" type int
  59 *)
  60   meta "encoding:base" type real
  61   syntax predicate (=)  "(%1 = %2)"
  62   meta "eliminate_algebraic" "no_index"
  63 end
  64
  65 import "discrimination.gen"
  66
  67 theory real.Real
  68
  69   syntax function zero "0.0"
  70   syntax function one  "1.0"
  71
  72   syntax function (+)  "(%1 + %2)"
  73   syntax function (-)  "(%1 - %2)"
  74   syntax function (-_) "(-%1)"
  75   syntax function (*)  "(%1 * %2)"
  76   syntax function (/)  "(%1 / %2)"
  77   syntax function inv  "(1/ %1)"
  78
  79   syntax predicate (<=) "(%1 <= %2)"
  80   syntax predicate (<)  "(%1 < %2)"
  81   syntax predicate (>=) "(%1 >= %2)"
  82   syntax predicate (>)  "(%1 > %2)"
  83
  84   meta "inline:no" predicate (<=)
  85   meta "inline:no" predicate (>=)
  86   meta "inline:no" predicate (>)
  87
  88   (* These follow from Metitarski's axioms. *)
  89   remove prop MulComm.Comm
  90   remove prop MulAssoc.Assoc
  91   remove prop Unit_def_l
  92   remove prop Unit_def_r
  93   remove prop Inv_def_l
  94   remove prop Inv_def_r
  95   remove prop Assoc
  96   remove prop Mul_distr_l
  97   remove prop Mul_distr_r
  98   remove prop Comm
  99   remove prop Unitary
 100   remove prop Inverse
 101   remove prop Refl
 102   remove prop Trans
 103   remove prop Antisymm
 104   remove prop Total
 105   remove prop NonTrivialRing
 106   remove prop CompatOrderAdd
 107   remove prop ZeroLessOne
 108
 109   remove prop add_div
 110   remove prop sub_div
 111   remove prop neg_div
 112   remove prop assoc_mul_div
 113   remove prop assoc_div_mul
 114   remove prop assoc_div_div
 115   remove prop CompatOrderMult
 116 end
 117
 118 prelude "%%% this is a prelude for Metitarski"
 119 prelude "include('Axioms/general.ax')."
 120
 121 theory real.Abs
 122   prelude "%%% this is a prelude for Metitarski absolute value"
 123
 124   syntax function abs "abs(%1)"
 125
 126   prelude "include('Axioms/abs.ax')."
 127   prelude "include('Axioms/abs2.ax')."
 128
 129   (* These follow from Metitarski's axioms. *)
 130   remove prop Abs_le
 131   remove prop Abs_pos
 132   remove prop Abs_sum
 133   remove prop Abs_prod
 134   remove prop triangular_inequality
 135 end
 136
 137 theory real.Square
 138   prelude "%%% this is a prelude for Metitarski square"
 139
 140   prelude "include('Axioms/sqrt-general.ax')."
 141
 142   syntax function sqr  "(%1)^2"
 143   syntax function sqrt "sqrt(%1)"
 144
 145   (* This follows from Metitarski's general axioms. *)
 146   remove prop Sqrt_positive
 147   remove prop Sqrt_le
 148 end
 149
 150 theory real.Trigonometry
 151   prelude "%%% this is a prelude for Metitarski trigonometry"
 152   remove allprops
 153
 154   prelude "include('Axioms/pi.ax')."
 155
 156   syntax function atan "arctan(%1)"
 157   syntax function tan  "tan(%1)"
 158
 159   prelude "include('Axioms/tan.ax')."
 160   prelude "include('Axioms/arctan-lower.ax')."
 161   prelude "include('Axioms/arctan-upper.ax')."
 162
 163   syntax function cos  "cos(%1)"
 164   syntax function sin  "sin(%1)"
 165
 166   prelude "include('Axioms/cos.ax')."
 167   prelude "include('Axioms/sin.ax')."
 168
 169   (* The following files "greatly increase the search space" and thus
 170      cause failures. Do not include them! *)
 171   (*
 172   prelude "include('Axioms/cos-constant.ax')."
 173   prelude "include('Axioms/sin-constant.ax')."
 174   *)
 175
 176 end
 177
 178 theory real.MinMax
 179   prelude "%%% this is a prelude for Metitarski min-max"
 180
 181   prelude "include('Axioms/minmax.ax')."
 182
 183   syntax function min "min(%1,%2)"
 184   syntax function max "max(%1,%2)"
 185
 186   remove prop Max_l
 187   remove prop Min_r
 188   remove prop Max_comm
 189   remove prop Min_comm
 190   remove prop Max_assoc
 191   remove prop Min_assoc
 192 end
 193
 194 (* support for integers disabled because may be inconsistent
 195 theory real.PowerInt
 196   syntax function power "%1^%2"
 197
 198   prelude "%%% this is a prelude for Metitarski power function"
 199
 200   prelude "include('Axioms/pow.ax')."
 201
 202   (* These follow from Metitarski's axioms. *)
 203 end
 204 *)
 205
 206 theory real.ExpLog
 207   syntax function exp "exp(%1)"
 208   syntax function log "ln(%1)"
 209
 210   prelude "%%% this is a prelude for Metitarski exp/log"
 211
 212   prelude "include('Axioms/exp-general.ax')."
 213   prelude "include('Axioms/ln-general.ax')."
 214
 215   (* These follow from Metitarski's axioms. *)
 216   remove prop Log_one
 217   remove prop Exp_zero
 218 end
 219
 220 theory real.PowerReal
 221   syntax function pow "pow(%1,%2)"
 222
 223   prelude "include('Axioms/pow.ax')."
 224
 225   (* These follow from Metitarski's axioms. *)
 226   remove prop Pow_def
 227   remove prop Pow_one_y
 228 end
 229
 230 (* support for integers disabled because may be inconsistent
 231 theory int.Int
 232
 233   syntax function zero "0"
 234   syntax function one  "1"
 235
 236   syntax function (+)  "(%1 + %2)"
 237   syntax function (-)  "(%1 - %2)"
 238   syntax function (*)  "(%1 * %2)"
 239   syntax function (-_) "(-%1)"
 240
 241   syntax predicate (<=) "(%1 <= %2)"
 242   syntax predicate (<)  "(%1 < %2)"
 243   syntax predicate (>=) "(%1 >= %2)"
 244   syntax predicate (>)  "(%1 > %2)"
 245
 246   (* These follow from Metitarski's axioms. *)
 247   remove prop MulComm.Comm
 248   remove prop MulAssoc.Assoc
 249   remove prop Unit_def_l
 250   remove prop Unit_def_r
 251   remove prop Inv_def_l
 252   remove prop Inv_def_r
 253   remove prop Assoc
 254   remove prop Mul_distr_l
 255   remove prop Mul_distr_r
 256   remove prop Comm
 257   remove prop Unitary
 258   remove prop Refl
 259   remove prop Trans
 260   remove prop Antisymm
 261   remove prop Total
 262   remove prop NonTrivialRing
 263   remove prop CompatOrderAdd
 264   remove prop CompatOrderMult
 265   remove prop ZeroLessOne
 266
 267 end
 268 *)