Reglas de eliminación de los tipos inductivos en Lean 4

En el post sobre Lean como lenguaje de tipos vimos que los tipos inductivos son la construcción para definir nuevos tipos de datos y que se especifican enumerando sus constructores, que son las formas básicas de construir elementos del tipo. Además, cuentan con las reglas de eliminación, que son el mecanismo fundamental que permite definir funciones por recursión y demostrar propiedades por inducción. Estas reglas se materializan en los recursers (o eliminadores) que Lean genera automáticamente a partir de la definición de cada tipo inductivo.

La terminación de las funciones recursivas se justifica traduciéndolas a usos del recursor, de modo que el kernel de Lean solo necesita verificar aplicaciones del recursor, sin un análisis de terminación separado.

Un recursor tiene la siguiente forma general para un tipo inductivo T con constructores c₁, ..., cₙ:

T.rec : {motive : T → Sort u} →
        (caso para c₁) → ... → (caso para cₙ) → (t : T) → motive t

El motive es una familia T → Sort u; es el tipo de resultado en el uso final que haces del tipo para cada t : T (una propiedad, si Sort u es Prop, o un tipo de datos, si Sort u es Type).

Para poder construir el resultado final, debes explicarle al recursor qué hacer en cada uno de los escenarios posibles:

• Constructores base (sin recursión): Si el constructor no contiene elementos de tipo T, el argumento esperado es simplemente una regla o valor que produzca motive (cᵢ ...).
• Constructores inductivos / recursivos: Si el constructor toma un elemento previo de tipo T (por ejemplo, el predecesor en los números naturales), Lean te proporcionará automáticamente la hipótesis de inducción (o el resultado de la llamada recursiva) como un argumento adicional dentro de ese caso.

Finalmente, tras proveer el motivo y las reglas para cada constructor, el recursor se convierte en una función lista para usarse. Recibe un elemento t de tipo T y te devuelve el motivo aplicado a ese t (la demostración final o el valor calculado).

Ejemplo con números naturales

Vamos a ver un ejemplo con el tipo Nat, que se define con dos constructores: zero y succ. Su recursor Nat.rec tiene el siguiente tipo (verificado con #check Nat.rec):

Nat.rec : {motive : Nat → Sort u} 
        → motive Nat.zero 
        → ((n : Nat) → motive n → motive (Nat.succ n)) 
        → (t : Nat) 
        → motive t

Definir una función por recursión usando el recursor

Podemos definir la suma de dos naturales usando directamente Nat.rec:

def suma (m n : Nat) : Nat :=
  Nat.rec (motive := fun _ => Nat)
          m                    -- caso base: n = 0 → m
          (fun _ ih => ih + 1) -- paso: n+1 → (m+n)+1
          n

Aquí motive es constante (fun _ => Nat) porque el resultado no depende de n. Esta es la forma no dependiente del recursor. 

Demostrar una propiedad por inducción

Para demostrar que 0 + n = n para todo n, podemos usar el recursor con un motive proposicional:

theorem cero_suma (n : Nat) : 0 + n = n :=
  Nat.rec (motive := fun n => 0 + n = n)
          rfl                          -- caso base: 0 + 0 = 0
          (fun n ih => congrArg Nat.succ ih) -- paso: si 0+n=n, entonces 0+(n+1)=n+1
          n

Tenemos:

• motive: La propiedad 0 + n = n
• caso para cero: Una demostración de que P 0 es verdadero (caso base). Usa la propiedad reflexiva rfl.
• caso para succ: Una función que toma un número n, la hipótesis de inducción P n, y devuelve una demostración de P (n + 1) (paso inductivo). Si ih demuestra que A = B, entonces congrArg Nat.succ ih genera automáticamente una demostración de que Nat.succ A = Nat.succ B.

En el uso normal de Lean 4, pocas veces escribirás T.rec directamente, ya que las tácticas como induction, cases o el propio sistema de pattern matching (coincidencia de patrones) actúan como una capa de abstracción más cómoda sobre este recursor subyacente e infieren el motivo.

Resumiendo, el tipo inductivo T define la estructura de los datos, el recursor T.rec es el motor de eliminación/recursión sobre esa estructura y el motive es el destino final al que quieres llegar en un uso concreto.