Existe-t-il des progiciels Mathematica pour présenter des preuves/dérivations?

Question

Lorsque j'écris une preuve ou une dérivation sur papier, je fais fréquemment des erreurs de signe ou des conditions d'abandon lorsque je passe d'une étape à l'autre. J'aimerais utiliser Mathematica pour me sauver de ces erreurs stupides. Je ne veux pas que Mathematica résolve l'expression, je veux juste l'utiliser pour réaliser et afficher une série de manipulations algébriques. Pour un exemple (trivial)

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 

Est-ce que quelqu'un peut me diriger vers un paquet qui supporterait ce type de manipulation?

Modifier

Merci pour l'entrée, pas tout à fait ce que je suis à la recherche de bien. La manipulation des symboles n'est pas vraiment le problème. Je cherche vraiment quelque chose qui rendra explicite la justification algébrique ou mathématique de chaque étape d'une dérivation. Mon objectif ici est vraiment pédagogique.

Answer 1

Mathematica fournit également un certain nombre de fonctions de haut niveau pour la manipulation algébrique. Parmi ceux-ci sont Expand, Apart et Together, et Cancel, mais il y en a un peu plus.

Aussi, pour votre exemple spécifique de l'application de la même transformation sur les deux côtés d'une équation (qui est, et d'expression avec la tête Equal), vous pouvez utiliser la fonction Thread, qui fonctionne exactement comme votre fonction MultBothSides, mais avec beaucoup plus de généralité.

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 

---

Dans l'une des solutions présentées, il devrait être relativement facile de voir ce que l'étape impliquait. Si vous voulez quelque chose d'un peu plus explicite, vous pouvez écrire votre propre fonction comme ceci:

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

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

Il est une généralisation de votre fonction MultBothSides qui profite du fait que Map travaux sur les expressions avec une tête, non seulement la tête List. Si vous essayez de communiquer avec un public qui n'est pas familier avec Mathematica, l'utilisation de ce type de noms peut vous aider à communiquer plus clairement. Dans le même ordre d'idées, si vous voulez utiliser des règles de remplacement comme suggéré par Ira Baxter, il peut être utile d'écrire Replace ou ReplaceAll au lieu d'utiliser le sucre syntaxique /..

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

Si vous pensez qu'il serait plus clair d'avoir l'équation réelle, au lieu du nom de la variable expression, dans votre entrée, et que vous utilisez l'interface portable, mettez en surbrillance le mot expression avec votre souris, appelez le menu contextuel et sélectionnez "Évaluer sur place". L'interface portable est également un environnement très agréable pour faire de la "programmation alphabétisée", vous pouvez donc également expliquer les étapes qui ne sont pas immédiatement évidentes en mots. Je crois que c'est une bonne pratique pour écrire des preuves mathématiques quel que soit le support.

Answer 2

Je ne pense pas que vous ayez besoin d'un paquet. Ce que vous voulez faire est de manipuler chaque formule selon une règle d'inférence. Dans MMa, vous pouvez modéliser des règles d'inférence sur une formule à l'aide de transformations. Donc, si vous avez une formule f, vous pouvez appliquer une règle d'inférence je en exécutant (ma syntaxe Mma est de 15 ans rouillées)

f ./ I 

pour produire la formule suivante dans la séquence. MMa va bien sûr essayer de simplifier vos formules si elles contiennent des opérateurs et des termes algébriques standard, tels que les nombres constants et les opérateurs arithmétiques. Vous pouvez empêcher MMa d'appliquer ses propres règles d '"inférence" en incluant votre formule dans un formulaire Hold [...].