Add trigonometric functions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/arith/arith.cpp

@@ -365,6 +365,13 @@ MK_CONSTANT(real_neg_fn, name({"Real", "neg"}));
 MK_CONSTANT(real_ge_fn, name({"Real", "ge"}));
 MK_CONSTANT(real_lt_fn, name({"Real", "lt"}));
 MK_CONSTANT(real_gt_fn, name({"Real", "gt"}));
+MK_CONSTANT(real_pi, name("\u03C0")); // lower case pi
+MK_CONSTANT(sin_fn, name("sin"));
+MK_CONSTANT(cos_fn, name("cos"));
+MK_CONSTANT(tan_fn, name("tan"));
+MK_CONSTANT(cot_fn, name("cot"));
+MK_CONSTANT(sec_fn, name("sec"));
+MK_CONSTANT(csc_fn, name("csc"));
 // =======================================
 
 // =======================================
@@ -449,6 +456,15 @@ void add_arith_theory(environment & env) {
     env.add_definition(real_lt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(y, x))));
     env.add_definition(real_gt_fn_name, rr_b,  Fun({{x, Real}, {y, Real}}, Not(rLe(x, y))));
 
+    env.add_var(real_pi_name, Real);
+    env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi
+    env.add_var(sin_fn_name, r_r);
+    env.add_definition(cos_fn_name, r_r, Fun({x,Real}, Sin(rSub(x, rDiv(mk_real_pi(), mk_real_value(2))))));
+    env.add_definition(tan_fn_name, r_r, Fun({x,Real}, rDiv(Sin(x), Cos(x))));
+    env.add_definition(cot_fn_name, r_r, Fun({x,Real}, rDiv(Cos(x), Sin(x))));
+    env.add_definition(sec_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Cos(x))));
+    env.add_definition(csc_fn_name, r_r, Fun({x,Real}, rDiv(mk_real_value(1), Sin(x))));
+
     env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x))));
 }
 }

src/kernel/arith/arith.h

@@ -128,6 +128,29 @@ inline expr rGt(expr const & e1, expr const & e2) { return mk_app(mk_real_gt_fn(
 inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(Real, c, t, e); }
 // =======================================
 
+// =======================================
+// Transcendental and Hyperbolic
+expr mk_real_pi();
+
+expr mk_sin_fn();
+inline expr Sin(expr const & e) { return mk_app(mk_sin_fn(), e); }
+
+expr mk_cos_fn();
+inline expr Cos(expr const & e) { return mk_app(mk_cos_fn(), e); }
+
+expr mk_tan_fn();
+inline expr Tan(expr const & e) { return mk_app(mk_tan_fn(), e); }
+
+expr mk_cot_fn();
+inline expr Cot(expr const & e) { return mk_app(mk_cot_fn(), e); }
+
+expr mk_sec_fn();
+inline expr Sec(expr const & e) { return mk_app(mk_sec_fn(), e); }
+
+expr mk_csc_fn();
+inline expr Csc(expr const & e) { return mk_app(mk_csc_fn(), e); }
+// =======================================
+
 // =======================================
 // Coercions
 expr mk_nat_to_int_fn();

src/kernel/builtin.cpp

@@ -226,7 +226,7 @@ void add_basic_theory(environment & env) {
     env.add_definition(exists_fn_name, q_type, Fun({{A,TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x)))))));
 
     // homogeneous equality
-    env.add_definition(homo_eq_fn_name, Pi({A,TypeU}, A >> (A >> Bool)), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
+    env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
 
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));

tests/lean/arith4.lean

@@ -0,0 +1,7 @@
+Variable x : Real
+Eval sin(x)
+Eval cos(x)
+Eval tan(x)
+Eval cot(x)
+Eval sec(x)
+Eval csc(x)

tests/lean/arith4.lean.expected.out

@@ -0,0 +1,7 @@
+  Assumed: x
+sin x
+sin (x + -1 * (π / 2))
+(sin x) / (sin (x + -1 * (π / 2)))
+(sin (x + -1 * (π / 2))) / (sin x)
+1 / (sin (x + -1 * (π / 2)))
+1 / (sin x)