Menu Close

RA2018: Verificación de algoritmos de ordenación con Isabelle/HOL

En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo verificar con Isabelle/HOL la corrección de distintos algoritmos de ordenación.

El primero de los algoritmos verificados ha sido el de ordenación por inserción. La correspondiente teoría Isabelle/HOL se muestra a continuación

chapter {* T6a: Verificación de la ordenación por inserción *}
 
theory T6a_Verificacion_de_la_ordenacion_por_insercion
imports Main
begin
 
text {*
  En este de tema se define el algoritmo de ordenación de listas 
  por inserción y se demuestra que es correcto. *}
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función
     inserta :: int ⇒ int list ⇒ int list
  tal que (inserta a xs) es la lista obtenida insertando a delante del
  primer elemento de xs que es mayor o igual que a. Por ejemplo,
     inserta 3 [2,5,1,7] = [2,3,5,1,7]
  ------------------------------------------------------------------ *}
 
fun inserta :: "int ⇒ int list ⇒ int list" where
  "inserta a []     = [a]"
| "inserta a (x#xs) = (if a ≤ x 
                       then a # x # xs 
                       else x # inserta a xs)"
 
value "inserta 3 [2,5,1,7] = [2,3,5,1,7]"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función
     ordena :: int list ⇒ int list
  tal que (ordena xs) es la lista obtenida ordenando xs por inserción. 
  Por ejemplo, 
     ordena [3,2,5,3] = [2,3,3,5]
  ------------------------------------------------------------------ *}
 
fun ordena :: "int list ⇒ int list" where
  "ordena []     = []"
| "ordena (x#xs) = inserta x (ordena xs)"
 
value "ordena [3,2,5,3] = [2,3,3,5]"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función
     menor :: int ⇒ int list ⇒ bool
  tal que (menor a xs) se verifica si 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 {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir 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 {*  
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar que si y es una cota inferior de zs y x ≤ y,
  entonces x es una cota inferior de zs.
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
lemma menor_menor: 
  assumes "x ≤ y"  
  shows   "menor y zs ⟶ menor x zs"
using assms
by (induct zs) auto
 
― ‹La demostración estructurada es›
lemma menor_menor_2: 
  assumes "x ≤ y"  
  shows   "menor y zs ⟶ menor x zs"
proof (induct zs)
  show "menor y [] ⟶ menor x []" by simp
next
  fix z zs
  assume HI: "menor y zs ⟶ menor x zs"  
  show "menor y (z # zs) ⟶ menor x (z # zs)"
  proof
    assume sup: "menor y (z # zs)"
    show "menor x (z # zs)"
    proof (simp only: menor.simps(2))
      show "x ≤ z ∧ menor x zs"
      proof
          have "x ≤ y" using assms .
          also have "y ≤ z" using sup by simp
          finally show "x ≤ z" .
      next
        have "menor y zs" using sup by simp
        with HI show "menor x zs" by simp
      qed
    qed
  qed
qed
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar el siguiente teorema de corrección: x es una
  cota inferior de la lista obtenida insertando y en zs syss x ≤ y y x
  es una cota inferior de zs.
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
lemma menor_inserta:
  "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
by (induct zs) auto
 
― ‹La demostración estructurada es›
lemma menor_inserta_2: 
  "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
proof (induct zs)
  show "menor x (inserta y []) = (x ≤ y ∧ menor x [])" by simp
next 
  fix z zs
  assume HI: "menor x (inserta y zs) = (x ≤ y ∧ menor x zs)"
  show "menor x (inserta y (z#zs)) = (x ≤ y ∧ menor x (z#zs))" 
  proof (cases "y ≤ z")
    assume "y ≤ z"
    hence "menor x (inserta y (z#zs)) = menor x (y#z#zs)" by simp
    also have "… = (x ≤ y ∧ menor x (z#zs))" by simp
    finally show ?thesis by simp
  next
    assume "¬(y ≤ z)"
    hence "menor x (inserta y (z#zs)) = 
           menor x (z # inserta y zs)" by simp
    also have "… = (x ≤ z ∧ menor x (inserta y zs))" by simp
    also have "… = (x ≤ z ∧ x ≤ y ∧ menor x zs)" using HI by simp
    also have "… = (x ≤ y ∧ menor x (z#zs))" by auto
    finally show ?thesis by simp
  qed
qed
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar que al insertar un elemento la lista obtenida
  está ordenada syss lo estaba la original.
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
lemma ordenada_inserta:
  "ordenada (inserta a xs) = ordenada xs"
by (induct xs) (auto simp add: menor_menor menor_inserta)
 
― ‹La demostración estructurada es›
lemma ordenada_inserta_2:
  "ordenada (inserta a xs) = ordenada xs"
proof (induct xs)
  show "ordenada (inserta a []) = ordenada []" by simp
next
  fix x xs
  assume HI: "ordenada (inserta a xs) = ordenada xs" 
  show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
  proof (cases "a ≤ x")
    assume "a ≤ x"
    hence "ordenada (inserta a (x # xs)) = 
           ordenada (a # x # xs)" by simp
    also have "… = (menor a (x#xs) ∧ ordenada (x # xs))" by simp
    also have "… = ordenada (x # xs)"  
      using `a ≤ x`  by (auto simp add: menor_menor)
    finally show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
      by simp
  next
    assume "¬(a ≤ x)"
    hence "ordenada (inserta a (x # xs)) = 
           ordenada (x # inserta a xs)" by simp
    also have "… = (menor x (inserta a xs) ∧ ordenada (inserta a xs))" 
      by simp
    also have "… = (menor x (inserta a xs) ∧ ordenada xs)" 
      using HI by simp
    also have "… = (menor x xs ∧ ordenada xs)" 
      using(a ≤ x)` by (simp add: menor_inserta)
    also have "… = ordenada (x # xs)" by simp
    finally show "ordenada (inserta a (x # xs)) = ordenada (x # xs)" 
      by simp
  qed
qed
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que, para toda lista xs, (ordena xs) está
  ordenada. 
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
theorem ordenada_ordena:
  "ordenada (ordena xs)"
by (induct xs) (auto simp add: ordenada_inserta)
 
― ‹La demostración estructurada es›
theorem ordenada_ordena_2:
  "ordenada (ordena xs)"
proof (induct xs) 
  show "ordenada (ordena [])" by simp
next
  fix x xs
  assume "ordenada (ordena xs)" 
  then have "ordenada (inserta x (ordena xs))" 
    by (simp add: ordenada_inserta)  
  then show "ordenada (ordena (x # xs))" by simp
qed
 
text {*  
  --------------------------------------------------------------------- 
  Nota. El teorema anterior no garantiza que ordena sea correcta, ya que
  puede que (ordena xs) no tenga los mismos elementos que xs. Por
  ejemplo, si se define (ordena xs) como [] se tiene que (ordena xs)
  está ordenada pero no es una ordenación de xs. 
 
  Para garantizarlo, definimos la función cuenta.
  ------------------------------------------------------------------ *}
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 8. Definir 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 {*  
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar que el número de veces que aparece y en 
  (inserta x xs) es 
  * uno más el número de veces que aparece en xs, si y = x; 
  * el número de veces que aparece en xs, si y ≠ x; 
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
lemma cuenta_inserta:
  "cuenta (inserta x xs) y =
   (if x=y then Suc (cuenta xs y) else cuenta xs y)"
by (induct xs) auto
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar que el número de veces que aparece y en 
  (ordena xs) es el número de veces que aparece en xs.
  ------------------------------------------------------------------ *}
 
― ‹La demostración automática es›
theorem cuenta_ordena:
  "cuenta (ordena xs) y = cuenta xs y"
by (induct xs) (auto simp add: cuenta_inserta)
 
― ‹La demostración estructurada es›
theorem cuenta_ordena_2:
  "cuenta (ordena xs) y = cuenta xs y"
proof (induct xs)
  show "cuenta (ordena []) y = cuenta [] y" by simp
next
  fix x xs
  assume HI: "cuenta (ordena xs) y = cuenta xs y"
  show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" 
  proof (cases "x = y")
    assume "x = y"
    have "cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y" 
      by simp
    also have "… = Suc (cuenta (ordena xs) y)" using `x = y` 
      by (simp add: cuenta_inserta) 
    also have "… = Suc (cuenta xs y)" using HI by simp
    also have "… = cuenta (x # xs) y" using `x = y` by simp
    finally show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" by simp
  next
    assume "x ≠ y"
    have "cuenta (ordena (x # xs)) y = cuenta (inserta x (ordena xs)) y" 
      by simp
    also have "… = cuenta (ordena xs) y" using `x ≠ y` 
      by (simp add: cuenta_inserta) 
    also have "… = cuenta xs y" using HI by simp
    also have "… = cuenta (x # xs) y" using `x ≠ y` by simp
    finally show "cuenta (ordena (x # xs)) y = cuenta (x # xs) y" 
      by simp
  qed
qed
 
text {*
    Para exportar el código Haskell de la función snoc se usa
*}
 
export_code ordena in Haskell 
  module_name OrdInsercion 
  file "CodigoGenerado/"
end

El segundo de los algoritmos verificados ha sido el de ordenación por mezcla. La correspondiente teoría Isabelle/HOL se muestra a continuación

chapter {* T6b: Verificación de la ordenación por mezcla *}
 
theory T6b_Verificacion_de_la_ordenacion_por_mezcla
imports Main
begin
 
text {*
  En esta relación de ejercicios se define el algoritmo de ordenación de
  listas por mezcla y se demuestra que es correcto.
*}
 
section {* Ordenación de listas *}
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función
     menor :: int ⇒ int list ⇒ bool
  tal que (menor a xs) se verifica si 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 {*  
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir 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 {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir 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"
 
section {* Ordenación por mezcla *}
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función
     mezcla :: int list ⇒ int list ⇒ int list
  tal que (mezcla xs ys) es la lista obtenida mezclando las listas
  ordenadas xs e ys. Por ejemplo, 
     mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]
  ------------------------------------------------------------------ *}
 
fun mezcla :: "int list ⇒ int list ⇒ int list" where
  "mezcla [] ys = ys" 
| "mezcla xs [] = xs" 
| "mezcla (x # xs) (y # ys) = (if x ≤ y
                               then x # mezcla xs (y # ys)
                               else y # mezcla (x # xs) ys)"
 
value "mezcla [1,2,5] [3,5,7] = [1,2,3,5,5,7]"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir la función
     ordenaM :: int list ⇒ int list
  tal que (ordenaM xs) es la lista obtenida ordenando la lista xs
  mediante mezclas; es decir, la divide en dos mitades, las ordena y las
  mezcla. Por ejemplo, 
     ordenaM [3,2,5,2] = [2,2,3,5]
  ------------------------------------------------------------------ *}
 
fun ordenaM :: "int list ⇒ int list" where
  "ordenaM []  = []" 
| "ordenaM [x] = [x]" 
| "ordenaM xs = 
     (let mitad = length xs div 2 in
      mezcla (ordenaM (take mitad xs)) 
             (ordenaM (drop mitad xs)))"
 
value "ordenaM [3,2,5,2] = [2,2,3,5]"
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Sea x ≤ y. Si y es menor o igual que todos los elementos
  de xs, entonces x es menor o igual que todos los elementos de xs
  ------------------------------------------------------------------ *}
 
lemma menor_menor: 
  "x ≤ y ⟹ menor y xs ⟶ menor x xs"
by (induct xs) auto
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que el número de veces que aparece n en la
  mezcla de dos listas es igual a la suma del número de apariciones en
  cada una de las listas
  ------------------------------------------------------------------ *}
 
lemma cuenta_mezcla: 
  "cuenta (mezcla xs ys) n = cuenta xs n + cuenta ys n"
by (induct xs ys rule: mezcla.induct) auto
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar que si x es menor que todos los elementos de
  ys y de zs, entonces también lo es de su mezcla.
  ------------------------------------------------------------------ *}
 
lemma menor_mezcla:
  assumes "menor x ys" 
          "menor x zs" 
  shows   "menor x (mezcla ys zs)"
using assms 
by (induct ys zs rule: mezcla.induct) simp_all
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar que la mezcla de dos listas ordenadas es una
  lista ordenada. 
  Indicación: Usar los siguientes lemas
  · linorder_not_le: (¬ x ≤ y) = (y < x)
  · order_less_le:   (x < y) = (x ≤ y ∧ x ≠ y)
  ------------------------------------------------------------------ *}
 
lemma ordenada_mezcla:
  assumes "ordenada xs" 
          "ordenada ys" 
  shows   "ordenada (mezcla xs ys)"
using assms 
by (induct xs ys rule: mezcla.induct) 
   (auto simp add: menor_mezcla
                   menor_menor
                   linorder_not_le 
                   order_less_le)
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar que si x es mayor que 1, entonces el mínimo de
  x y su mitad es menor que x.
  ------------------------------------------------------------------ *}
 
lemma min_mitad: 
  "1 < x ⟹ min x (x div 2::int) < x"
by simp
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar que si x es mayor que 1, entonces x menos su
  mitad es menor que x. 
  ------------------------------------------------------------------ *}
 
lemma menos_mitad: 
  "1 < x ⟹ x - x div (2::int) < x"
by arith
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar que (ordenaM xs) está ordenada.
  ------------------------------------------------------------------ *}
 
theorem ordenada_ordenaM:
  "ordenada (ordenaM xs)"
by (induct xs rule: ordenaM.induct) 
   (auto simp add: ordenada_mezcla)
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar que el número de apariciones de un elemento en
  la concatenación de dos listas es la suma del número de apariciones en
  cada una.
  ------------------------------------------------------------------ *}
 
lemma cuenta_conc: 
  "cuenta (xs @ ys) x = cuenta xs x + cuenta ys x"
by (induct xs) auto
 
text {*  
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar que las listas xs y (ordenaM xs) tienen los
  mismos elementos.
  ------------------------------------------------------------------ *}
 
theorem cuenta_ordenaM: 
  "cuenta (ordenaM xs) x = cuenta xs x"
by (induct xs rule: ordenaM.induct) 
   (auto simp add: cuenta_mezcla 
                   cuenta_conc [symmetric])
end

Finalmente, se ha dejado conmo tarea el estudio del algoritmo eficiente de ordenación por mezcla de GHC que se describe en el artículo Proof pearl: A mechanized proof of GHC’s mergesort y cuya correspondiente teoría es Efficient mergesort.

RA2018