From 4eaba93591d82c6d01738f785f8d73cafc43c6a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Sep 2013 17:01:50 -0700 Subject: [PATCH] Add trigonometric functions Signed-off-by: Leonardo de Moura --- src/kernel/arith/arith.cpp | 16 ++++++++++++++++ src/kernel/arith/arith.h | 23 +++++++++++++++++++++++ src/kernel/builtin.cpp | 2 +- tests/lean/arith4.lean | 7 +++++++ tests/lean/arith4.lean.expected.out | 7 +++++++ 5 files changed, 54 insertions(+), 1 deletion(-) create mode 100644 tests/lean/arith4.lean create mode 100644 tests/lean/arith4.lean.expected.out diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp index 7fa53cae7..db4257bed 100644 --- a/src/kernel/arith/arith.cpp +++ b/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)))); } } diff --git a/src/kernel/arith/arith.h b/src/kernel/arith/arith.h index 1c711e1c9..8a1cd2b8c 100644 --- a/src/kernel/arith/arith.h +++ b/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(); diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index f0aa04cbe..c1c8f62b2 100644 --- a/src/kernel/builtin.cpp +++ b/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)); diff --git a/tests/lean/arith4.lean b/tests/lean/arith4.lean new file mode 100644 index 000000000..54f6e74e2 --- /dev/null +++ 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) \ No newline at end of file diff --git a/tests/lean/arith4.lean.expected.out b/tests/lean/arith4.lean.expected.out new file mode 100644 index 000000000..3d819ea0b --- /dev/null +++ b/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)