Nivel 8 · Quicksort verificado (experto)

Corrección I: permutación

La primera mitad de la

afirma que la salida de quicksort contiene exactamente los mismos elementos que la entrada, con las mismas multiplicidades. Primero se registra el único hecho combinatorio sobre el filtrado que la prueba necesita: partir una lista por una prueba booleana y concatenar las dos mitades es una permutación de la original.

Lema 12.7 (La partición por filtro es una permutación)

Para toda prueba booleana $q$ y lista $\ell$ ,

\mathsf{filter}(q)(\ell)\ +\!\!+\ \mathsf{filter}(\lambda x.\,\neg q\,x)(\ell)\ \ \sim\ \ \ell.

Demostración.

A probar: $\mathsf{filter}(q)(\ell) +\!\!+\, \mathsf{filter}(q^{c})(\ell)\sim\ell$ , donde se abrevia $q^{c}:=\lambda x.\,\neg q\,x$ . Por inducción sobre $\ell$ .

$\ell=[\,]$ . Ambos filtrados son $[\,]$ , luego $[\,] +\!\!+\, [\,]=[\,]\sim[\,]$ por reflexividad.
$\ell=a::\ell'$ . Se distingue según $q\,a$ $q a$ .
- Si $q\,a$ se cumple: $\mathsf{filter}(q)(a::\ell')=a::\mathsf{filter}(q)(\ell')$ y $\mathsf{filter}(q^{c})(a::\ell')=\mathsf{filter}(q^{c})(\ell')$ , de modo que $\mathsf{filter}(q)(a::\ell') +\!\!+\, \mathsf{filter}(q^{c})(a::\ell') = a::\big(\mathsf{filter}(q)(\ell') +\!\!+\, \mathsf{filter}(q^{c})(\ell')\big) \ \overset{\text{HI}}{\sim}\ a::\ell'.$
- Si $q\,a$ falla: $\mathsf{filter}(q)(a::\ell')=\mathsf{filter}(q)(\ell')$ y $\mathsf{filter}(q^{c})(a::\ell')=a::\mathsf{filter}(q^{c})(\ell')$ , de modo que la concatenación es $\mathsf{filter}(q)(\ell') +\!\!+\, \big(a::\mathsf{filter}(q^{c})(\ell')\big)$ . Trasladar $a$ al frente es una permutación (las transposiciones adyacentes generan $\sim$ ), y se aplica la hipótesis de inducción: $\mathsf{filter}(q)(\ell') +\!\!+\, \big(a::\mathsf{filter}(q^{c})(\ell')\big) \ \sim\ a::\big(\mathsf{filter}(q)(\ell') +\!\!+\, \mathsf{filter}(q^{c})(\ell')\big) \ \overset{\text{HI}}{\sim}\ a::\ell'.$

El teorema de permutación

Teorema 12.8 (Permutación)

Para toda lista $\ell$ , $\ \mathsf{qsort}(\ell)\sim\ell$ .

Demostración.

A probar: $\mathsf{qsort}(\ell)\sim\ell$ . Por inducción bien fundamentada sobre $|\ell|$ (legítima por la Proposición 12.6).

$\ell=[\,]$ . $\mathsf{qsort}([\,])=[\,]\sim[\,]$ por reflexividad.
$\ell=p::r$ . Las dos llamadas recursivas son sobre $\ell_{\leq}$ y $\ell_{>}$ , ambas más cortas que $p::r$ (Proposición 12.6); la hipótesis de inducción da entonces $\mathsf{qsort}(\ell_{\leq})\sim\ell_{\leq}$ y $\mathsf{qsort}(\ell_{>})\sim\ell_{>}$ . Se encadenan tres permutaciones por transitividad: $\begin{aligned} \mathsf{qsort}(p::r)=\mathsf{qsort}(\ell_{\leq}) +\!\!+\, \big(p::\mathsf{qsort}(\ell_{>})\big) &\ \sim\ \ell_{\leq} +\!\!+\, \big(p::\ell_{>}\big) \\ &\ \sim\ p::(\ell_{\leq} +\!\!+\, \ell_{>}) \\ &\ \sim\ p::r. \end{aligned}$ La primera permutación es la congruencia de $\sim$ para $+\!\!+$ y $::$ aplicada a las dos hipótesis de inducción; la segunda es la permutación «del medio», que lleva el pivote $p$ al frente; y la tercera aplica el Lema 12.7 bajo la cabeza $p$ , pues $\ell_{\leq} +\!\!+\, \ell_{>}\sim r$ . Por transitividad, $\mathsf{qsort}(p::r)\sim p::r$ .

Corolario 12.9 (Se preserva la pertenencia)

Para todo $a$ y $\ell$ , $\ a\in\mathsf{qsort}(\ell)\leftrightarrow a\in\ell$ .

Demostración.

A probar: $a\in\mathsf{qsort}(\ell)\leftrightarrow a\in\ell$ . Por el Teorema 12.8, $\mathsf{qsort}(\ell)\sim\ell$ ; y dos listas permutadas contienen exactamente los mismos elementos (con las mismas multiplicidades), de donde, en particular, $a\in\mathsf{qsort}(\ell)\leftrightarrow a\in\ell$ .

Este corolario, en apariencia modesto, es el puente hacia la mitad de ordenamiento: permitirá transportar la pertenencia a las salidas recursivas de vuelta a las mitades de la partición, donde la prueba del filtro da las cotas contra el pivote.

Lean

La prueba en Thesis/Sort/Quicksort.lean sigue la matemática línea por línea. Los dos have son las hipótesis de inducción (llamadas recursivas sobre las mitades más cortas); ih1.append (ih2.cons p) es el paso de congruencia; perm_middle lleva el pivote al frente; y filter_append_perm es el Lema 12.7.

theorem quicksort_perm : ∀ l : List α, quicksort l ~ l
  | [] => by simp
  | p :: rest => by
      rw [quicksort_cons]
      -- las llamadas recursivas permutan las dos mitades de la partición
      have ih1 : quicksort (rest.filter (fun x => decide (x ≤ p)))
            ~ rest.filter (fun x => decide (x ≤ p)) := quicksort_perm _
      have ih2 : quicksort (rest.filter (fun x => ! decide (x ≤ p)))
            ~ rest.filter (fun x => ! decide (x ≤ p)) := quicksort_perm _
      -- pegar las mitades en torno al pivote y recombinar los dos filtros
      refine (ih1.append (ih2.cons p)).trans ?_
      refine (perm_middle).trans ?_
      exact (filter_append_perm (fun x => decide (x ≤ p)) rest).cons p
  termination_by l => l.length
  decreasing_by
    all_goals simp_wf
    all_goals exact le_trans (length_filter_le _ _) (le_of_eq (by simp))

theorem mem_quicksort {a : α} {l : List α} : a ∈ quicksort l ↔ a ∈ l :=
  (quicksort_perm l).mem_iff

Nota (La inducción sigue a la recursión)

Obsérvese que quicksort_perm lleva sus propias cláusulas termination_by y decreasing_by, idénticas a las de la definición: el teorema se prueba por la misma recursión bien fundamentada con la que se definió la función, y las llamadas quicksort_perm _ sobre las mitades son exactamente las hipótesis de inducción del argumento matemático. En Lean, «inducción bien fundamentada siguiendo la recursión» no es una metáfora: es literalmente el mismo mecanismo.