ZFLean: a framework for set-level mathematics in Lean

1. Enunciato del Problema

La formalizzazione moderna negli assistenti di dimostrazione come Lean è prevalentemente basata sulla teoria dei tipi (in particolare la teoria dei tipi dipendenti), dove gli oggetti matematici sono tipi costruiti. Sebbene potente, questo approccio può essere ingombrante per la matematica a livello di insiemi (ZFC), che è spesso preferita per:

• Ragionamento estensionale: Ragionare sull'uguaglianza basandosi sugli elementi piuttosto che sulla costruzione.
• Parzialità: Gestire le funzioni parziali in modo naturale tramite relazioni invece di codificarle con tipi Option o tipi dipendenti.
• Ragionamento in stile categoriale: Lavorare "a meno di isomorfismo" invece che con l'uguaglianza definizionale stretta.

La Sfida: Lavorare direttamente in un modello insiemistico all'interno di un assistente tipato (come il modello ZFC di Mathlib in Lean) introduce un attrito significativo:

• Boilerplate: Gli utenti devono gestire costantemente manualmente le "condizioni laterali" (ad esempio, dimostrare che una relazione è ben definita, dimostrare che una funzione è totale).
• Fragilità: Attraversare il confine tra oggetti insiemistici (ZFSet) e tipi nativi di Lean (Type) è manuale e soggetto a errori.
• Mancanza di Automazione: Gli strumenti esistenti spesso mancano degli specifici suggerimenti di riscrittura e delle tattiche necessari per rendere le dimostrazioni insiemistiche fluide quanto quelle tipate.

2. Metodologia

L'autore presenta ZFLean, una libreria Lean 4 costruita sopra il modello ZFC esistente di Mathlib. La metodologia si concentra sulla creazione di un calcolo relazionale uniforme e di ponti di interoperabilità per rendere lo sviluppo a livello di insiemi ergonomico.

Scelte Progettuali Fondamentali:

• Fondamenta: Sfrutta l'implementazione di ZFC di Mathlib, che costruisce gli insiemi come quoziente estensionale di "pre-insiemi" induttivi (PSet).
• Calcolo Relazionale: Invece di trattare le funzioni come oggetti totali di prima classe (come nella teoria dei tipi standard), ZFLean le tratta come relazioni funzionali. Introduce un calcolo per relazioni binarie, funzioni parziali e funzioni totali.
• Automazione tramite Tattiche: Il framework introduce tre tattiche leggere (zrel, zpfun, zfun) progettate per scaricare automaticamente le condizioni laterali di correttezza (ad esempio, dimostrare che una composizione è una relazione o una funzione).
• Ponti: La libreria costruisce isomorfismi espliciti (ponti) tra oggetti ZFC canonici (ad esempio ZFBool, ZFNat) e i tipi nativi di Lean (Bool, Nat), permettendo il trasporto di proprietà tra i due mondi.

3. Contributi Chiave

A. Calcolo Relazionale e Automazione

• Definizioni: Formalizza inversa, identità, composizione, dominio, codominio e immagine per le relazioni.
• Funzionalità: Distingue tra funzioni parziali (IsPFunc) e funzioni totali (IsFunc).
• Tattiche:
  • zrel: Scarica gli obiettivi che dimostrano che un insieme è una relazione ($R \subseteq A \times B$).
  • zpfun: Scarica gli obiettivi che dimostrano che un insieme è una funzione parziale.
  • zfun: Scarica gli obiettivi che dimostrano che un insieme è una funzione totale.
  • Queste tattiche utilizzano lemmi contrassegnati da attributi (ad esempio @[zfun]) per risolvere ricorsivamente le condizioni laterali, nascondendo il boilerplate all'utente.
• Notazione: Introduce una sintassi comoda per l'applicazione di funzioni (@zf(x)) e per l'astrazione $\lambda$, con teoremi per la $\beta$-riduzione, l'espansione $\eta$ e l'estensionalità.

B. Costruzioni Canoniche

La libreria fornisce una serie di oggetti matematici standard definiti all'interno di ZFC, completi delle loro proprietà universali:

• Booleani: Un insieme a due elementi $B$ con struttura algebrica (congiunzione, disgiunzione, negazione) e un eliminatore di casi.
• Numeri Naturali ($\mathbb{N}$): Definiti come il più piccolo insieme induttivo (ordini di von Neumann). Include un ricorsore, un principio di induzione e operazioni aritmetiche. Crucialmente, è dotato di una struttura CommSemiring per sfruttare la tattica ring di Lean.
• Interi ($\mathbb{Z}$) e Razionali ($\mathbb{Q}$): Costruiti come tipi quoziente di coppie di naturali/interi, con operazioni sollevate dai rappresentanti.
• Coproductti e Opzioni: Definizioni insiemistiche di tipi somma e tipi opzione.

C. Isomorfismi e Trasporto

• Immissioni e Isomorfismi: Definisce immissioni a livello di insiemi ($A \hookrightarrow_z B$) e isomorfismi ($A \cong_z B$) tramite funzioni iniettive e biiettive.
• Teorema di Cantor-Schröder-Bernstein: Formalizzato all'interno del framework.
• Trasporto: Dimostra che le costruzioni ZFC sono isomorfe ai tipi nativi di Lean (ad esempio ZFBool $\simeq$ Bool). Questo permette agli utenti di "trasportare" teoremi dalla ricca libreria tipata di Mathlib nel contesto insiemistico in modo trasparente.

D. Caso di Studio: Isomorfismo di Currying

Il documento dimostra l'utilità del framework dimostrando l'Isomorfismo di Currying: $C^{A \times B} \cong (C^B)^A$.

• La dimostrazione definisce curryz e uncurryz come funzioni a livello di insiemi.
• Dimostra che sono reciproci usando l'automazione del framework per gestire le condizioni laterali (correttezza delle composizioni e delle immagini).
• Lo script di dimostrazione rispecchia da vicino gli argomenti matematici standard, con il livello di automazione che gestisce la "noiosa" verifica insiemistica.

4. Risultati

• Dimensione dell'Artifatto: La libreria consiste in 8.324 righe di codice Lean e 706 teoremi dimostrati.
• Suddivisione dei Componenti:
  • Calcolo Relazionale: ~2.534 righe di codice (172 teoremi).
  • Naturali: ~1.260 righe di codice (199 teoremi).
  • Immissioni/Isomorfismi: ~1.626 righe di codice (31 teoremi).
• Usabilità: Il caso di studio dimostra che il framework riduce con successo l'attrito della formalizzazione a livello di insiemi. Gli utenti possono scrivere dimostrazioni che assomigliano a argomenti insiemistici standard senza dimostrare manualmente che ogni composizione di relazioni è una relazione valida.
• Interoperabilità: La possibilità di passare tra ZFSet e Type nativo permette il riutilizzo delle tattiche algebriche di Mathlib (come ring) su oggetti insiemistici.

5. Significato

• Ponte tra Fondamenti: ZFLean riconcilia efficacemente le visioni "insiemistica" e "tipata" della matematica all'interno di un singolo assistente di dimostrazione. Permette ai matematici di scegliere il fondamento più naturale per un problema specifico (insiemi estensionali vs tipi costruttivi) senza perdere l'accesso all'automazione dell'ecosistema.
• Ergonomia: Automatizzando le condizioni laterali tediose intrinseche alla teoria degli insiemi (dimostrazioni di appartenenza, correttezza delle relazioni), rende lo sviluppo ZFC in Lean fattibile per i non esperti e pratico per la formalizzazione su larga scala.
• Estendibilità: Il design modulare (calcolo relazionale + oggetti canonici + ponti) permette una facile estensione. Lavori futuri includono la formalizzazione dei numeri reali (tramite successioni di Cauchy o tagli di Dedekind) e analisi di base.
• Confronto: A differenza di Isabelle/ZF (dove la teoria degli insiemi è una logica oggetto separata) o degli sviluppi insiemistici di Rocq (che spesso mancano di una profonda integrazione con l'automazione tipata), ZFLean offre un approccio ibrido che mantiene le dimostrazioni a livello di insiemi sfruttando al contempo l'infrastruttura nativa tipata di Lean.

In conclusione, ZFLean fornisce un framework robusto, ergonomico e interoperabile per fare matematica fondamentale in ZFC all'interno di Lean 4, riducendo con successo la barriera all'ingresso per la formalizzazione insiemistica mantenendo la compatibilità con il più ampio ecosistema Mathlib.