Esistono pacchetti Mathematica per la presentazione di prove/derivazioni?

Question

Quando scrivo una prova o una derivazione su carta, faccio spesso errori di segno o termini di rilascio mentre passo da un passaggio a quello successivo. Mi piacerebbe usare Mathematica per salvarmi da questi errori stupidi. Non voglio che Mathematica risolva l'espressione, voglio solo usarla per eseguire e visualizzare una serie di manipolazioni algebriche. Per un esempio (banale)

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 

Qualcuno può indicarmi un pacchetto che supporti questo tipo di manipolazione?

Modifica

Grazie per l'ingresso, non è proprio quello che sto cercando però. La manipolazione dei simboli non è davvero il problema. Sto davvero cercando qualcosa che renderà esplicita la giustificazione algebrica o matematica di ogni fase di una derivazione. Il mio obiettivo qui è davvero pedagogico.

Answer 1

Mathematica fornisce anche una serie di funzioni di alto livello per la manipolazione algebrica. Tra questi ci sono Expand, Apart e Together e Cancel, anche se ce ne sono molti altri.

Inoltre, per lo specifico esempio di applicazione della stessa trasformazione di entrambi i lati di un'equazione (cioè, e l'espressione con la testa Equal), è possibile utilizzare la funzione Thread, che funziona come la funzione MultBothSides, ma con molto più generalità.

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 entrambe le soluzioni presentate, dovrebbe essere relativamente facile vedere qual è il passo comportava. Se volete qualcosa di un po 'più esplicito, è possibile scrivere la propria funzione in questo modo:

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

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

Si tratta di una generalizzazione della funzione MultBothSides che sfrutta il fatto che Map opere su espressioni con qualsiasi testa, non solo la testa List. Se stai cercando di comunicare con un pubblico che non ha familiarità con Mathematica, l'utilizzo di questi tipi di nomi può aiutarti a comunicare in modo più chiaro. In una vena correlata, se si desidera utilizzare le regole di sostituzione come suggerito da Ira Baxter, potrebbe essere utile scrivere Replace o ReplaceAll invece di utilizzare lo zucchero sintattico /..

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

Se si pensa che sarebbe più chiaro di avere l'equazione reale, al posto del nome della variabile expression, nel vostro ingresso, e si sta utilizzando l'interfaccia notebook, evidenziare la parola expression con il mouse, richiamare il menu contestuale e selezionare "Valuta in posizione".

L'interfaccia notebook è anche un ambiente molto piacevole per fare "programmazione alfabetica", quindi è anche possibile spiegare eventuali passaggi che non sono immediatamente evidenti a parole. Credo che questa sia una buona pratica quando si scrivono prove matematiche indipendentemente dal mezzo.

Answer 2

Non penso che sia necessario un pacchetto. Quello che vuoi fare è manipolare ciascuna formula in base a una regola di inferenza. In MMa, puoi modellare le regole di inferenza su una formula utilizzando le trasformazioni. Quindi, se si dispone di una formula f, è possibile applicare una regola di inferenza I eseguendo (la mia sintassi MMA è di 15 anni) arrugginiti

f ./ I 

per produrre la formula successiva nella sequenza.

MMa cercherà ovviamente di semplificare le formule se contengono operatori algebrici standard e termini, come numeri costanti e operatori aritmetici. È possibile impedire a MMa di applicare le proprie regole di "inferenza" allegando la formula in un modulo Hold [...] Hold.