algorithm - 如何实现三角身份证明算法

Question

我如何实现一个接受三角方程两侧的程序(可以推广到任何东西，但现在我将只保留三角恒等式)并且该程序将输出将一侧转换为的步骤另一个(或将它们都转换)以表明它们实际上是相等的。该程序将假定它们首先是相等的。我对如何实现算法来执行此操作感到非常困惑。我的第一个想法是与图表有关，但我想不出除此之外的任何事情。从那里，我认为我应该首先将等式的两边解析为树。例如 (cot x * sin)/(sin x + cos x) 看起来像这样:

     division
     /    \
    *      +
  /  \    / \
cot sin sin cos

在这之后，我有两个类似的想法，都存在问题。第一个想法是选择叶子数量最少的一侧，并尝试使用由“树正则表达式”表示的等效项将其操纵到另一侧。这些“树形正则表达式”的示例是 csc = 1/sin 或 cot = cos/sin(当然是树形)等。我的第二个想法是选择叶子较多的一侧并尝试找到一些表达式，当乘以该表达式时等于另一侧。使用倒数这不会太糟糕，但是，我必须证明我乘以等于 1 的结果。我又回到了这个“树正则表达式”的事情。

这两者的主要缺陷在于我如何应用这些替换的顺序/方式。是只需要一堆 if 语句还是有更优雅的解决方案？实际上是否有我没有看到的基于图形的解决方案。 什么(如果有的话)可能是证明三角恒等式的好算法。

需要明确的是，我不是在谈论“求解 x”类型的问题，例如 tan(x)sin(x) = 5，找到 x 的所有值，而是证明 sqrt((1 + sin x)/(1 - sin x)) = sec x + tan x

Answer 1

这是一个简单的算法，用于确定可以带入 polynomial(sin x, cos x) = 0 形式的三角恒等式。 :

1. 去掉tan x , cot x , sec x , ..., sin 2x , ... 通过明显的替换( tan x -> (sin x)/(cos x) , ..., sin 2x -> 2 (sin x) (cos x) , ...)

2. 通过对(孤立的)根求平方将恒等式转换为多项式(不过，去除一个恒等式中的多个根可能很棘手)，乘以分母并将所有展开的项放在一边

3. 替换所有条款cos^2 x在多项式 ( cos^3 x = (cos^2 x)(cos x) , cos^4 x = (cos^2 x)(cos^2 x) , ...) 中 1 - sin^2 x并展开多项式。

4. 最后是一个没有 cos^2 x 的多项式被计算。如果它与 0 相同，则证明身份，否则身份不成立。

你的例子 sqrt((1 + sin x)/(1 - sin x)) = sec x + tan x :

1. 使用替换 sec x -> 1/(cos x)和 tan x -> (sin x)/(cos x)我们得到

sqrt((1 + sin x)/(1 - sin x)) = 1/(cos x) + (sin x)/(cos x) .

为简洁起见，我们写成s而不是 sin x和 c而不是 cos x ，这给了我们:

sqrt((1 + s)/(1 - s)) = 1/c + s/c

1. 对方程求平方并将两边乘以 (1 - s)c^2我们得到

(1 + s)c^2 = (1 + s)^2(1 - s) .

展开括号并将所有内容都放在一边，我们得到

c^2 - sc^2 + s^3 + s^2 - s - 1 = 0

1. 替换 c^2 = 1 - s^2进入我们得到的多项式

(1 - s^2) - s(1 - s^2) + s^3 + s^2 - s - 1扩展为 0 .

1. 因此身份得到证明。