Nivel 6 · El CIC y Lean

Tácticas: metaprogramas sobre el CIC

Aunque cada prueba en Lean es un término del cálculo lambda tipado, escribir estos términos directamente es impráctico. En su lugar, el trabajo interactivo se realiza mediante tácticas. Las tácticas no son pruebas; son metaprogramas (programas que escriben pruebas) que manipulan el estado de la prueba: cada táctica transforma el contexto (las hipótesis disponibles) y la meta (la proposición por demostrar), construyendo iterativamente el término-prueba subyacente (Avigad et al., 2015) .

Para el lector que no programa en Lean, esta página se resume en una sola idea: una táctica es un metaprograma que construye un término del CIC , y las pocas tácticas estructurales son las construcciones ya vistas. La táctica intro construye una abstracción ($\lambda$, introducción de $\Pi$); apply es la aplicación (eliminación de $\Pi$, el modus ponens); constructor elige un constructor del tipo inductivo (una regla de introducción); y cases/induction son el eliminador y el recursor del tipo. Quien retenga esta correspondencia ya está en condiciones de leer el código Lean del módulo 07; los ejemplos que siguen solo la ilustran en detalle.

intro: la introducción de la implicación y de Pi

Si la meta es una expresión de enlace (un tipo función o un cuantificador), intro mueve el antecedente o la variable cuantificada al contexto local:

• para una meta $\vdash A \to B$, intro h introduce una hipótesis $h : A$ y establece $B$ como nueva meta;
• para una meta $\vdash (x : A) \to B\,x$ (notación $\forall x{:}A,\ B\,x$), intro x introduce un parámetro arbitrario $x : A$ y la meta pasa a ser $\vdash B\,x$.

En ambos casos, intro envuelve el resto de la prueba dentro de una abstracción $\lambda$ (fun ... => ...). Es la correspondencia de Curry–Howard en acción: al introducir una hipótesis o variable, se construye un término-prueba que es una función que la toma como argumento.

theorem id_prop (p : Prop) : p → p := by
  -- Meta: ⊢ p → p
  intro h
  -- Contexto: h : p
  -- Meta: ⊢ p
  exact h
-- Término-prueba construido: fun (h : p) => h

theorem all_id (α : Type) (P : α → Prop) : (∀ x, P x → P x) := by
  -- Meta: ⊢ ∀ x, P x → P x
  intro x
  -- Contexto: x : α          Meta: ⊢ P x → P x
  intro hx
  -- Contexto: x : α, hx : P x    Meta: ⊢ P x
  exact hx
-- Término-prueba construido: fun (x : α) (hx : P x) => hx

constructor: la introducción de propósito general

En Lean, los conectivos $\land$ y $\lor$ no son primitivos: son tipos inductivos de la biblioteca estándar.

inductive And (p q : Prop) : Prop where
  | intro : p → q → And p q

inductive Or (p q : Prop) : Prop where
  | inl : p → Or p q
  | inr : q → Or p q

La táctica constructor intenta resolver la meta aplicando el primer constructor aplicable del tipo inductivo que se intenta probar. Para una meta $\vdash p \land q$ solo hay un constructor, And.intro, que toma una prueba de $p$ y una de $q$: constructor reemplaza la meta por las dos submetas $\vdash p$ y $\vdash q$.

theorem build_and (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq
-- Se aplica And.intro y se resuelven sus dos argumentos

-- Caso 1: se tiene evidencia de p, se usa la rama izquierda
theorem solve_left (p q : Prop) (hp : p) : p ∨ q := by
  left      -- aplica el constructor Or.inl
  exact hp

-- Caso 2: se tiene evidencia de q, se usa la rama derecha
theorem solve_right (p q : Prop) (hq : q) : p ∨ q := by
  right     -- aplica el constructor Or.inr
  exact hq

apply: la eliminación de la implicación (modus ponens)

La táctica apply implementa el razonamiento hacia atrás (backward chaining). Si la meta es $\vdash B$ y existe una hipótesis (o teorema) $h : A \to B$, apply h empata la conclusión $B$ de la hipótesis con la meta y la reemplaza por la premisa $\vdash A$. En términos del CIC, apply prepara una aplicación de función: si el término-prueba de la nueva meta $A$ es $t_A$, el término final para $B$ será $h\ t_A$.

theorem modus_ponens (p q : Prop) (h_imp : p → q) (h_p : p) : q := by
  -- Contexto: h_imp : p → q, h_p : p     Meta: ⊢ q
  apply h_imp
  -- apply reduce la meta q a la premisa de h_imp
  -- Nueva meta: ⊢ p
  exact h_p
-- Término-prueba construido: h_imp h_p

cases: eliminación por casos

La táctica cases implementa la eliminación por casos sobre una hipótesis $h$ de un tipo inductivo: genera una submeta por cada constructor y, en cada rama, reemplaza $h$ por los argumentos de ese constructor. Es la interfaz de alto nivel para el eliminador por casos generado automáticamente, .casesOn. Para Or p q se usa habitualmente la variante Or.elim, de tipo

donde $C$ es la meta; como Or habita $\text{Prop}$, la restricción de eliminación de la página de recursores exige además $C : \text{Prop}$.

theorem or_comm (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  -- Contexto: h : p ∨ q     Meta: ⊢ q ∨ p
  cases h with
  -- cases crea dos ramas, una para Or.inl y otra para Or.inr
  | inl hp =>
    -- Contexto: hp : p      Meta: ⊢ q ∨ p
    exact Or.inr hp
  | inr hq =>
    -- Contexto: hq : q      Meta: ⊢ q ∨ p
    exact Or.inl hq
-- Término-prueba subyacente:
-- fun (h : p ∨ q) =>
--   Or.elim h (fun hp => Or.inr hp) (fun hq => Or.inl hq)

induction: la interfaz para Nat.rec

Cuando se define Nat, Lean no solo genera sus constructores sino también su recursor Nat.rec, que es el principio de inducción matemática codificado como término del CIC. Su tipo (simplificado) es

donde $P$ es el motive. El nivel de universo $u$ determina la naturaleza de la operación: si $u = 0$ ($\text{Sort } 0 = \text{Prop}$), $P$ es un predicado y el recursor representa una prueba por inducción matemática; si $u \ge 1$, $P$ es una familia de tipos de datos y el recursor define funciones por recursión primitiva. La táctica induction es la interfaz de alto nivel que aplica Nat.rec a la meta actual.

theorem zero_plus_n_eq_n (n : Nat) : 0 + n = n := by
  -- Meta: ⊢ 0 + n = n     (el motive P es fun n => 0 + n = n)
  induction n with
  -- induction genera dos metas: caso base y paso inductivo
  | zero =>
    -- Meta: ⊢ 0 + 0 = 0
    rfl
  | succ k ih =>
    -- Contexto: k : Nat, ih : 0 + k = k   (hipótesis de inducción)
    -- Meta: ⊢ 0 + (k + 1) = k + 1
    rw [Nat.add_succ, ih]
-- Término-prueba subyacente (aproximado):
-- @Nat.rec (fun n => 0 + n = n)   -- el motive P
--   rfl                            -- prueba de P 0
--   (fun k ih => by rw [Nat.add_succ, ih])  -- prueba de P k → P (k+1)
--   n

¿Por qué rfl pudo resolver la meta $\vdash 0 + 0 = 0$ en el caso base? La respuesta revela la conexión más profunda entre prueba y computación en Lean. La táctica rfl prueba una meta $a = b$ si y solo si $a$ y $b$ son definicionalmente iguales: una igualdad que el núcleo verifica computando, reduciendo ambos términos a su forma normal . Las reglas de reducción del núcleo incluyen la reducción $\beta$ y, crucialmente, la reducción $\iota$ de la página anterior. La suma Nat.add se define internamente mediante Nat.rec; sus ecuaciones se validan desplegando la definición ($\delta$) y aplicando $\beta$ e $\iota$ sobre Nat.rec, de donde 0 + 0 se computa a 0. La meta se convierte definicionalmente en $\vdash 0 = 0$ y rfl tiene éxito. En el paso inductivo, rw [Nat.add_succ, ih] usa Nat.add_succ, un lema que expone la regla del caso succ como igualdad proposicional ($\forall m\, n,\ m + (n+1) = (m+n)+1$), para reescribir la meta, que luego resuelve la hipótesis de inducción ih.

Síntesis: del CIC a la formalización

Los elementos de este módulo sostienen la formalización del módulo 07. Allí, la lógica proposicional se realiza dentro del CIC, y cada noción matemática tiene una contraparte exacta:

• la sintaxis de las fórmulas es un tipo inductivo (con $\bot$, $\neg$ y $\to$ como constructores) y su evaluación semántica se define por el recursor asociado;
• la relación de derivabilidad $\Gamma \vdash_{\mathrm{ND}} \varphi$ es un predicado inductivo en $\text{Prop}$ cuyos constructores son las reglas de inferencia de la deducción natural ; como el tipo es el menor punto fijo cerrado bajo ellas, toda derivación es un término construido con esos constructores, y «razonar por inducción sobre una derivación» es aplicar su recursor;
• la corrección y la completitud son metateoremas: términos que habitan los $\Pi$-tipos correspondientes y cuya verificación delega en el núcleo.

Así, la correspondencia de Curry–Howard deja de ser una analogía y pasa a ser el formato de trabajo: demostrar el teorema de completitud consistirá en construir un término del CIC y dejar que el núcleo lo verifique.