Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

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