Nivel 8 · Quicksort verificado (experto)

Corrección II: ordenamiento

La prueba de ordenamiento descansa en dos cosas: cómo se comporta el predicado por pares de la

bajo la concatenación, y la propiedad definitoria de las dos mitades de la partición.

Lema 12.10 (Pairwise sobre la concatenación)

Para una relación $R$ y listas $\ell_1,\ell_2$ ,

\mathrm{Pairwise}\,R\,(\ell_1 +\!\!+\, \ell_2) \ \Longleftrightarrow\ \mathrm{Pairwise}\,R\,\ell_1 \ \wedge\ \mathrm{Pairwise}\,R\,\ell_2 \ \wedge\ \big(\forall a\in\ell_1,\ \forall b\in\ell_2,\ R\,a\,b\big).

Asimismo $\mathrm{Pairwise}\,R\,(a::\ell)\Leftrightarrow(\forall b\in\ell,\ R\,a\,b)\wedge\mathrm{Pairwise}\,R\,\ell$ .

Demostración.

A probar: las dos equivalencias del enunciado. La primera, por inducción sobre $\ell_1$ .

$\ell_1=[\,]$ . Entonces $[\,] +\!\!+\, \ell_2=\ell_2$ , $\mathrm{Pairwise}\,R\,[\,]$ es verdadero y la condición cruzada « $\forall a\in[\,],\dots$ » es vacua; los dos lados se reducen a $\mathrm{Pairwise}\,R\,\ell_2$ .
$\ell_1=a::\ell_1'$ . Por la forma cons (segunda equivalencia), $\mathrm{Pairwise}\,R\,\big((a::\ell_1') +\!\!+\, \ell_2\big)\Leftrightarrow \big(\forall c\in \ell_1' +\!\!+\, \ell_2,\ R\,a\,c\big)\wedge \mathrm{Pairwise}\,R\,(\ell_1' +\!\!+\, \ell_2).$ Separando $c\in\ell_1'$ de $c\in\ell_2$ en la primera conjunción y aplicando la hipótesis de inducción a la segunda, se obtiene $\mathrm{Pairwise}\,R\,\ell_1 \wedge \mathrm{Pairwise}\,R\,\ell_2 \wedge (\forall a\in\ell_1,\forall b\in\ell_2,R\,a\,b)$ .

La segunda equivalencia es la definición de $\mathrm{Pairwise}$ sobre una lista cons. (En Lean estos son los lemas de biblioteca List.pairwise_append y List.pairwise_cons.)

La observación decisiva es la separación garantizada por la partición: todo elemento de la mitad pequeña es $\leq p$ y todo elemento de la mitad grande es $>p$ (luego $\geq p$ ). Combinado con la transitividad de $\leq$ , esto da la cota cruzada necesaria para pegar las mitades ordenadas recursivamente.

El teorema de ordenamiento

Teorema 12.11 (Ordenamiento)

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

Demostración.

A probar: $\mathsf{Sorted}(\mathsf{qsort}(\ell))$ , para toda $\ell$ . Por inducción bien fundamentada sobre $|\ell|$ .

$\ell=[\,]$ . $\mathsf{qsort}([\,])=[\,]$ está ordenada de manera vacua.
$\ell=p::r$ . Abréviese $A=\mathsf{qsort}(\ell_{\leq})$ y $B=\mathsf{qsort}(\ell_{>})$ , de modo que $\mathsf{qsort}(p::r)=A +\!\!+\, (p::B)$ . La hipótesis de inducción (aplicable porque $\ell_{\leq},\ell_{>}$ son más cortas que $p::r$ ) da $\mathsf{Sorted}(A)$ y $\mathsf{Sorted}(B)$ .

Paso 1: cotas sobre las mitades.
- Sea $a\in A$ . Por el Corolario 12.9, $a\in\ell_{\leq}$ , esto es, $a$ aparece en $r$ y pasa la prueba; luego $a\leq p$ .
- Sea $b\in B$ . Por el Corolario 12.9, $b\in\ell_{>}$ , esto es, $b$ aparece en $r$ y falla la prueba $b\leq p$ . Como $\leq$ es lineal, $\neg(b\leq p)$ implica $p < b$ , luego $p\leq b$ .
En resumen,
$(\forall a\in A,\ a\leq p) \qquad\text{y}\qquad (\forall b\in B,\ p\leq b). \tag{$\ast$}$
Paso 2: ensamblaje. Por el Lema 12.10 aplicado a $A +\!\!+\, (p::B)$ , probar $\mathsf{Sorted}(A +\!\!+\, (p::B))$ se reduce a tres obligaciones:
1. $\mathsf{Sorted}(A)$ : es la hipótesis de inducción.
2. $\mathsf{Sorted}(p::B)$ : por la forma cons del Lema 12.10, equivale a $(\forall b\in B,\ p\leq b)$ , la mitad derecha de $(\ast)$ , junto con $\mathsf{Sorted}(B)$ , la hipótesis de inducción.
3. Cota cruzada $\forall a\in A,\ \forall c\in(p::B),\ a\leq c$ . Fíjense $a\in A$ y $c\in p::B$ . Si $c=p$ , entonces $a\leq p$ por la mitad izquierda de $(\ast)$ . Si $c\in B$ , entonces $a\leq p\leq c$ por ambas mitades de $(\ast)$ y la transitividad de $\leq$ .
Las tres se cumplen, luego $\mathsf{Sorted}(A +\!\!+\, (p::B))=\mathsf{Sorted}(\mathsf{qsort}(p::r))$ .

Nota (Las tres zonas de la salida)

Las tres obligaciones corresponden exactamente a las tres «zonas» de la salida ensamblada $A +\!\!+\, (p::B)$ y a las relaciones de orden entre ellas: dentro de $A$ y dentro de $B$ el orden se cumple por la hipótesis de inducción; a través del pivote se cumple por las cotas de la partición $(\ast)$ ; y la cota de largo alcance de $A$ a $B$ se sigue encadenando por $p$ , esto es, por transitividad. El widget de la

página del algoritmo

verifica precisamente estas cotas en cada nodo del árbol de recursión.

Lean

La prueba en Thesis/Sort/Quicksort.lean nombra las mismas piezas: ih1, ih2 son $\mathsf{Sorted}(A)$ , $\mathsf{Sorted}(B)$ ; hsmall, hlarge son las dos mitades de $(\ast)$ , cada una obtenida transportando la pertenencia de vuelta por mem_quicksort (Corolario 12.9) y desplegando la prueba del filtro; pairwise_append y pairwise_cons son el Lema 12.10; y el le_trans final es el paso de transitividad de la obligación (3).

theorem quicksort_sorted : ∀ l : List α, Sorted (quicksort l)
  | [] => by simp [Sorted]
  | p :: rest => by
      have ih1 : Sorted (quicksort (rest.filter (fun x => decide (x ≤ p)))) :=
        quicksort_sorted _
      have ih2 : Sorted (quicksort (rest.filter (fun x => ! decide (x ≤ p)))) :=
        quicksort_sorted _
      simp only [Sorted] at ih1 ih2 ⊢
      rw [quicksort_cons]
      -- todo elemento de la mitad "pequeña" es ≤ p
      have hsmall : ∀ a ∈ quicksort (rest.filter (fun x => decide (x ≤ p))), a ≤ p := by
        intro a ha
        have hmem : a ∈ rest.filter (fun x => decide (x ≤ p)) := mem_quicksort.1 ha
        simp only [mem_filter, decide_eq_true_eq] at hmem
        exact hmem.2
      -- todo elemento de la mitad "grande" es ≥ p (de hecho > p)
      have hlarge : ∀ b ∈ quicksort (rest.filter (fun x => ! decide (x ≤ p))), p ≤ b := by
        intro b hb
        have hmem : b ∈ rest.filter (fun x => ! decide (x ≤ p)) := mem_quicksort.1 hb
        simp only [mem_filter, Bool.not_eq_true', decide_eq_false_iff_not] at hmem
        exact le_of_lt (not_le.1 hmem.2)
      rw [pairwise_append]
      refine ⟨ih1, ?_, ?_⟩
      · -- el bloque derecho `p :: grande` está ordenado
        rw [pairwise_cons]
        exact ⟨hlarge, ih2⟩
      · -- condición cruzada: todo elemento pequeño ≤ todo elemento de `p :: grande`
        intro a ha b hb
        rcases List.mem_cons.1 hb with hbp | hb'
        · subst hbp; exact hsmall a ha
        · exact le_trans (hsmall a ha) (hlarge b hb')
  termination_by l => l.length
  decreasing_by
    all_goals simp_wf
    all_goals exact le_trans (length_filter_le _ _) (le_of_eq (by simp))

El teorema principal

Reuniendo las dos mitades se obtiene la especificación de la Definición 12.1.

Teorema 12.12 (Corrección de quicksort)

Para toda lista $\ell$ sobre un tipo linealmente ordenado,

\mathsf{qsort}(\ell)\sim\ell \quad\text{y}\quad \mathsf{Sorted}(\mathsf{qsort}(\ell)).

Es decir, quicksort devuelve una permutación ordenada de su entrada.

Demostración.

A probar: $\mathsf{qsort}(\ell)\sim\ell$ y $\mathsf{Sorted}(\mathsf{qsort}(\ell))$ , para toda $\ell$ .

$\mathsf{qsort}(\ell)\sim\ell$ es el Teorema 12.8 (permutación).
$\mathsf{Sorted}(\mathsf{qsort}(\ell))$ es el Teorema 12.11 (ordenamiento).

La conjunción de ambos es precisamente la corrección de quicksort.

theorem quicksort_correct (l : List α) :
    quicksort l ~ l ∧ Sorted (quicksort l) :=
  ⟨quicksort_perm l, quicksort_sorted l⟩

El término ⟨quicksort_perm l, quicksort_sorted l⟩ es el constructor anónimo de un par: la conjunción es un tipo producto y su prueba, un par de pruebas, exactamente la lectura de $\land$ como $\times$ de la correspondencia de Curry–Howard . No queda obligación de prueba una vez que el núcleo verifica su tipo.