header {* Verificación de la ordenación rápida *}
theory Ordenacion_rapida
imports Main
begin
text {* ---------------------------------------------------------------------------------
En este trabajo se describe el algoritmo de ordenación rápida de listas y se propone
comprobar que es correcto.
El algoritmo de ordenación rápida de listas considera el primer elemento de la lista a
ordenar y separa los restantes en dos listas, una con los menores que el primero y otra
con los mayores o iguales que el primero. Ambas listas se ordenan y se concatenan los
resultados el el orden adecuado. Por ejemplo, dada la lista [2,7,1,5] el algoritmo
actúa como se describe a continuación:
- Lista a ordenar: [2,7,1,5]
Primer elemento: 2
Lista de elementos menores que 2: [1]
Lista de elementos mayores que 2: [7,5]
-- Lista a ordenar: [1]
Primer elemento: 1
Lista de elementos menores que 1: [], ya está ordenada
Lista de elementos mayores que 1: [], ya está ordenada
-- Lista ordenada: [1]
-- Lista a ordenar: [7,5]
Primer elemento: 7
Lista de elementos menores que 7: [5]
Lista de elementos mayores que 7: [], ya está ordenada
--- Lista a ordenar: [5]
Primer elemento: 5
Lista de elementos menores que 5: [], ya está ordenada
Lista de elementos mayores que 5: [], ya está ordenada
--- Lista ordenada: [5]
-- Lista ordenada: [5,7]
- Lista ordenada: [1,2,5,7]
Para implementar este algoritmo de ordenación se definen las siguientes funciones:
-------------------------------------------------------------------------------------- *}
text {* ---------------------------------------------------------------------------------
Consideramos la función
menores :: int ⇒ int list ⇒ bool
tal que '(menores a xs)' es la lista de los elementos de la lista 'xs' que son menores
que el elemento 'a'. Por ejemplo,
-------------------------------------------------------------------------------------- *}
fun menores :: "int ⇒ int list ⇒ int list" where
"menores a [] = []"
| "menores a (x#xs) = (if x < a then x # (menores a xs)
else (menores a xs))"
value "menores 2 [3,0,1]" -- "= [0,1]"
value "menores 2 [3,0,5]" -- "= [0]"
text {* ---------------------------------------------------------------------------------
La longitud de la lista de elementos menores que uno dado es menor o igual que la
longitud de la lista original.
-------------------------------------------------------------------------------------- *}
lemma menores_menor[simp]:
"length (menores x xs) < Suc (length xs)"
by (induct xs) auto
text {* ---------------------------------------------------------------------------------
Consideramos la función
mayores :: int ⇒ int list ⇒ bool
tal que '(mayores a xs)' es la lista de los elementos de la lista 'xs' que son mayores
o iguales que el elemento 'a'. Por ejemplo,
-------------------------------------------------------------------------------------- *}
fun mayores :: "int ⇒ int list ⇒ int list" where
"mayores a [] = []"
| "mayores a (x#xs) = (if x < a then (mayores a xs)
else x # (mayores a xs))"
value "mayores 2 [3,2,1]" -- "= [3,2]"
value "mayores 2 [3,0,5]" -- "= [3,5]"
text {* ---------------------------------------------------------------------------------
La longitud de la lista de elementos mayores que uno dado es menor o igual que la
longitud de la lista original.
-------------------------------------------------------------------------------------- *}
lemma mayores_menor[simp]:
"length (mayores x xs) < Suc (length xs)"
by (induct xs) auto
text {* ---------------------------------------------------------------------------------
Consideramos la función
ordena :: int list ⇒ int list
tal que '(ordena xs)' es la lista obtenida ordenando la lista 'xs' por ordenación
rápida; es decir, la divide en dos partes, los elementos menores que el primer elemento
de 'xs' y los elementos mayores que el primer elemento de 'xs', se ordenan ambas partes
y se concatenan. Por ejemplo,
ordena [3,2,5,2] = [2,2,3,5]
-------------------------------------------------------------------------------------- *}
function ordena :: "int list ⇒ int list" where
"ordena [] = []"
| "ordena (x # xs) = ((ordena (menores x xs)) @ (x # (ordena (mayores x xs))))"
by pat_completeness auto
value "ordena [3,2,5,2]" -- "= [2,2,3,5]"
text {* ---------------------------------------------------------------------------------
La terminación de la función 'ordena' se basa en la longitud de su argumento, que
disminuye en las llamadas recursivas.
-------------------------------------------------------------------------------------- *}
termination ordena
by (relation "measure length") auto
section {* Corrección del algoritmo de ordenación *}
text {* ---------------------------------------------------------------------------------
La corrección del algoritmo de ordenación consiste en comprobar dos propiedades:
- El resultado del algoritmo de ordenación tiene los mismos elementos que la lista
original.
- El resultado del algoritmo de ordenación es una lista ordenada.
A continuación definimos las funciones necesarias para comprobar la corrección del
algoritmo de ordenación.
-------------------------------------------------------------------------------------- *}
text {* ---------------------------------------------------------------------------------
Consideramos la función
menor :: int ⇒ int list ⇒ bool
tal que '(menor a xs)' se verifica si el elemento 'a' es menor o igual que todos los
elementos de 'xs'. Por ejemplo,
menor 2 [3,2,5] = True
menor 2 [3,0,5] = False
-------------------------------------------------------------------------------------- *}
fun menor :: "int ⇒ int list ⇒ bool" where
"menor a [] = True"
| "menor a (x#xs) = (a ≤ x ∧ menor a xs)"
value "menor 2 [3,2,5]" -- "= True"
value "menor 2 [3,0,5]" -- "= False"
text {* ---------------------------------------------------------------------------------
Consideramos la función
menor_lista :: int list ⇒ int list ⇒ bool
tal que '(menor_lista xs ys)' se verifica si todos los elementos de 'xs' son menores o
iguales que todos los elementos de 'xs'. Por ejemplo,
menor_lista [1,2] [3,2,5] = True
menor_lista [1,2] [3,0,5] = False
-------------------------------------------------------------------------------------- *}
fun menor_lista :: "int list ⇒ int list ⇒ bool" where
"menor_lista [] ys = True"
| "menor_lista (x#xs) ys = (menor x ys ∧ menor_lista xs ys)"
value "menor_lista [1,2] [3,2,5]" -- "= True"
value "menor_lista [1,2] [3,0,5]" -- "= False"
text {* ---------------------------------------------------------------------------------
Consideramos la función
ordenada :: int list ⇒ bool
tal que '(ordenada xs)' se verifica si 'xs' es una lista ordenada de manera creciente.
Por ejemplo,
ordenada [2,3,3,5] = True
ordenada [2,4,3,5] = False
-------------------------------------------------------------------------------------- *}
fun ordenada :: "int list ⇒ bool" where
"ordenada [] = True"
| "ordenada (x#xs) = (menor x xs & ordenada xs)"
value "ordenada [2,3,3,5]" -- "= True"
value "ordenada [2,4,3,5]" -- "= False"
text {* ---------------------------------------------------------------------------------
Consideramos la función
cuenta :: int list ⇒ int ⇒ nat
tal que '(cuenta xs y)' es el número de veces que aparece el elemento 'y' en la lista
'xs'. Por ejemplo,
cuenta [1,3,4,3,5] 3 = 2
-------------------------------------------------------------------------------------- *}
fun cuenta :: "int list ⇒ int ⇒ nat" where
"cuenta [] y = 0"
| "cuenta (x#xs) y = (if x=y then Suc(cuenta xs y) else cuenta xs y)"
value "cuenta [1,3,4,3,5] 3" -- "= 2"
text {* ---------------------------------------------------------------------------------
Propiedad 1: El resultado del algoritmo de ordenación tiene los mismos elementos que la
lista original.
-------------------------------------------------------------------------------------- *}
lemma cuenta_append:
"cuenta (xs @ ys) y = (cuenta xs y + cuenta ys y)"
oops
lemma cuenta_menores:
"cuenta (menores x xs) y = (if y < x then cuenta xs y else 0)"
oops
lemma cuenta_mayores:
"cuenta (mayores x xs) y = (if y < x then 0 else cuenta xs y)"
oops
theorem cuenta_ordena:
"cuenta (ordena xs) y = cuenta xs y"
oops
text {* ---------------------------------------------------------------------------------
Propiedad 2: El resultado del algoritmo de ordenación es una lista ordenada.
-------------------------------------------------------------------------------------- *}
lemma conjConmutativaAsociativa[simp]:
"(P ∧ Q ∧ R) = (Q ∧ P ∧ R)"
by auto
lemma menor_append:
"menor a (xs @ ys) = (menor a xs ∧ menor a ys)"
oops
lemma menor_mayores:
"a ≤ x ⟶ menor a (mayores x xs)"
oops
lemma menor_lista_menores:
"x ≤ a ⟶ menor_lista (menores x xs) [a]"
oops
lemma menor_menores_mayores:
"(menor a (menores x xs) ∧ menor a (mayores x xs)) = menor a xs"
oops
lemma menor_ordena:
"menor a (ordena xs) = menor a xs"
oops
lemma menor_lista_cons:
"(menor_lista xs [y] ∧ menor_lista xs ys) = menor_lista xs (y # ys)"
oops
lemma menor_lista_append:
"menor_lista (xs @ ys) zs = (menor_lista xs zs ∧ menor_lista ys zs)"
oops
lemma ordenada_append:
"ordenada (xs @ ys) = (ordenada xs ∧ ordenada ys ∧ menor_lista xs ys)"
oops
lemma menor_lista_menores_mayores1:
"(menor_lista (menores x xs) ys ∧ menor_lista (mayores x xs) ys) = menor_lista xs ys"
oops
lemma menor_lista_menores_mayores2:
"menor_lista (menores x xs) (mayores x ys)"
oops
lemma menor_lista_ordena1:
"menor_lista (ordena xs) ys = menor_lista xs ys"
oops
lemma menor_lista_ordena2:
"menor_lista xs (ordena ys) = menor_lista xs ys"
oops
lemma menor_lista_menores_cons:
"menor_lista (menores x xs) (x # ys) = menor_lista (menores x xs) ys"
oops
theorem ordenada_ordena:
"ordenada (ordena xs)"
oops
text {* ------------------------------------------------------------------------------ *}
end