Tus primeras demostraciones en Lean

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

El primer artículo de esta serie explicó la correspondencia de Curry-Howard: las proposiciones son tipos, las demostraciones son programas. El segundo construyó un demostrador de teoremas (theorem prover) diminuto desde cero en Python. El tercero metió las mismas ideas dentro del sistema de tipos de Julia.

Ahora usamos la herramienta de verdad. Este artículo toma exactamente los mismos teoremas que demostraste a mano en Python y los muestra en Lean 4. Vas a ver qué cambia y qué queda igual: la sintaxis se mueve, la lógica no.

#Los mismos tres teoremas

En el artículo de Python demostramos tres cosas:

1. A -> A (si A, entonces A)
2. A -> B -> A (si A y B, entonces A)
3. (A -> B) -> (B -> C) -> A -> C (composición de implicaciones)

Armamos cada demostración como un término lambda y se lo pasamos a un type checker de 30 líneas. Si el checker aceptaba el término, la demostración era válida.

Lean funciona igual. La diferencia es que el kernel de Lean es mucho más potente, y encima tiene capas de automatización. Pero por debajo sigue siendo lo mismo: construir un término, verificar su tipo.

#Demostración 1: A -> A

En Python, la demostración era:

identity = Lam("x", A, Var("x"))
# inferred type: Arrow(Atom("A"), Atom("A"))

En Lean:

theorem identity (A : Prop) : A -> A :=
  fun hA => hA

Misma estructura. fun hA => hA es una lambda que toma evidencia de A y la devuelve. El tipo A -> A es a la vez la firma de la función y la afirmación lógica. El término es a la vez el programa y la demostración.

En el demostrador de Python teníamos que llamar a infer({}, identity) para verificar la demostración. En Lean, escribir theorem dispara el type checker automáticamente. Si el término no habita el tipo afirmado, el archivo no compila.

#Demostración 2: A -> B -> A

En Python:

proof = Lam("x", A, Lam("y", B, Var("x")))
# inferred type: Arrow(A, Arrow(B, A))

En Lean:

theorem keep_first (A B : Prop) : A -> B -> A :=
  fun hA _hB => hA

Ignorá la segunda hipótesis y devolvé la primera. El término de prueba tiene exactamente la misma estructura que la versión en Python. La única diferencia es la sintaxis: fun en lugar de Lam, => en lugar de una coma, guiones bajos para las variables que no se usan.

La misma demostración como demostración con tácticas (tactic proof):

theorem keep_first_tac (A B : Prop) : A -> B -> A := by
  intro hA
  intro _hB
  exact hA

• intro hA mueve la primera hipótesis del objetivo (goal) al contexto local
• intro _hB mueve la segunda
• exact hA cierra el objetivo con un término que ya está en el contexto

El demostrador de Python no tiene sistema de tácticas. O escribís el término de prueba o no escribís nada. Lean te da las dos opciones: escribir el término directamente, o usar tácticas para construirlo paso a paso. Las tácticas escalan a demostraciones largas de una forma en que la construcción de términos no escala.

#Demostración 3: (A -> B) -> (B -> C) -> A -> C

Esta era la demostración más compleja del artículo de Python:

compose = Lam(
    "f", Arrow(A, B),
    Lam(
        "g", Arrow(B, C),
        Lam(
            "x", A,
            App(Var("g"), App(Var("f"), Var("x")))
        )
    )
)

En Lean:

theorem compose (A B C : Prop) : (A -> B) -> (B -> C) -> A -> C :=
  fun hAB hBC hA => hBC (hAB hA)

En Lean, la aplicación de funciones es simplemente yuxtaposición: hAB hA aplica hAB a hA. No hace falta el envoltorio App(Var("f"), Var("x")). La demostración entra en una línea en lugar de ser un árbol anidado.

La versión con tácticas:

theorem compose_tac (A B C : Prop) : (A -> B) -> (B -> C) -> A -> C := by
  intro hAB hBC hA
  apply hBC
  apply hAB
  exact hA

Acá apply trabaja hacia atrás desde el objetivo. El objetivo es C. apply hBC dice “tengo B -> C, así que si puedo demostrar B, terminé”. Ahora el objetivo pasa a ser B. apply hAB dice “tengo A -> B, así que si puedo demostrar A, terminé”. Ahora el objetivo pasa a ser A. exact hA lo cierra.

Trabajar hacia atrás desde el objetivo es un modismo de las tácticas que no tiene equivalente en el demostrador de Python. Es una de las cosas que hacen que las demostraciones en Lean sean más naturales que construir términos a mano.

#Lo que acabás de ver

Demostraste tres teoremas en dos sistemas. La lógica es la misma. El checker es el mismo tipo de máquina. Pero Lean te da:

• Una sintaxis más limpia. fun hA => hA en lugar de Lam("x", A, Var("x")).
• Tácticas. intro, exact y apply te dejan construir demostraciones paso a paso en lugar de escribir el término entero de una.
• Razonamiento hacia atrás. apply te deja trabajar desde el objetivo hacia las hipótesis, que muchas veces es más natural que la construcción hacia adelante.

#Más allá de la implicación: igualdad y cómputo

El demostrador de Python maneja solamente la implicación. No puede hablar de igualdad, de números ni de cómputo dentro de los tipos. Lean sí.

theorem one_plus_one : 1 + 1 = 2 := by
  rfl

rfl significa reflexividad: los dos lados se reducen a la misma forma normal, así que la igualdad vale por cómputo. Lean evalúa 1 + 1 a 2, ve que los dos lados son idénticos y cierra el objetivo.

Esta es una de las ideas más importantes de Lean. Gran parte de demostrar no es razonamiento profundo sino llevar los dos lados de un enunciado a formas que la maquinaria de reducción de Lean pueda reconocer como iguales. En el artículo de Julia, demostrar 1 + 1 = 2 llevó cuatro pasos de encadenar axiomas a mano. En Lean, rfl dispara la reducción del kernel y cierra el objetivo.

#Reescritura

Cuando rfl no alcanza, podés reescribir una igualdad en otra.

theorem add_zero_twice (n : Nat) : (n + 0) + 0 = n := by
  rw [Nat.add_zero]

rw significa: usar una igualdad como regla de reescritura. Nat.add_zero es el lema que dice que n + 0 = n. Lean lo aplica a todos los subtérminos del objetivo que coinciden y lo cierra en un solo paso.

Acá es donde Lean empieza a sentirse menos como programar y más como transformación simbólica. Aplicás igualdades ya demostradas para transformar el objetivo.

#Simplificación

Reescribir una y otra vez se vuelve tedioso. simp es el simplificador de propósito general de Lean.

theorem add_zero_twice_simp (n : Nat) : (n + 0) + 0 = n := by
  simp

simp aplica automáticamente una gran colección de lemas de simplificación conocidos. Este es el primer punto donde la distancia entre un demostrador de juguete y Lean se vuelve inconfundible. En el demostrador de Python hacés todo a mano. En el artículo de Julia, cada paso es una cadena de axiomas manual. En Lean, simp se encarga del laburo rutinario.

#Inducción

Para propiedades que valen para todos los números naturales, necesitás inducción.

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero =>
      rfl
  | succ n ih =>
      simp

induction n with divide la demostración en:

• el caso zero
• el caso succ, donde obtenés una hipótesis inductiva ih

Eso es inducción matemática en forma ejecutable: caso base, después paso inductivo.

Este es el momento en que los artículos anteriores deberían encajar:

• En el artículo de Python no podíamos hacer inducción para nada. El demostrador solo manejaba lógica proposicional.
• En el artículo de Julia, la inducción se veía como recursión sobre tipos Nat, y cada paso era una cadena de axiomas manual.
• En Lean, induction es una táctica incorporada, y simp se encarga de los casos rutinarios. La misma idea, pero sin el trabajo mecánico pesado.

#Qué hace que Lean se sienta distinto a programar

Trabajar en Lean se parece menos a escribir código y más a ir dirigiéndote hacia un blanco que la herramienta te mantiene adelante. El objetivo siempre está a la vista: estás tratando de habitar un tipo específico, y en cada paso Lean te muestra lo que falta demostrar. Las hipótesis que tenés en el contexto suelen importar más que el orden de los comandos que escribiste. Y las tácticas de alto nivel, rfl, rw, simp, induction, terminan todas en un término de prueba verificado contra un kernel chico, la misma arquitectura que los demostradores de Python y Julia de antes en esta serie, con herramientas mucho mejores encima. El cambio mental es pasar de seguir cómo corre el código a preguntarte qué contaría como evidencia de que un enunciado vale.

#Una buena forma de aprender

Aprendé Lean leyendo objetivos, no memorizando tácticas.

1. Mirá el objetivo.
2. Preguntate qué forma de término lo habitaría.
3. Usá las tácticas solo para ayudarte a construir ese término.

Entonces, cuando ves:

⊢ A -> B -> A

tendrías que pensar:

• Esto es una implicación, así que probablemente necesito intro
• Después de dos intro, debería tener A en el contexto
• Después, exact con esa hipótesis

Esto ya lo sabés por el artículo de Python. El término de prueba es fun hA _hB => hA. Las tácticas son solo una interfaz para construir ese mismo término de a poco.

#Por dónde seguir

Después de estas primeras demostraciones, lo siguiente que vale la pena aprender es:

• cases para separar en casos sobre datos inductivos
• constructor para construir demostraciones estructuradas
• have para introducir lemas intermedios
• apply para trabajar hacia atrás desde el objetivo
• omega para resolver aritmética lineal automáticamente
• simp y rw, lo suficientemente bien como para que las demostraciones aritméticas dejen de sentirse manuales

A esa altura Lean se vuelve agradable de usar.

Una vez que ves las demostraciones como construcciones tipadas y no como ceremonia, las tácticas de Lean se vuelven predecibles. Y si seguiste esta serie desde el principio, ya tenés ese modelo mental. El demostrador de Python te dio la arquitectura. El demostrador de Julia te dio la frontera de confianza. Lean te da la automatización para trabajar a escala.

La dificultad es la misma que la de programar: los detalles exigen precisión.