Nivel 8 · Quicksort verificado (experto)

Ejemplos y auditoría

Ejemplos resueltos

Como $\mathsf{qsort}$ es una función computable ordinaria, se puede tanto ejecutar como probar hechos sobre entradas concretas especializando los teoremas generales, sin recomputar ni usar decide. De Thesis/Sort/Examples.lean:

open List

-- Ejecutar quicksort sobre entradas concretas (evaluadas por el compilador).
#eval quicksort [3, 1, 2]            -- [1, 2, 3]
#eval quicksort [5, 5, 1, 4, 1, 3]   -- [1, 1, 3, 4, 5, 5]
#eval quicksort ([] : List Nat)      -- []
#eval quicksort [2, 1, 2, 1]         -- [1, 1, 2, 2]  (se conservan los duplicados)

-- Los teoremas generales se especializan a cualquier lista concreta, sin trabajo extra.
example : quicksort [3, 1, 2] ~ [3, 1, 2] := quicksort_perm _
example : Sorted (quicksort [5, 5, 1, 4, 1, 3]) := quicksort_sorted _
example : quicksort [1, 2, 3, 4] ~ [1, 2, 3, 4] ∧ Sorted (quicksort [1, 2, 3, 4]) :=
  quicksort_correct _

Los example merecen atención: la prueba de cada hecho concreto es el teorema general aplicado a un guion bajo. No hay cómputo de casos, no hay decide, no hay verificación por fuerza bruta: el Teorema 12.12 vale para toda lista, así que instanciar $\ell:=[3,1,2]$ es un paso de aplicación de función. El ejemplo [2, 1, 2, 1] ↦ [1, 1, 2, 2] ilustra además que quicksort es una permutación, no una deduplicación: ambas copias de cada valor sobreviven, que es exactamente lo que garantiza el Teorema 12.8.

La auditoría de axiomas

Una prueba formal es tan confiable como sus supuestos ocultos. Deben excluirse dos modos de fallo: una laguna admitida (sorry, que aflora como el pseudo-axioma sorryAx) y un lema postulado en silencio. El comando #print axioms de Lean informa la dependencia transitiva completa de axiomas de un teorema. Ejecutado sobre el resultado principal, en Thesis/Sort/Audit.lean, arroja:

#print axioms quicksort_correct
-- 'quicksort_correct' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms quicksort_perm
-- 'quicksort_perm' depends on axioms: [propext, Classical.choice, Quot.sound]
#print axioms quicksort_sorted
-- 'quicksort_sorted' depends on axioms: [propext, Classical.choice, Quot.sound]

Los tres axiomas reportados, a saber, propext (extensionalidad proposicional), Classical.choice (elección) y Quot.sound (corrección de los cocientes), son los mismos fundamentos clásicos estándar que sostienen el

del módulo anterior y todo Mathlib; no son específicos de este desarrollo. Y, lo más importante, sorryAx no aparece: no hay lagunas admitidas, ni se usa ningún lema de ordenamiento o de corrección postulado. Este es el certificado formal de que el

es exactamente lo que afirma ser. La auditoría de axiomas cierra así el mismo circuito de confianza que en el caso de la lógica.

Conclusión: una lógica y un algoritmo

Se ha dado una demostración completa, verificada por el núcleo, de que el quicksort funcional cumple la especificación de un algoritmo de ordenamiento:

El argumento tuvo tres ingredientes matemáticamente distintos, cada uno reflejado con exactitud en Lean: la terminación por la medida de longitud, la propiedad de permutación vía el lema de partición por filtro y las propiedades de congruencia y «del medio» de $\sim$, y la propiedad de ordenamiento vía las cotas de separación de la partición, el comportamiento de $\mathrm{Pairwise}$ bajo la concatenación y la transitividad del orden.

Con este módulo se cierra la ruta completa. El mismo principio de «pruebas como términos» de la correspondencia de Curry–Howard , montado sobre el CIC y auditado con #print axioms, certificó primero una lógica (la completitud proposicional del módulo 7) y ahora un algoritmo. En Lean la frontera entre programa y prueba desaparece: la función quicksort es un programa ejecutable y, a la vez, los teoremas que la acompañan son términos del mismo cálculo, verificados por el núcleo, tal como prometía la visión de Avigad et al. (2015) y como ilustran a mayor escala Gonthier (2008) y Leroy (2023) . Como control adicional, el desarrollo de la tesis fue validado de forma cruzada con la herramienta Aristotle, que reprodujo las pruebas de manera independiente.

Quien haya llegado hasta aquí puede ahora leer el repositorio lean_execution completo de principio a fin, reproducir la auditoría de axiomas con #print axioms sobre cualquiera de sus teoremas, y, con la plantilla de este módulo, emprender su propia verificación: elegir un algoritmo, escribir su especificación completa y dejar que el núcleo exija el resto.