是否有Mathematica包用于提供证明/推导？

Question

当我在纸上写出证明或推导时,我经常会在我从一步到下一步时发出符号错误或删除条款.我想用Mathematica来避免这些愚蠢的错误.我不希望Mathematica解决表达式,我只是想用它来执行并显示一系列代数操作.对于(微不足道的)例子

In[111]:= MultBothSides[Equal[a_, b_], c_] := Equal[c a, c b];

In[112]:= expression = 2 a == a b

Out[112]= 2 a == a b

In[113]:= MultBothSides[expression, 1/a]

Out[113]= 2 == b

任何人都可以指出一个支持这种操作的包吗？

编辑

感谢您的投入,但不是我想要的.符号操作并不是真正的问题.我真的在寻找能够明确推导出每个步骤的代数或数学证明的东西.我的目标是教学.

Answer 1

Mathematica 还提供了许多用于处理代数的高级函数。其中有Expand、Apart、Together、 和Cancel，不过还有很多。

另外，对于将相同变换应用于方程两侧（即带有 head 的表达式Equal）的具体示例，您可以使用该Thread函数，它的工作原理与您的函数类似MultBothSides，但具有更多的通用性。

In[1]:=  expression = 2 a == a b
Out[1]:= 2 a == a b

In[2]:=  Thread[expression /a, Equal]
Out[2]:= 2 == b

In[3]:=  Thread[expression - c, Equal]
Out[3]:= 2 a - c == a b - c

在所提出的任一解决方案中，应该相对容易看出该步骤需要做什么。如果您想要更明确的东西，您可以编写自己的函数，如下所示：

In[4]:=  ApplyToBothSides[f_, eq_Equal] := Map[f, eq]

In[5]:=  ApplyToBothSides[4 * #&, expression]
Out[5]:= 8 a == 4 a b

它是您的函数的概括MultBothSides，它利用了适用于Map任何 head 的表达式，而不仅仅是 head 的事实List。如果您尝试与不熟悉 Mathematica 的受众进行交流，使用此类名称可以帮助您更清晰地进行交流。与此相关的是，如果您想使用 Ira Baxter 建议的替换规则，则写出 Replace 或 ReplaceAll 而不是使用/.语法糖可能会有所帮助。

In[6]:=  ReplaceAll[expression, a -> (x + y)]
Out[6]:= 2 (x + y) == b (x + y)

如果您认为在输入中使用实际方程而不是变量名称会更清晰，expression并且您正在使用笔记本界面，请expression用鼠标突出显示该单词，调出上下文菜单，然后选择“评估”地方”。

笔记本界面也是进行“文学编程”的一个非常愉快的环境，因此您还可以解释任何文字上不明显的步骤。我相信在编写数学证明时，无论使用何种媒介，这都是一个很好的做法。