Tema 11: Verificación de la ordenación por inserción
De Razonamiento automático (2019-20)
<soure lang="isabelle"> chapter ‹T11: Verificación de la ordenación por inserción›
theory T11_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 detallada 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 only: menor.simps(1)
simp_thms(17))
next
fix z zs
assume HI: "menor y zs ⟶ menor x zs"
show "menor y (z # zs) ⟶ menor x (z # zs)"
proof (rule impI)
assume sup: "menor y (z # zs)"
show "menor x (z # zs)"
proof (simp only: menor.simps(2))
show "x ≤ z ∧ menor x zs"
proof (rule conjI)
have "x ≤ y"
using assms
by this
also have "y ≤ z"
using sup
by (simp only: menor.simps(2))
finally show "x ≤ z"
by this
next
have "menor y zs"
using sup
by (simp only: menor.simps(2))
with HI show "menor x zs"
by (rule mp)
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 detallada 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 only: menor.simps(2)
inserta.simps(1))
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"
then have "menor x (inserta y (z#zs)) = menor x (y#z#zs)"
by (simp only: inserta.simps(2)
if_True)
also have "… = (x ≤ y ∧ menor x (z#zs))"
by (simp only: menor.simps(2))
finally show ?thesis
by this
next
assume "¬(y ≤ z)"
then have "menor x (inserta y (z#zs)) =
menor x (z # inserta y zs)"
by (simp only: inserta.simps(2)
if_False)
also have "… = (x ≤ z ∧ menor x (inserta y zs))"
by (simp only: menor.simps(2))
also have "… = (x ≤ z ∧ (x ≤ y ∧ menor x zs))"
by (simp only: HI)
also have "… = ((x ≤ z ∧ x ≤ y) ∧ menor x zs)"
by (simp only: conj_assoc)
also have "… = ((x ≤ y ∧ x ≤ z) ∧ menor x zs)"
by (simp only: conj_commute)
also have "… = (x ≤ y ∧ (x ≤ z ∧ menor x zs))"
by (simp only: conj_assoc)
also have "… = (x ≤ y ∧ menor x (z#zs))"
by (simp only: menor.simps(2))
finally show ?thesis
by this
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 a xs) = ordenada xs" by (induct xs) (auto simp add: menor_menor menor_inserta)
― ‹La demostración estructurada es› lemma
"ordenada (inserta a xs) = ordenada xs"
proof (induct xs)
case Nil then show ?case try by simp
next
case (Cons a xs)
then show ?case
using menor_inserta
menor_menor
by auto
qed
lemma ordenada_inserta:
"ordenada (inserta a xs) = ordenada xs"
proof (induct xs)
show "ordenada (inserta a []) = ordenada []"
proof -
have "ordenada (inserta a []) = ordenada [a]"
by (simp only: inserta.simps(1))
also have "… = (menor a [] ∧ ordenada [])"
by (simp only: ordenada.simps(2))
also have "… = (True ∧ ordenada [])"
by (simp only: menor.simps(1))
also have "… = ordenada []"
by (simp only: simp_thms(22))
finally show ?thesis
by this
qed
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"
then show "ordenada (inserta a (x # xs)) = ordenada (x # xs)"
using menor_menor by auto
next
assume "¬(a ≤ x)"
then have "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 xs)"
by (induct xs) (auto simp add: ordenada_inserta)
― ‹La demostración estructurada es› theorem
"ordenada (ordena xs)"
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons a xs) then show ?case by (simp add: ordenada_inserta)
qed
theorem ordenada_ordena:
"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 xs) y = cuenta xs y" by (induct xs) (auto simp add: cuenta_inserta)
― ‹La demostración estructurada es› theorem
"cuenta (ordena xs) y = cuenta xs y"
proof (induct xs)
case Nil then show ?case by simp
next
case (Cons a xs) then show ?case by (simp add: cuenta_inserta)
qed
― ‹La demostración estructurada es› theorem cuenta_ordena:
"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_prefix "CodigoGenerado/"
end </source>