chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)›
theory R11_sol
imports Main
begin
text ‹ ---------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
+ automática
+ en el ejercicio 1.2, la prueba detallada usando "simp only:..."
(bien de forma declarativa o aplicativa)
+ en los ejercicios 5, 6 y 7 sólo es necesario hacer la demostración
detallada usando "simp", sin llegar al detalle de usar "simp only:..."
------------------------------------------------------------------ ›
text ‹ ---------------------------------------------------------------
Ejercicio 1.1. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ ›
fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"
value "factR 4" ― ‹= 24›
text ‹ ---------------------------------------------------------------
Ejercicio 1.2. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1
factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- ›
fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (x* (Suc n))"
fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"
― ‹Demostración automática:›
lemma "factI' n x = x * factR n"
by (induct n arbitrary: x)
(auto simp del: mult_Suc)
― ‹Demostración en lenguaje natural:
Por inducción en n con x arbitrario, hay que probar
∀n. (∀x. factI' n x = x * factR n)
+ Caso base: hay que probar ∀x. factI' 0 x = x * factR 0
En efecto, para cualquier x, se tiene factI' 0 x = x * factR 0,
aplicando directamenta las definiciones de ambas funciones.
+ Paso inductivo:
+ HI: ∀x. factI' n x = x * factR n
+ Hay que probar ∀x. factI' (n+1) x = x * factR (n+1)
En efecto, sea a cualquiera
factI' (n+1) a = (por def. de factI')
factI' n (a*(n+1)) = (por HI, para x = a*(n+1))
(a*(n+1))*(factR n) = (asociativa de *)
a*((n+1)*(factR n)) = (def. de factR)
a*(factR (n+1))
›
― ‹Demostración estructurada:›
lemma "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "⋀x. factI' n x = x * factR n"
show "⋀x. factI' (Suc n) x = x * factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
also have "... = (x * Suc n) * factR n" using HI by simp
also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc)
also have "... = x * factR (Suc n)" by simp
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed
qed
― ‹Demostración detallada declarativa:›
lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
fix x
have "factI' 0 x = x"
by (simp only: factI'.simps(1))
also have "... = x * 1"
by (simp only: mult_1_right)
also have "... = x * factR 0"
by (simp only: factR.simps(1))
finally show "factI' 0 x= x* factR 0"
by this
next
fix n
assume HI: " ⋀x. factI' n x = x *factR n"
show "⋀x. factI' (Suc n) x = x*factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x*Suc n)"
by (simp only: factI'.simps(2))
also have "... = (x*Suc n)*factR n"
by (simp only: HI)
also have "... = x*(Suc n*factR n)"
by (simp only: mult.assoc)
also have "... = x*factR (Suc n)"
by (simp only: factR.simps(2))
finally show "factI' (Suc n) x= x*factR (Suc n)"
by this
qed
qed
― ‹Demostración detallada aplicativa:›
lemma "factI' n x = x * factR n"
apply (induct n arbitrary: x)
apply (simp only: factI'.simps(1))
apply (simp only: factR.simps(1))
apply (simp only: factI'.simps(2))
apply (simp only: factR.simps(2))
done
text ‹ ---------------------------------------------------------------
Ejercicio 1.3. Demostrar que
factI n = factR n
------------------------------------------------------------------- ›
― ‹Demostración automática:›
corollary "factI n = factR n"
by (simp add: fact)
― ‹Demostración en lenguaje natural:
factI n = (def. de factI)
factI' n 1 = (lema fact)
1 * (factR n) = (1 es elemento neutro de *)
factR n
›
― ‹Demostración estructurada:›
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1"
by simp
also have "… = 1 * factR n"
by (simp add: fact)
also have "… = factR n"
by simp
finally show "factI n = factR n"
by this
qed
― ‹Demostración detallada declarativa:›
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1"
by (simp only: factI.simps)
also have "… = 1 * factR n"
by (simp only: fact)
also have "… = factR n"
by (simp only: nat_mult_1)
finally show "factI n = factR n"
by this
qed
text ‹
---------------------------------------------------------------------
Ejercicio 2. Definir la función
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
›
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"
text ‹
---------------------------------------------------------------------
Ejercicio 3. Definir la función
sinDuplicados :: 'a list ⇒ bool
tal que (sinDuplicados xs) se verifica si la lista xs no contiene
duplicados. Por ejemplo,
sinDuplicados [1::nat,4,2] = True
sinDuplicados [1::nat,4,2,4] = False
---------------------------------------------------------------------
›
fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = True"
| "sinDuplicados (a#xs) = ((¬ estaEn a xs) ∧ sinDuplicados xs)"
text ‹
---------------------------------------------------------------------
Ejercicio 4. Definir la función
borraDuplicados :: 'a list ⇒ bool
tal que (borraDuplicados xs) es la lista obtenida eliminando los
elementos duplicados de la lista xs. Por ejemplo,
borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]
Nota: La función borraDuplicados es equivalente a la predefinida
remdups.
---------------------------------------------------------------------
›
fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (a#xs) = (if estaEn a xs
then borraDuplicados xs
else (a#borraDuplicados xs))"
text ‹
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
›
― ‹Demostración automática:›
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) simp_all
― ‹Demostración en lenguaje natural:
Por inducción en xs.
+ Caso base:
length (borraDuplicados []) ≤ length [], directamente por las definciones.
+ Paso inductivo:
+ HI: length (borraDuplicados xs) ≤ length xs
+ Hay que probar: length (borraDuplicados (a#xs)) ≤ length (a#xs)
La demostración se realiza por casos:
+ Caso 1: estaEn a xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
length (borraDuplicados xs) ≤ (por HI)
length xs ≤ (aritmética)
1 + length xs = (por def. de length)
length (a#xs)
+ Caso 2: ¬ (estaEn a xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = a#(borraDuplicados xs). Por tanto,
length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
length (a#(borraDuplicados xs)) = (def. de length)
1 + length (borraDuplicados xs) ≤ (por HI)
1 + length xs = (por def. de length)
length (a#xs)
›
― ‹Demostración estructurada:›
lemma
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
proof (cases)
assume "estaEn a xs"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
using HI by simp
next
assume "(¬ estaEn a xs)"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
using HI by simp
qed
qed
― ‹Auxiliares para la demostración detallada:›
lemma estaEnBD1:
assumes "estaEn b xs"
shows "borraDuplicados (b#xs) = borraDuplicados xs"
using assms by (simp only:borraDuplicados.simps(2) if_P)
lemma estaEnBD2:
assumes "¬ (estaEn b xs)"
shows "borraDuplicados (b#xs) = b#(borraDuplicados xs)"
proof-
have "borraDuplicados (b#xs) = (if estaEn b xs
then borraDuplicados xs
else (b#borraDuplicados xs))"
by (simp only: borraDuplicados.simps(2))
also have "…= (b#borraDuplicados xs)" using assms by (rule if_not_P)
finally show "borraDuplicados (b # xs) = b # borraDuplicados xs" by this
qed
― ‹Demostración detallada declarativa:›
lemma length_borraDuplicados_d:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []"
by (simp only: borraDuplicados.simps(1) list.size)
next
fix a xs
assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
show "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
proof (cases)
assume "estaEn a xs"
then have "borraDuplicados (a#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "length (borraDuplicados (a#xs)) = length (borraDuplicados xs)"
by (rule arg_cong)
also have "... ≤ length xs" using HI by this
also have "... ≤ length (a#xs)" by (simp only: list.size)
finally show ?thesis by this
next
assume "(¬ estaEn a xs)"
then have "borraDuplicados (a#xs) = a#(borraDuplicados xs)"
by (rule estaEnBD2)
then have "length (borraDuplicados (a#xs)) = length (a#(borraDuplicados xs))"
by (rule arg_cong)
also have "... = 1 + length (borraDuplicados xs)" by (simp only: list.size)
also have "... ≤ 1 + length xs" using HI by (simp only: add_left_mono)
also have "... = length (a#xs)" by (simp only: list.size)
finally show ?thesis by this
qed
qed
― ‹Demostración aplicativa detallada:›
lemma length_borraDuplicados_a:
"length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply (simp only: borraDuplicados.simps(1) list.size)
apply (simp only: borraDuplicados.simps(2))
apply(split if_split)
apply (rule conjI)
apply (rule impI)
apply (drule estaEnBD1)
apply (simp only:list.size)
apply (rule impI)
apply (drule estaEnBD2)
apply (simp only:list.size)
done
text ‹
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
›
― ‹Demostración automática:›
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto
― ‹Demostración en lenguaje natural:
Por inducción en xs.
+ Caso base:
estaEn a (borraDuplicados []) = estaEn a [], directamente por las definiciones.
+ Paso inductivo:
+ HI: estaEn a (borraDuplicados xs) = estaEn a xs
+ Hay que probar: estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs).
La demostración se realiza por casos.
+ Caso 1: estaEn b xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (b#xs) = borraDuplicados xs. Por tanto,
estaEn a (borraDuplicados (b#xs)) = (def. de borraDuplicados)
estaEn a (borraDuplicados xs) = (por HI)
estaEn a xs = (por (estaEn b xs))
estaEn a (b#xs)
+ Caso 2: ¬ (estaEn b xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (b#xs) = b # (borraDuplicados xs). Por tanto,
estaEn a (borraDuplicados (b#xs)) = (def. de borraDuplicados)
estaEn a ( b # (borraDuplicados xs)) = (def. de estaEn)
(a = b) ∨ (estaEn a (borraDuplicados xs) = (por HI)
(a = b) ∨ (estaEn a xs = (def. de estaEn)
estaEn a (b#xs)
›
― ‹Demostración estructurada:›
lemma
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix b xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)"
proof (cases)
assume "estaEn b xs"
then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (borraDuplicados xs)" by (rule arg_cong)
also have "… = estaEn a xs" using HI by this
also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by auto
finally show ?thesis by this
next
assume " ¬ estaEn b xs"
then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
by (simp only: estaEn.simps(2))
also have "… = ((a = b) ∨ (estaEn a xs))" using HI by simp
also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
finally show ?thesis by this
qed
qed
― ‹Auxiliar:›
lemma estaEnCons:
assumes "estaEn b xs"
shows "estaEn a xs = estaEn a (b#xs)"
proof (rule iffI)
assume " estaEn a xs "
then have "((a = b) ∨ (estaEn a xs))" by (rule disjI2)
then show "estaEn a (b # xs)" by (simp only:estaEn.simps(2))
next
assume "estaEn a (b # xs)"
then have "((a = b) ∨ (estaEn a xs))" by (simp only:estaEn.simps(2))
then show "estaEn a xs"
proof
assume "a = b" then show "estaEn a xs" using assms by (rule ssubst)
next
assume "estaEn a xs" then show "estaEn a xs" by this
qed
qed
― ‹Demostración detallada declarativa:›
lemma estaEn_borraDuplicados_d:
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []"
by (simp only:borraDuplicados.simps(1))
next
fix b xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)"
proof (cases)
assume "estaEn b xs"
then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (borraDuplicados xs)" by (rule arg_cong)
also have "… = estaEn a xs" using HI by this
also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by (rule estaEnCons)
finally show ?thesis by this
next
assume " ¬ estaEn b xs"
then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
by (simp only: estaEn.simps(2))
also have "… = ((a = b) ∨ (estaEn a xs))" using HI by simp
also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
finally show ?thesis by this
qed
qed
― ‹Demostración detallada aplicativa:›
lemma
"estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply (simp only: borraDuplicados.simps(1))
apply (simp only: borraDuplicados.simps(2))
apply(split if_split)
apply (rule conjI)
apply (rule impI)
apply (simp only: estaEnCons)
apply (rule impI)
apply (simp only: estaEn.simps(2))
done
text ‹
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
›
― ‹Demostración automática:›
lemma "sinDuplicados (borraDuplicados xs)"
by (induct xs)
(auto simp add: estaEn_borraDuplicados_d)
― ‹Demostración en lenguaje natural:
Por inducción en xs.
+ Caso base:
sinDuplicados (borraDuplicados []), directamente por las definiciones.
+ Paso inductivo:
+ HI: sinDuplicados (borraDuplicados xs)
+ Hay que probar: sinDuplicados (borraDuplicados (a#xs))
La demostración se realiza por casos.
+ Caso 1: estaEn a xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
sinDuplicados (borraDuplicados (a#xs)) = (def.de borraDuplicados)
sinDuplicados (borraDuplicados xs) (cierto, por HI)
+ Caso 2: ¬ (estaEn a xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = a # (borraDuplicados xs). Por tanto,
sinDuplicados (borraDuplicados (a#xs)) = (def. de borraDuplicados)
sinDuplicados (a#(borraDuplicados xs)) = (def. de sinDuplicados)
((¬ estaEn a (borraDuplicados xs)) ∧
sinDuplicados (borraDuplicados xs)) = (por hI)
¬ estaEn a (borraDuplicados xs) (cierto por la hipótesis del
caso 2 y el ejercicio 6)
›
― ‹Demostración estructurada:›
lemma
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados (xs :: 'a list))"
show "sinDuplicados (borraDuplicados (a#xs))"
proof (cases)
assume "estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
next
assume "¬ estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))"
using `¬ estaEn a xs` HI by (auto simp add: estaEn_borraDuplicados_d)
qed
qed
― ‹Demostración detallada declarativa:›
lemma sinDuplicados_borraDuplicados_d:
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])"
by (simp only: borraDuplicados.simps(1)
sinDuplicados.simps(1))
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados (xs:: 'a list))"
show "sinDuplicados (borraDuplicados (a#xs))"
proof (cases)
assume "estaEn a xs"
then have "borraDuplicados (a#xs) = borraDuplicados xs"
by (rule estaEnBD1)
then show "sinDuplicados (borraDuplicados (a#xs))" using HI
by (rule ssubst)
next
assume 1: "¬ estaEn a xs"
then have 2: "borraDuplicados (a#xs) = a#(borraDuplicados xs)"
by (rule estaEnBD2)
have "¬ estaEn a (borraDuplicados xs)" using 1
by (simp add: estaEn_borraDuplicados_d)
then have "¬ (estaEn a (borraDuplicados xs))
∧ sinDuplicados (borraDuplicados xs)"
using HI by (rule conjI)
then have "sinDuplicados (a#(borraDuplicados xs))"
by (simp only: sinDuplicados.simps(2)[THEN sym])
with 2 show "sinDuplicados (borraDuplicados (a#xs))"
by (rule ssubst)
qed
qed
text ‹
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
›
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops
(*
Auto Quickcheck found a counterexample:
xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
borraDuplicados (rev xs) = [a⇩2, a⇩1]
rev (borraDuplicados xs) = [a⇩1, a⇩2]
*)
end
![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)