Come si definisce la moltiplicazione e la struttura degli interi di Gauss in Lean?

La definizione della moltiplicazione negli interi di Gauss è fondata sulla struttura algebrica complessa, dove ogni elemento è rappresentato da una coppia ordinata di numeri interi, indicati come parte reale e parte immaginaria. Formalmente, un elemento è dato da 〈a, b〉 con a, b ∈ ℤ, e l’operazione di moltiplicazione è definita da:

ossia moltiplicando le parti reali e immaginarie secondo la regola usuale dei numeri complessi, ma con componenti intere. In Lean, tale operazione è codificata come una funzione che prende due elementi e restituisce la loro moltiplicazione secondo questa formula.

Questa definizione si colloca all’interno di un namespace dedicato, denominato GaussInt, in cui sono raccolte tutte le definizioni correlate, come gli elementi zero e uno, e le operazioni di somma, negazione e moltiplicazione. L’implementazione fa uso della sintassi e delle funzionalità di Lean per definire istanze di strutture algebriche, permettendo di trattare gli interi di Gauss come un tipo con operazioni algebriche ben definite e coerenti. In particolare, è possibile definire la struttura di anello commutativo (CommRing), dimostrando proprietà algebriche fondamentali come l’associatività e la commutatività delle operazioni, e la distribuzione della moltiplicazione rispetto alla somma.

Gli interi di Gauss, così definiti, costituiscono un esempio di dominio euclideo, ovvero un anello dotato di una norma che permette di generalizzare l’algoritmo euclideo. La norma è definita come:

ossia il prodotto di un numero e del suo coniugato, garantendo proprietà fondamentali come la moltiplicatività della norma:

Questa norma consente di effettuare divisioni con resto analoghe a quelle negli interi classici, permettendo di scrivere ogni elemento non nullo come somma di un multiplo e un resto con norma minore. Tale caratteristica implica che gli interi di Gauss sono un dominio euclideo e, di conseguenza, un dominio di fattorizzazione unica, ovvero ogni elemento può essere scritto in modo unico come prodotto di elementi irriducibili, analogamente alla fattorizzazione degli interi.

Il processo di divisione con resto si basa su un’interpretazione geometrica dei numeri complessi, trattando la divisione come un’operazione su numeri reali e immaginari e approssimando i risultati ai valori interi più vicini. Ciò assicura che il resto abbia norma inferiore a quella del divisore, permettendo l’applicazione dell’algoritmo euclideo.

Questa costruzione in Lean è un esempio paradigmatico di come la teoria algebrica e l’informatica si incontrino per formalizzare strutture matematiche complesse in modo rigoroso e automatizzato. Definire esplicitamente le operazioni, le proprietà e le istanze permette non solo di modellare gli interi di Gauss ma anche di sfruttare le potenzialità della prova automatica per garantire la correttezza formale delle affermazioni algebriche.

È fondamentale comprendere che l’approccio basato su Lean non si limita alla mera definizione di operazioni, ma ingloba anche la struttura e le proprietà astratte che ne conseguono, come il dominio euclideo, la non trivialità dell’anello, e la conseguente fattorizzazione unica. Inoltre, si evidenzia come l’astrazione formale permetta di distinguere concetti quali unità, elementi irriducibili e primi, e come la loro interazione definisca profondamente la struttura algebrica studiata.

La formalizzazione degli interi di Gauss rappresenta un passo cruciale nello studio delle strutture algebriche tramite strumenti di proof assistant, con implicazioni sia teoriche che pratiche. Offre una base solida per ulteriori sviluppi, come la dimostrazione di teoremi più complessi di teoria dei numeri, e fornisce un modello chiaro di come la matematica formale possa essere espressa, verificata e manipolata tramite software.

Perché non è necessario aggiungere add_zero o add_neg_cancel come assiomi del anello?

Nel contesto della teoria degli anelli formale, molte proprietà che sembrano fondamentali in realtà derivano direttamente dagli assiomi di base. Ad esempio, la proprietà che l’elemento zero sia l’identità additiva a sinistra o a destra, o che la somma di un elemento e il suo opposto dia zero, non necessita di essere assunta come assioma separato. Questi risultati si dimostrano a partire dagli assiomi originari, come associatività, commutatività dell’addizione, esistenza dell’elemento neutro e dell’opposto additivo.

Un esempio illuminante è dato dal teorema che l’addizione di un elemento e zero restituisce quell’elemento stesso: si può dimostrare semplicemente usando la commutatività e l’identità a sinistra dello zero. Analogamente, la cancellazione dell’opposto si ricava dalla cancellazione degli elementi con la somma zero. Questi passaggi mostrano che non è necessario dichiararli come assiomi indipendenti.

Nel linguaggio di Lean, questo si traduce nel fatto che alcune variabili di tipo possono essere dichiarate come implicite, cioè omesse durante l’applicazione dei teoremi perché deducibili dal contesto, riducendo la verbosità e migliorando la leggibilità delle dimostrazioni. La sintassi con parentesi graffe {R : Type*} segnala che l’argomento è implicito, permettendo di scrivere dimostrazioni più concise, come add_left_cancel h invece di add_left_cancel a b c h, dove h è l’ipotesi principale.

Un altro aspetto importante è l’uso di sotto-obiettivi nel processo dimostrativo: la tattica have introduce una nuova proposizione da dimostrare all’interno della prova principale, facilitando un approccio modulare alla costruzione della dimostrazione. Questa struttura gerarchica aiuta a mantenere le prove ordinate e facilmente gestibili, mentre l’uso di tattiche come rw, apply ed exact consente di manipolare espressioni algebriche e di chiudere obiettivi con precisione.

Nel contesto degli anelli, la sottrazione è definita come somma dell’opposto additivo, e ciò è formalizzato in Lean attraverso un’uguaglianza definizionale che permette di sostituire a - b con a + (-b). Questa equivalenza è una forma di uguaglianza definizionale, che consente di usare entrambi i lati dell’uguaglianza in modo intercambiabile, semplificando le dimostrazioni.

Un aspetto essenziale da comprendere è che molte proprietà di base dell’addizione e dell’opposto additivo richiedono in realtà una struttura più debole rispetto a un anello, ovvero quella di un gruppo additivo. La teoria dei gruppi, infatti, assume solo la chiusura, associatività, esistenza dell’elemento neutro e dell’inverso, senza necessità di moltiplicazione o commutatività. Questa distinzione permette di vedere gli anelli come estensioni dei gruppi con ulteriori operazioni e assiomi.

Per una comprensione più profonda, è utile cogliere che dimostrare teoremi in questo contesto è spesso una questione di manipolare correttamente gli assiomi e utilizzare tattiche che permettono di decomporre i problemi complessi in parti più semplici e gestibili. La formalizzazione con strumenti come Lean non solo verifica la correttezza delle dimostrazioni, ma aiuta anche a illuminare le interrelazioni tra le proprietà algebriche, rendendo evidente ciò che è effettivamente necessario assumere e ciò che invece si ottiene come conseguenza.

È importante ricordare che l’astrazione delle strutture algebriche permette di trasportare facilmente risultati da una struttura all’altra. Conoscere la dipendenza tra proprietà permette di evitare di assumere ridondanze, concentrando l’attenzione sugli assiomi essenziali. Questo approccio migliora la chiarezza e la comprensione della teoria algebrica in senso generale.