Preámbulo · Lean desde cero

Demostrar es programar

La página anterior dejó una pregunta abierta. Si un enunciado como $p \to q$ es un tipo, ¿qué es entonces una función de tipo p → q? Esta página da la respuesta, que es la idea más hermosa de todo el edificio: esa función es una demostración. Y no hará falta aprender nada nuevo: las expresiones son las mismas fun de la página 2.

El primer teorema

En Lean, un teorema se declara con su enunciado como tipo y su demostración como expresión:

example (p : Prop) : p → p :=
  fun h => h

Léase con calma, porque aquí está todo:

• (p : Prop) introduce una proposición arbitraria $p$: «sea $p$ una proposición».
• El enunciado es el tipo p → p: «$p$ implica $p$».
• La demostración, tras el :=, es la expresión fun h => h: la función identidad.

¿Por qué funciona? Una prueba de p → p debe ser una función que reciba una prueba de $p$ y devuelva una prueba de $p$. La identidad hace exactamente eso: recibe h (léase «la hipótesis») y la devuelve intacta. Es palabra por palabra la prueba del cuaderno: «supóngase $p$; entonces $p$». La suposición es el binder fun h =>; el «entonces» es el cuerpo.

Modus ponens: aplicar es deducir

El segundo teorema del repertorio clásico: de $p \to q$ y $p$ se deduce $q$.

example (p q : Prop) : (p → q) → p → q :=
  fun hpq hp => hpq hp

La demostración es fun hpq hp => hpq hp, y su cuerpo es una aplicación de función, la operación de la página 2. Si hpq es una prueba de $p \to q$ (una función de pruebas de $p$ a pruebas de $q$) y hp es una prueba de $p$, entonces hpq hp es una prueba de $q$. El modus ponens, la regla de inferencia más antigua de la lógica, es la aplicación de funciones. La flecha se consume igual que cuando (fun (x : Nat) => x + 1) 41 consumía Nat → Nat para dar Nat.

theorem modus_ponens (p q : Prop) (hpq : p → q) (hp : p) : q :=
  hpq hp

La conjunción: pruebas que son pares

¿Y $p \wedge q$? Una prueba de una conjunción es un par de pruebas: una de $p$ y una de $q$. Lean lo escribe con And.intro, o con la notación de par anónimo ⟨·, ·⟩, y las dos componentes se extraen con .1 y .2:

example (p q : Prop) : p ∧ q → q ∧ p :=
  fun h => ⟨h.2, h.1⟩

La conmutatividad de la conjunción, uno de los primeros teoremas de cualquier curso de lógica, es intercambiar las componentes de un par. Nada más. La demostración recibe el par h, y devuelve el par con h.2 (la prueba de $q$) primero y h.1 (la de $p$) después.

Qué verifica Lean exactamente

Cuando Lean acepta example (p : Prop) : p → p := fun h => h, lo que hace es comprobar un tipo: verifica que la expresión fun h => h tiene el tipo p → p, con las mismas reglas de derivación que el laboratorio mostraba para fun (x : Nat) => x + 1 : Nat → Nat. No hay un «módulo de lógica» aparte: demostrar un teorema y tipar una expresión son la misma operación del mismo núcleo. Por eso una prueba aceptada no depende de la buena fe de nadie: o el término tiene el tipo, o no lo tiene.

Lo que ya sabes

• Un teorema se declara theorem nombre : Enunciado := demostración, donde el enunciado es un tipo y la demostración una expresión.
• fun h => h demuestra $p \to p$; la aplicación hpq hp es el modus ponens; el par ⟨h.2, h.1⟩ conmuta la conjunción.
• Verificar una demostración = comprobar el tipo de una expresión. Ni más ni menos.

Escribir estas expresiones a mano se vuelve tedioso en cuanto las pruebas crecen. La página siguiente presenta el modo interactivo de Lean: las tácticas, órdenes que construyen estas mismas expresiones paso a paso mientras Lean muestra qué falta por demostrar.