Preámbulo · Lean desde cero

Lean es una calculadora que juzga

Olvida por un momento las demostraciones. Lean es, antes que nada, una calculadora con una manía: antes de calcular nada, clasifica. Toda expresión que se le escribe recibe primero un tipo, y solo después, si se le pide, un valor. Ese orden (primero el tipo, luego el valor) es todo el secreto del asistente, y este preámbulo lo destapa escribiendo expresiones, no leyendo teoría.

La primera expresión

En matemática se escribe $2 + 2 = 4$ y se piensa « $2 \in \mathbb{N}$ ». Lean separa esas dos ideas en dos órdenes distintas:

#eval 2 + 2    -- 4
#check 2 + 2   -- 2 + 2 : Nat

La orden #eval calcula: responde 4. La orden #check juzga: responde 2 + 2 : Nat, que se lee «la expresión 2 + 2 tiene tipo Nat». Los dos puntos : son la versión de Lean del símbolo de pertenencia: donde el matemático escribe $2 \in \mathbb{N}$ , Lean escribe 2 : Nat.

Nota (∈ contra :)

La analogía es útil pero no es identidad: $\in$ relaciona un elemento con un conjunto que existe por su cuenta; : relaciona una expresión con su tipo, y en Lean toda expresión tiene exactamente un tipo antes de poder usarse. No hay expresiones «sueltas»: si Lean no puede asignar un tipo, rechaza la expresión sin intentar calcular nada. La ruta teórica (niveles 1 y 2) construye esta idea con todo rigor; aquí basta la intuición.

Decir el tipo en voz alta: la ascripción

Casi siempre Lean deduce el tipo solo. Pero se le puede declarar, con la sintaxis (expresión : Tipo), llamada ascripción:

#check (2 + 2 : Nat)   -- 2 + 2 : Nat

Parece redundante, y aquí lo es. Pero guarda esta herramienta: en la página siguiente habrá expresiones cuyo tipo Lean no puede adivinar, y la ascripción será la manera de dárselo. Es exactamente lo que hace un matemático al escribir «sea $f \colon \mathbb{N} \to \mathbb{N}$ » antes de dar la fórmula de $f$ .

La primera sorpresa: la resta de Nat

Pide a Lean que calcule $2 - 5$ :

#eval (2 - 5 : Nat)   -- 0  (¡!)

El resultado es 0, no $-3$ . No es un error: es una decisión de diseño con contenido matemático. El tipo Nat son los naturales $\{0, 1, 2, \dots\}$ ; el $-3$ no existe en ese tipo, y Lean no puede devolver un valor fuera del tipo que juzgó. La resta de Nat es la resta truncada: $a \dot{-} b = \max(0,\, a - b)$ . Si se quieren enteros, se usa otro tipo (Int), con otra resta.

La moraleja importa más que el ejemplo: el tipo se decide antes que el valor, y el valor no puede escaparse del tipo. Un teorema sobre Nat es un teorema sobre esta resta truncada; quien formaliza tiene que saberlo. La tesis explota esta disciplina página tras página.

Los booleanos

Hay más tipos que Nat. Las comparaciones producen valores del tipo Bool, el de los dos valores de verdad computables true y false:

#check 2 + 2 == 5   -- 2 + 2 == 5 : Bool
#eval 2 + 2 == 5    -- false

El doble signo == es la igualdad que se calcula: compara y responde true o false. Existe también un = de un solo signo, el de los enunciados, que no calcula nada y vive en otro tipo; la distinción es importante y tiene su propia página (la quinta). Por ahora: en este laboratorio, ==.

Pruébalo

Todo lo anterior, en vivo. El botón «¿por qué?» muestra la derivación del tipo: la cadena de razones por la que Lean acepta la expresión. Esa cadena de razones, hecha matemática rigurosa, es el corazón de la ruta teórica.

Laboratorio Lean

Un Lean en miniatura: cada expresión pasa por el mismo ciclo que en el asistente real, primero el tipo (#check), después el valor (#eval).

#checkNat

#eval4

Nota (Qué es este laboratorio (y qué no))

El laboratorio implementa un fragmento diminuto de Lean (números, booleanos y las funciones de las páginas siguientes), suficiente para sentir el ciclo juzgar-calcular. No es el Lean completo: no tiene demostraciones, ni tipos definidos por el usuario, ni bibliotecas. Todo lo que muestra, sin embargo, se comporta exactamente como en Lean 4.

Lo que ya sabes

Toda expresión de Lean tiene un tipo, y el tipo se juzga antes de calcular.
#check pregunta el tipo; #eval pide el valor; (e : T) declara el tipo esperado.
El valor nunca se sale del tipo: la resta de Nat trunca en cero.
== calcula un Bool; el = de los enunciados es otra cosa (página 5).

En la página siguiente aparece la expresión más importante de todo Lean: la función anónima fun. Con ella, y con nada más, se construyen desde el sucesor de un número hasta las demostraciones de la tesis.