Demostraciones hacia atrás (backward) y hacia adelante (forward) en Lean 4

En Lean 4 existen dos enfoques principales para construir demostraciones: el enfoque hacia atrás (backward) y hacia adelante (forward). Ambos son formas de construir el mismo término de prueba, pero difieren en la dirección en que razona el demostrador. En ocasiones, es útil usar un enfoque híbrido que combine los dos enfoques.

BACKWARD PROOFS (PRUEBAS HACIA ATRÁS)

Una demostración hacia atrás comienza con el objetivo (la conclusión que se quiere probar) y aplica tácticas que transforman ese objetivo en subobjetivos más simples, hasta que todos se cierran con las hipótesis disponibles o con hechos elementales. Es el estilo que se usa típicamente en el modo táctica (by ...), donde el estado de la prueba muestra el objetivo actual y las hipótesis en el contexto.

Las tácticas más representativas de este enfoque son:

• intro: introduce una hipótesis a partir de un objetivo de la forma P → Q o ∀ x, P x. Convierte el objetivo en el consecuente, añadiendo la premisa del objetivo al contexto local.
• apply: aplica una lemma o teorema cuya conclusión coincide con el objetivo, generando nuevos subobjetivos para las premisas de esa lemma. Es la táctica clave del razonamiento hacia atrás.
• exact: cierra el objetivo proporcionando un término de prueba que coincide exactamente con la conclusión. Se usa cuando ya se tiene una hipótesis o un lema que prueba el objetivo sin más pasos.
• rfl: cierra objetivos de la forma a = a (igualdad reflexiva). Lean lo usa para igualdades definicionales.
• constructor: cuando el objetivo es por ejemplo conjunción P ∧ Q, la divide en dos subobjetivos P y Q.
• left / right: para objetivos de disyunción P ∨ Q, eligen cuál de los dos disyuntos probar.
• cases: se usa para realizar análisis de casos sobre tipos inductivos, dividiendo una meta actual en tantos subobjetivos como constructores tenga el tipo de la hipótesis o expresión que se analiza.
• rw: Si tienes una hipótesis o un lema h : a = b, la orden rw [h] busca la primera aparición de a en el objetivo actual y la sustituye por b. También se puede hacer sustitución inversa con rw [← h].

FORWARD PROOFS (PRUEBAS HACIA ADELANTE)

Una demostración hacia adelante parte de lo que ya se conoce (hipótesis, lemas previos, definiciones) y construye paso a paso nuevos hechos hasta alcanzar la conclusión deseada. Se van añadiendo proposiciones intermedias al contexto mediante comandos estructurados o tácticas que generan nuevos términos de prueba. Este estilo refleja la forma más empleada de escribir demostraciones en matemáticas.

Los tácticas más representativas de este enfoque son:

• intro: introduce hipótesis en el contexto. En Lean 4, reemplaza al antiguo assume en modo táctica.
• have: prueba un hecho intermedio y lo añade al contexto con un nombre. Es el comando central del razonamiento hacia adelante: permite establecer lemas auxiliares que luego se usan en la prueba.
• let: define una variable local (puede ser un término, una función o un tipo). A diferencia de have, conserva la definición o el valor, no solo el tipo.
• show: repite el objetivo actual o lo reformula hasta una forma computacionalmente equivalente. Sirve como documentación y para hacer explícito qué se está probando en cada paso.
• calc: permite encadenar igualdades o relaciones transitivas en un formato de cálculo paso a paso, muy útil para demostraciones algebraicas.
• apply … at …: aplica un lema o teorema a una hipótesis existente para generar una nueva hipótesis (razonamiento forward sobre hipótesis).

EJEMPLO

Para ilustrar ambos estilos, consideremos el siguiente teorema sobre conectivas lógicas:

Teorema: Si P → Q y Q → R, entonces P → R.

En el enfoque hacia atrás, trabajamos desde el objetivo P → R hacia las hipótesis.

theorem trans_imp_backward (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) : P → R := by
  intro hP          -- introducimos la hipótesis P para probar R
  apply hQR         -- el objetivo cambia de R a Q
  apply hPQ         -- el objetivo cambia de Q a P
  exact hP          -- cerramos con la hipótesis hP

En el enfoque hacia adelante, partimos de las hipótesis y construimos la conclusión paso a paso.

theorem forward_tactic (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) (hp : P) : R := by
  have hQ : Q := hPQ hp   -- Añadimos Q al contexto.
  have hR : R := hQR hQ   -- Añadimos R al contexto.
  exact hR                -- Cerramos usando el hecho que acabamos de crear.