Come si costruiscono e manipolano le strutture in Lean?

In Lean, la definizione di strutture permette di organizzare in modo compatto dati e proprietà logiche. Si tratta di una forma di astrazione essenziale che consente non solo di raggruppare informazioni, ma anche di vincolarle a soddisfare determinate condizioni. La potenza di questo approccio emerge chiaramente quando si lavora con oggetti matematici complessi, come spazi geometrici o strutture algebriche, che richiedono coerenza tra i dati e le proprietà che essi devono rispettare.

La definizione alternativa addAlt mostra chiaramente come, anche se l’operazione resta formalmente identica, il contesto tecnico in cui viene interpretata cambia. Il teorema della commutatività, addAlt_comm, ne è un esempio: pur essendo valido in entrambe le definizioni, l’interfaccia offerta dalla versione con costruttori anonimi rende meno chiara la traccia della dimostrazione. È un dettaglio che acquista peso nella costruzione di teoremi più articolati, dove la pulizia semantica della formulazione incide sulla chiarezza del ragionamento.

La modellazione del 2-simplesso standard rappresenta un altro esempio significativo. Esso è definito come l’insieme di punti tridimensionali reali che soddisfano tre disuguaglianze (coordinate non negative) e una equazione (la somma delle coordinate è uno). Lean consente di formalizzare tutto questo come una struttura in cui le proprietà richieste sono incorporate come campi di tipo Prop, legati direttamente ai dati. È notevole la capacità di Lean di consentire il riutilizzo sistematico di queste proprietà nei costruttori secondari, come nella funzione midpoint, dove si ottiene il punto medio tra due elementi del simplesso garantendo che tutte le proprietà siano automaticamente verificate.

Questo approccio si estende in modo naturale al simplesso di dimensione arbitraria $n$, dove si rappresenta un p

Come Lean gestisce le strutture algebriche tramite l'inferenza delle classi?

Questa modalità consente di definire operazioni come la moltiplicazione, l’identità e l’inversione in un gruppo in maniera generica. Per esempio, per il gruppo delle permutazioni di un tipo, si specificano come istanze le operazioni di composizione, identità e inversione usando le funzioni standard di equivalenza. Lean, così, attraverso la sua inferenza, riesce a dedurre automaticamente la struttura del gruppo in contesti più ampi, senza la necessità di dichiarare esplicitamente ogni volta l’istanza o il tipo.

Un esempio tipico è la definizione di funzioni generiche su gruppi, come una funzione mySquare che eleva al quadrato un elemento del gruppo. Grazie all’inferenza, non è necessario specificare esplicitamente la struttura di gruppo ogni volta che si usa questa funzione: Lean la riconosce implicitamente tramite gli argomenti impliciti {α : Type*} per il tipo degli elementi e [Group2 α] per la struttura del gruppo.

La potenza di questo sistema emerge anche nell'uso di notazioni standard, come il simbolo + per l'addizione. In Lean, l'operatore + è un’abbreviazione per un’operazione binaria registrata tramite una classe, ad esempio Add. Per un tipo definito come Point, si può registrare un’istanza di Add che lega l’operazione + all’implementazione specifica per Point. Allo stesso modo, si possono definire e sovraccaricare le notazioni per altre strutture algebriche (come i gruppi additivi, i gruppi moltiplicativi e gli anelli) creando una gerarchia coerente di classi e istanze.

Il meccanismo funziona tramite una ricerca ricorsiva degli istanze dichiarate. Per esempio, per trovare l’operazione di moltiplicazione per un tipo complesso come Equiv.Perm α, Lean cerca un’istanza di Mul associata a quel tipo. Se questa non è definita direttamente, cerca un’istanza di Group2 corrispondente, che a sua volta fornisce l’operazione di moltiplicazione. Questo meccanismo permette di combinare e comporre strutture algebriche in modo flessibile e modulare.

Tuttavia, l’uso di questa potenza deve essere gestito con attenzione. È facile incorrere in ambiguità quando più istanze compatibili sono presenti contemporaneamente, come nel caso di diverse definizioni di gruppo per lo stesso tipo. Lean sceglie per default l’istanza più recente a meno che non venga specificata una priorità diversa. Inoltre, è possibile dichiarare che una struttura estende un’altra, facilitando la definizione di gerarchie algebriche, per esempio indicando che ogni anello commutativo è anche un anello.

Ad esempio, si può definire una nuova classe AddGroup2, simile a Group2 ma per la somma, insieme alle operazioni di addizione, negazione e zero, e dimostrare che un tipo come Point ne è istanza. L’inferenza permetterà quindi di usare la notazione + per i punti come se fosse una somma algebrica standard.

Nell’uso pratico, ciò significa che quando si formalizza la matematica in Lean, la definizione di una struttura algebrica e delle sue istanze non è solo una questione di indicare operazioni e proprietà, ma anche di fornire al sistema un modo per dedurre automaticamente come combinare queste informazioni. Questo consente di scrivere codice matematico altamente generico, riutilizzabile e integrato, riducendo la necessità di ripetizioni e rendendo più semplice estendere la libreria matematica.

Un aspetto importante da considerare è che, dietro le quinte, Lean conduce una ricerca ricorsiva per risolvere gli argomenti impliciti basandosi sulle istanze dichiarate. Questo sistema di inferenza automatica, benché potente, deve essere usato con consapevolezza, perché una cattiva gestione delle istanze o ambiguità può portare a errori difficili da diagnosticare o a comportamenti non intenzionali. Una buona pratica è mantenere ordine nelle priorità delle istanze e definire chiaramente le relazioni tra le strutture, sfruttando il meccanismo extends per mantenere una gerarchia logica.

Oltre alla pura definizione delle strutture, è importante riconoscere che questo sistema abilita la costruzione di oggetti matematici più complessi, come i numeri Gaussiani, considerati come un tipo proprio e non semplicemente come un sottoinsieme dei numeri complessi. Qui si definisce il tipo GaussInt come una struttura contenente due componenti intere, rappresentando la parte reale e immaginaria. Si possono quindi definire le operazioni di anello, inclusa la moltiplicazione, in modo coerente con le proprietà algebriche attese, e dimostrare che i numeri Gaussiani costituiscono un dominio euclideo.

Come si definiscono e si utilizzano le nozioni fondamentali degli spazi metrici?

Nel contesto degli spazi metrici, una delle costruzioni fondamentali è quella delle palle metriche, sia aperte che chiuse. La palla chiusa di centro $a$ e raggio $r$, denotata come $\text{closedBall } a \, r = \{ b \mid \text{dist}(b,a) \leq r \}$, è definita senza alcuna restrizione sul segno di $r$. Tuttavia, molte proprietà rilevanti richiedono che il raggio sia positivo o non negativo, ad esempio la proprietà che $a$ appartiene alla palla aperta o chiusa di centro $a$ e raggio $r$, per $r>0$ o $r \geq 0$ rispettivamente.

Nel quadro più ampio della topologia sui metrici, i filtri di intorno giocano un ruolo cruciale: le palle metriche formano una base per il filtro degli intorni di un punto, sia per le palle aperte sia per quelle chiuse di raggio positivo.

La compattezza emerge come una nozione topologica fondamentale, che distingue quegli insiemi metrici con proprietà analoghe agli intervalli chiusi e limitati dei reali. Per un insieme compatto vale, tra l’altro, che ogni successione con valori in esso contiene una sottosuccessione convergente, che ogni funzione continua definita sull’insieme assume i propri estremi e che l’insieme stesso è chiuso. Queste proprietà, spesso dedotte da risultati più generali, costituiscono la spina dorsale dell’analisi e della topologia degli spazi metrici.

Passando alle funzioni uniformemente continue, queste sono caratterizzate dalla possibilità di scegliere un unico $\delta$ valido uniformemente per tutti i punti del dominio in risposta a un dato $\varepsilon$. Un risultato fondamentale è che ogni funzione continua definita su uno spazio metrico compatto è uniformemente continua. La dimostrazione di ciò sfrutta la compattezza del dominio per ridurre il problema all’estremo valore di una funzione continua opportunamente definita sul prodotto cartesiano.

Infine, il teorema di Baire per spazi metrici completi fornisce un risultato potente e non banale: l’intersezione numerabile di insiemi aperti densi è ancora densa. La dimostrazione utilizza tecniche sofisticate quali definizioni induttive e costruzioni esplicite di successioni di palle di raggio decrescente, che permettono di affermare la densità dell’intersezione.

Inoltre, la comprensione del ruolo dei filtri di intorni e delle basi generate dalle palle metriche permette di afferrare le radici più profonde della continuità e della topologia metrica. La uniformità nella continuità, distinta dalla mera continuità puntuale, garantisce un controllo globale sul comportamento delle funzioni, elemento chiave in molte applicazioni pratiche e teoriche.

Questa visione integrata consente di cogliere la potenza e la flessibilità del linguaggio degli spazi metrici, fornendo al lettore gli strumenti per affrontare problemi complessi, sia in analisi pura che in applicazioni interdisciplinari.