Metitarski, improved driver

drivers/metitarski.drv

@@ -24,8 +24,8 @@ time "why3cpulimit time : %s s"
 (* to be improved *)
 
 transformation "inline_trivial"
-
 transformation "eliminate_builtin"
+transformation "inline_all"
 transformation "eliminate_definition"
 transformation "eliminate_inductive"
 transformation "eliminate_algebraic"
@@ -118,6 +118,7 @@ theory real.Square
   prelude "include('Axioms/sqrt-general.ax')."
 
   syntax function sqr  "(%1)^2"
+  syntax function sqrt "sqrt(%1)"
 
   (* This follows from Metitarski's general axioms. *)
   remove prop Sqrt_positive
@@ -130,6 +131,17 @@ theory real.Trigonometry
   prelude "include('Axioms/pi.ax')."
 
   remove prop Pi_interval
+  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
 
   prelude "include('Axioms/tan.ax')."
   prelude "include('Axioms/arctan-lower.ax')."
@@ -138,17 +150,20 @@ theory real.Trigonometry
   syntax function atan  "arctan(%1)"
   syntax function tan  "tan(%1)"
 
-  (* These follow from Metitarski's base axioms. *)
   prelude "include('Axioms/cos.ax')."
   prelude "include('Axioms/sin.ax')."
 
+  syntax function cos  "cos(%1)"
+  syntax function sin  "sin(%1)"
+
+  (* These follow from Metitarski's base axioms. *)
   remove prop Cos_0
   remove prop Sin_0
 
-  (* These follow from Metitarski's auxiliary axioms. *)
   prelude "include('Axioms/cos-constant.ax')."
   prelude "include('Axioms/sin-constant.ax')."
 
+  (* These follow from Metitarski's auxiliary axioms. *)
   remove prop Cos_le_one
   remove prop Sin_le_one
 end

examples/tests-provers/metitarski.why

@@ -10,4 +10,28 @@ theory P
   goal sqr_pos :
     forall x:real. sqr x >= 0.0
 
-end
\ No newline at end of file
+end
+
+theory P2
+
+  use import real.Real
+  use import real.Square
+
+  goal sqr_pos :
+    forall x:real. sqr x >= 0.0
+
+end
+
+theory P3
+
+  use import real.Real
+  use import real.Trigonometry
+
+  goal cos_bound :
+    forall x:real. -1.0 <= cos x <= 1.0
+
+  goal cos_bound_harder :
+    forall x:real. 0.0 <= x <= 0.1 -> 0.1 <= cos x <= 1.0
+
+end
+

plugins/tptp/tptp_printer.ml

@@ -71,8 +71,10 @@ let number_format = {
   Number.def_int_support = Number.Number_unsupported;
   Number.dec_real_support = Number.Number_default;
   Number.hex_real_support = Number.Number_unsupported;
-  Number.frac_real_support = Number.Number_unsupported;
-  Number.def_real_support = Number.Number_unsupported;
+  Number.frac_real_support = Number.Number_custom
+    (Number.PrintFracReal ("%s", "(%s * %s)", "(%s / %s)"));
+  Number.def_real_support = Number.Number_unsupported
+  ;
 }
 
 let rec print_app info fmt ls tl oty =