Существуют ли пакеты 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, использование таких имен может помочь вам общаться более четко. В том же духе, если вы хотите использовать правила замены, предложенные Айрой Бакстер, полезно написать Replace или ReplaceAll вместо использования синтаксического сахара /..

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

Если вы думаете, что было бы яснее ввести в уравнение действительное уравнение вместо имени переменной expression и вы используете интерфейс ноутбука, выделите слово expression с помощью мыши, вызовите в контекстном меню выберите «Оценить на месте».

Интерфейс ноутбука также очень приятная среда для «грамотного программирования», поэтому вы также можете объяснить любые шаги, которые не сразу очевидны на словах. Я считаю, что это хорошая практика при написании математических доказательств независимо от среды.

Answer 2

Не думаю, что вам нужен пакет. Что вы хотите сделать, это манипулировать каждой формулой в соответствии с правилом вывода. В MMa вы можете моделировать правила вывода по формуле, используя преобразования. Итак, если у вас есть формула f , вы можете применить правило вывода I , выполнив (мой синтаксис MMa устарел на 15 лет)

f ./ I 

для получения следующей формулы в вашей последовательности.

MMa, конечно, попытается упростить ваши формулы, если они содержат стандартные алгебраические операторы и термины, такие как постоянные числа и арифметические операторы. Вы можете запретить MMa применять свои собственные правила «вывода», заключив вашу формулу в форму Hold [...] .