Preámbulo · Lean desde cero

Tácticas: el modo interactivo

Escribir términos a mano, como en la página anterior, funciona mientras las pruebas caben en una línea. En cuanto crecen, se vuelve tedioso: hay que tener toda la expresión en la cabeza antes de escribir el primer símbolo. Lean ofrece un segundo modo de trabajo, el que se usa en la práctica diaria: tras el := se escribe la palabra by, y a partir de ahí ya no se escribe la demostración, sino órdenes que la construyen. Esas órdenes se llaman tácticas.

El estado de la meta

Al entrar en modo táctico, Lean muestra en todo momento el estado de la meta: arriba las hipótesis disponibles (cada una con su nombre y su tipo) y abajo, tras el símbolo ⊢, lo que falta por demostrar. Ese panel es el «infoview», la ventana que acompaña a quien formaliza:

p q : Prop
hpq : p → q
⊢ p → q

Se lee como el estado de un cuaderno a media prueba: «se tienen $p$ y $q$ proposiciones, y una hipótesis hpq de que $p \to q$; falta demostrar $p \to q$». Cada táctica transforma este estado, y la prueba termina cuando no queda ninguna meta.

Las tres tácticas esenciales

Con tres tácticas basta para todo este preámbulo, y cada una tiene su traducción exacta al lenguaje de términos de la página 6:

• intro h: «supóngase h». Si la meta es una implicación a → b, la táctica mueve el antecedente a las hipótesis con el nombre h y deja como meta b. En el término, es abrir un fun h => ….
• exact e: «esto lo demuestra exactamente». La expresión e debe tener el tipo de la meta; la táctica la coloca y cierra la meta. En el término, es rellenar el hueco pendiente con e.
• apply f: «basta demostrar la premisa de f». Si f prueba a → b y la meta es b, la táctica deja como nueva meta a. En el término, es escribir la aplicación f ?_ con un hueco ?_ por rellenar.

El mismo teorema, dos veces

El modus ponens de la página 6, en sus dos presentaciones:

-- Modo término (página 6)
example (p q : Prop) : (p → q) → p → q :=
  fun hpq hp => hpq hp

-- Modo táctico (esta página)
example (p q : Prop) : (p → q) → p → q := by
  intro hpq
  intro hp
  exact hpq hp

La correspondencia es línea a línea: cada intro es uno de los binders del fun, y el exact final es el cuerpo hpq hp. Al terminar el guion táctico, Lean tiene en las manos exactamente el término fun hpq hp => hpq hp, y lo verifica con las mismas reglas de tipado de siempre.

Para el matemático, el atractivo es que un guion táctico se lee como un cuaderno: «supóngase $p \to q$; supóngase $p$; entonces $q$, exactamente por modus ponens». El estilo declarativo de la prueba de pizarra y el estilo interactivo del asistente son el mismo texto con distinta ortografía.

El visor de metas

El simulador siguiente reproduce el infoview para tres guiones curados. A la izquierda, el estado de la meta tras cada táctica; a la derecha, el término en construcción, con ?_ marcando los huecos pendientes. Conviene recorrer los tres, paso a paso, mirando las dos columnas a la vez: es la mejor manera de interiorizar que táctica y término son la misma prueba.

example (p q : Prop) : (p → q) → p → q := by

Lo que ya sabes

• by entra en modo táctico: Lean muestra hipótesis arriba y meta tras ⊢ abajo, y las tácticas transforman ese estado hasta que no quedan metas.
• intro h supone (abre un fun h =>); exact e cierra la meta con e; apply f reduce la meta a la premisa de f (una aplicación con hueco).
• Las tácticas son programas que escriben el término: la prueba verificada es el mismo término de la página 6, no una lógica aparte.

Con esto queda cubierto todo el vocabulario necesario. La página siguiente no enseña nada nuevo: toma el enunciado de un teorema real de la tesis y lo lee, símbolo por símbolo, solo con lo visto en este preámbulo.