是否有用于提供证明/推导的 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，不过还有很多。

此外，对于对方程两边应用相同转换的具体示例（即，带有头部 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 在表达式上工作的事实任何头部，而不仅仅是头部List。如果您尝试与不熟悉 Mathematica 的受众进行交流，使用此类名称可以帮助您更清晰地进行交流。与此相关，如果您想按照 Ira Baxter 的建议使用替换规则，则写出 Replace 或 ReplaceAll 而不是使用 /. 语法糖可能会有所帮助。

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

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

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

Answer 2

我认为你不需要包裹。你要做的就是根据推理规则来操作每个公式。在 MMa 中，您可以使用转换对公式的推理规则进行建模。因此，如果您有一个公式 f，您可以通过执行（我的 MMa 语法已经 15 年了）来应用推理规则 I

f ./ I 

来生成序列中的下一个公式。

如果公式包含标准代数运算符和术语，例如常数和算术运算符，MMa 当然会尝试简化您的公式。您可以通过将公式包含在 Hold[...] 表单中来防止 MMa 应用其自己的“推理”规则。