Relación 8
De Razonamiento automático (2014-15)
Revisión del 23:32 10 dic 2014 de Domcadgom (discusión | contribuciones)
header {* R8: Árboles binarios completos *}
theory R8_Arboles_binarios_completos
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir el tipo de datos arbol para representar los
árboles binarios que no tienen información ni en los nodos y ni en las
hojas. Por ejemplo, el árbol
·
/ \
/ \
· ·
/ \ / \
· · · ·
se representa por "N (N H H) (N H H)".
---------------------------------------------------------------------
*}
datatype arbol = H | N arbol arbol
value "N (N H H) (N H H)"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
hojas :: "arbol => nat"
tal que (hojas a) es el número de hojas del árbol a. Por ejemplo,
hojas (N (N H H) (N H H)) = 4
---------------------------------------------------------------------
*}
-- "javrodviv1 jeshorcob,davoremar, domcadgom"
fun hojas :: "arbol => nat" where
"hojas H = 1"
| "hojas (N i d) = hojas i + hojas d"
value "hojas (N (N H H) (N H H))" -- "= 4"
text {*
---------------------------------------------------------------------
Ejercicio 4. Definir la función
profundidad :: "arbol => nat"
tal que (profundidad a) es la profundidad del árbol a. Por ejemplo,
profundidad (N (N H H) (N H H)) = 2
---------------------------------------------------------------------
*}
-- "javrodviv1"
fun max :: "nat ⇒ nat ⇒ nat" where
"max a b= (if a≥ b then a else b)"
value "max 6 3" -- "= 6"
--"davoremar"
fun profundidad :: "arbol => nat" where
"profundidad H = 0"
| "profundidad (N a b) = 1 + max (profundidad a) (profundidad b)"
value "profundidad (N (N H H) (N H H))" -- "= 2"
(* Javrodviv1: Explico estas dos funciones, la que utilizo para los
lemas de abajo es profundidad ya que profundidad1 me encuentra
contraejemplos y para evitar eso busque definir profundidad
definidad de manera distinta. No obstante la que a mi me parece
mas sensata para definir la profundidad de un árbol es la
profundidad1 *)
(* Javrodviv1: Fallo mio ya lo corregí*)
(*Pedrosrei: La profundidad correcta es la mayor. Si te encuentra
contraejemplos más adelante es que te has equivocado en los
enunciados. Las funciones máximo y mínimo vienen predefinidas
ya sin necesidad de definirlas. *)
--"jeshorcob, domcadgom"
fun pr1 :: "arbol => nat" where
"pr1 H = 0"
|"pr1 (N i d) = Suc(max (pr1 i) (pr1 d))"
text {*
---------------------------------------------------------------------
Ejercicio 5. Definir la función
abc :: "nat ⇒ arbol"
tal que (abc n) es el árbol binario completo de profundidad n. Por
ejemplo,
abc 3 = N (N (N H H) (N H H)) (N (N H H) (N H H))
---------------------------------------------------------------------
*}
-- "javrodviv1 jeshorcob,davoremar, domcadgom"
fun abc :: "nat ⇒ arbol" where
"abc 0 = H"
| "abc (Suc n) = N (abc n) (abc n)"
--"jeshorcob" (*¿Pudiera ser que esta sea más rápida?*)
fun abc1 :: "nat ⇒ arbol" where
"abc1 0 = H"
|"abc1 (Suc n) = (let a = abc1 n in N a a)"
value "abc 3" -- "= N (N (N H H) (N H H)) (N (N H H) (N H H))"
text {*
---------------------------------------------------------------------
Ejercicio 6. Un árbol binario a es completo respecto de la medida f si
a es una hoja o bien a es de la forma (N i d) y se cumple que tanto i
como d son árboles binarios completos respecto de f y, además,
f(i) = f(r).
Definir la función
es_abc :: "(arbol => 'a) => arbol => bool
tal que (es_abc f a) se verifica si a es un árbol binario completo
respecto de f.
---------------------------------------------------------------------
*}
-- "javrodviv1"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
| "es_abc f (N a b) = ((f a = f b) ∧ (es_abc f a ∧ es_abc f b))"
--"jeshorcob,davoremar, domcadgom"
fun es_abc :: "(arbol => 'a) => arbol => bool" where
"es_abc f H = True"
|"es_abc f (N i d) = (f i = f d ∧ es_abc f i ∧ es_abc f d)"
text {*
---------------------------------------------------------------------
Nota. (size a) es el número de nodos del árbol a. Por ejemplo,
size (N (N H H) (N H H)) = 3
---------------------------------------------------------------------
*}
text{*Para entenderme he cambiado de función de tamaño, la demostración
es análoga pero buscando las simplificaciones de size cuando correspondan
*}
fun nodos::"arbol ⇒ nat" where
"nodos H = 0"
|"nodos (N i d) = 1+(nodos i)+(nodos d)"
lemma "size t= nodos t"
apply (induct t, auto)done
value "size (N (N H H) (N H H))"
value "size (N (N (N H H) (N H H)) (N (N H H) (N H H)))"
text {*
---------------------------------------------------------------------
Nota. Tenemos 3 funciones de medida sobre los árboles: número de
hojas, número de nodos y profundidad. A cada una le corresponde un
concepto de completitud. En los siguientes ejercicios demostraremos
que los tres conceptos de completitud son iguales.
---------------------------------------------------------------------
*}
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de hojas.
---------------------------------------------------------------------
*}
text{*Pedrosrei: Los enunciados y demostraciones que vienen a continuación
son feos y engorrosos. Yo he optado por demostrarlo todo a través de
una propiedad extraña a la demostración en principio. Animo encarecidamente
a que pongáis una demostración más corta y directa. Voy explicando paso
a paso qué he hecho en cada momento. Hecha esta demostración, el resto
son triviales por una cadena de resultados.
No existe relación de implicación en ningún sentido
entre hojas y profundidad, como es obvio y muestran los siguientes
contraejemplos: *}
lemma "(((hojas(t1) = hojas(t2)))-->(profundidad(t1) = profundidad(t2)))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) -->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
lemma "((profundidad(t1) = profundidad(t2)) <->
((hojas(t1) = hojas(t2))))"
quickcheck
oops
text {* Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
t1 = N (N H H) (N H H)
t2 = N H (N H H)
Evaluated terms:
hojas t1 = 4
hojas t2 = 3
Ahora pongo una serie de resultados auxiliares que ayudarán en la prueba
*}
lemma auxprof:"(es_abc profundidad t)∧(profundidad t = n)==> (t= abc n)"
apply (induct t arbitrary:n, auto)done
lemma eq_1_iff_exp_0:"Suc 0 = 2 ^ n <-> n=0" apply (cases n, auto) done
lemma auxhojas:"(t= abc n)==> (es_abc hojas t)"
apply (induct n arbitrary: t, auto simp add: eq_1_iff_exp_0) done
lemma auxhoja:"(t= abc n)==>((hojas t = 2^n))"
apply (induct n arbitrary: t rule: abc.induct, auto)done
text{* Pedrosrei. Y aquí viene la demostración larga y fea que os animo a mejorar.
He dejado los pasos exactamente que indica el razonador para que
veáis qué hace en cada caso:
*}
lemma prof_eq_hoja:"es_abc profundidad t <-> es_abc hojas t"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc hojas t" using auxhojas by auto
next
show "es_abc hojas t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc hojas t1 ==>
es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc hojas t1"
thus "es_abc hojas t2 ==>
hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc hojas t2"
thus "hojas t1 = hojas t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"hojas t1 = hojas t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc hojas t1" using auxhojas by auto
have "hojas t1 = (2::nat)^n" using 2 auxhoja by auto
hence 3:"hojas t2 = (2::nat)^n" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc hojas t2" using auxhojas by auto
have "hojas t2 = (2::nat)^m" using 5 auxhoja by auto
with 3 have " (2::nat)^m = (2::nat) ^n" by auto
hence "m = n" apply (induct, auto)done
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed
(*jeshorcob: creo que tengo una demostración mas elegante tan
sólo hace falta encontrar la relacion entre hojas y profundidad*)
--"jeshorcob"
lemma a1:
assumes "es_abc hojas a"
shows "hojas a = 2^(pr1 a)"
using assms by (induct a, simp_all)
--"jeshorcob"
lemma cpr1_chojas: "es_abc pr1 a = es_abc hojas a"
by (induct a, auto simp add: a1)
(*jeshorcob: esta la detallada*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc hojas a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc pr1 (N i d) =
(pr1 i = pr1 d ∧ es_abc pr1 i ∧ es_abc pr1 d )" by simp
also have "... = (pr1 i = pr1 d ∧ es_abc hojas i ∧ es_abc hojas d)"
using h1 and h2 by simp
also have "... = (hojas i = hojas d
∧ es_abc hojas i ∧ es_abc hojas d)" using a1 by auto
also have "... = es_abc hojas (N i d)" by simp
finally show "?P (N i d)" by simp
qed
-- "domcadgom"
lemma aux1: "(es_abc profundidad a) ⟹ (hojas a) = (2^(profundidad a))"
by (induct a,simp_all)
lemma completo1: "(es_abc (profundidad) a) = (es_abc (hojas) a)"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc profundidad a1 = es_abc hojas a1"
assume a2: "es_abc profundidad a1 = es_abc hojas a1"
assume a3: "es_abc profundidad a2 = es_abc hojas a2"
assume a4: "es_abc profundidad a2 = es_abc hojas a2"
have "es_abc profundidad a2 ∧ es_abc profundidad a1 ⟶ es_abc profundidad
(N a1 a2) = es_abc hojas (N a1 a2)" using a1 a3 by (simp add: aux1)
thus "es_abc profundidad (N a1 a2) = es_abc hojas (N a1 a2)"
using a2 a4 es_abc.simps(2) by blast
qed
text {*
---------------------------------------------------------------------
Ejercicio 8. Demostrar que un árbol binario a es completo respecto del
número de hojas syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
(* Javrodviv1: Bueno yo para este ejercicio he encontrado algo mas sencillo,
tan solo hay que encontrar una relación de igualdad entre hojas y size,
que para este caso es sencillo.*)
-- "Javrodviv1"
lemma hojasize_igualdad:
"hojas x = size x + 1"
by (induct x, simp_all)
(*lemma "es_abc size a <-> es_abc hojas a" Son equivalentes = es lo mismo que <->
matemáticamente hablando*)
lemma " es_abc size a = es_abc hojas a"
quickcheck
by (induct a, simp_all add: hojasize_igualdad)
text{* Pedrosrei. Aquí dejo esta. Es trivial debido a la demostración anterior,
sólo hace falta coger el mismo desvío. Aquí sí que podéis encontrar
una mucho más directa: *}
lemma auxnodo:"(t= abc n)==>(es_abc nodos t)∧(nodos t = (2^n - 1))"
apply (induct n arbitrary: t rule: abc.induct, auto)done
lemma nodos_eq_hoja:"es_abc nodos t <-> es_abc hojas t" (is "?P t")
proof -
have 1:"es_abc hojas t <-> es_abc profundidad t" using prof_eq_hoja by auto
hence 2:"?P t = (es_abc profundidad t <-> es_abc nodos t)" by auto
have "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed
with 1 2 show ?thesis by auto
qed
(*jeshorcob: aquí similar*)
--"jeshorcob"
lemma a2:
assumes "es_abc size a"
shows "hojas a = (size a) + 1"
using assms by (induct a, simp_all)
--"jeshorcob"
lemma chojas_cnodos: "es_abc hojas a = es_abc size a"
by (induct a, auto simp add: a2)
--"jeshorcob"
lemma "es_abc hojas a = es_abc size a" (is "?P a")
proof (induct a)
show "?P H" by simp
next
fix i d
assume h1: "?P i"
assume h2: "?P d"
have "es_abc hojas (N i d) =
(hojas i = hojas d ∧ es_abc hojas i ∧ es_abc hojas d )" by simp
also have "... = (hojas i = hojas d ∧ es_abc size i ∧ es_abc size d)"
using h1 and h2 by simp
also have "... = (size i = size d
∧ es_abc size i ∧ es_abc size d)" using a2 by auto
also have "... = es_abc size (N i d)" by simp
finally show "?P (N i d)" by simp
qed
--"domcadgom"
lemma aux2: "(es_abc size a) ⟹ ((hojas a) = ((size a) +1))"
by (induct a, simp_all)
lemma completo2: "es_abc hojas a = es_abc (size) a"
proof (induct a, simp)
fix a1 :: arbol and a2 :: arbol
assume a1: "es_abc hojas a1 = es_abc size a1"
assume a2: "es_abc hojas a2 = es_abc size a2"
hence "es_abc hojas a2 ∧ es_abc hojas a1 ⟶
es_abc hojas (N a1 a2) = es_abc size (N a1 a2)" using a1 aux2 by auto
thus "es_abc hojas (N a1 a2) = es_abc size (N a1 a2)"
using a1 a2 es_abc.simps(2) by blast
qed
text {*
---------------------------------------------------------------------
Ejercicio 9. Demostrar que un árbol binario a es completo respecto de
la profundidad syss es completo respecto del número de nodos
---------------------------------------------------------------------
*}
text {* Pedrosrei. De hecho, esta es una parte de la anterior: *}
lemma prof_eq_nodos: "(es_abc profundidad t <-> es_abc nodos t)"
proof
assume a1:"es_abc profundidad t"
have "∀t. ∃n. n = profundidad t" by auto
then obtain n where "n = profundidad t" by auto
with a1 have 1:"t= abc n" using auxprof by auto
thus "es_abc nodos t" using auxnodo by auto
next
show "es_abc nodos t ==> es_abc profundidad t" apply (induct t, auto)
proof -
fix t1 t2
assume a1:"es_abc profundidad t1"
thus "es_abc profundidad t2 ==>
es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a2:"es_abc profundidad t2"
thus "es_abc nodos t1 ==>
es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a3:"es_abc nodos t1"
thus "es_abc nodos t2 ==>
nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2"proof-
assume a4:"es_abc nodos t2"
thus "nodos t1 = nodos t2 ==>
profundidad t1 = profundidad t2" proof -
assume a5:"nodos t1 = nodos t2"
thus "profundidad t1 = profundidad t2"
proof-
obtain n where 1:"profundidad t1 = n" by auto
with a1 have 2:"t1 = abc n"using auxprof by auto
hence 3:"es_abc nodos t1" using auxnodo by auto
have "nodos t1 = (2::nat)^n - 1" using 2 auxnodo by auto
hence 3:"nodos t2 = (2::nat)^n - 1" using a5 by auto
obtain m where 4:"profundidad t2 = m" by auto
with a2 have 5:"t2 = abc m"using auxprof by auto
hence 6:"es_abc nodos t2" using auxnodo by auto
have "nodos t2 = (2::nat)^m - 1" using 5 auxnodo by auto
with 3 have 7:" (2::nat)^m - 1 = (2::nat) ^n - 1" by auto
hence "m = n" proof -
have " (2::nat)^m - 1 = (2::nat) ^n - 1"using 7 by auto
hence "(2::nat)^m - 1 + 1 = (2::nat) ^n" by auto
hence "(2::nat)^m = (2::nat) ^n" by auto
thus ?thesis apply (induct, auto)done
qed
hence "t2 = abc n" using 5 by auto
with 2 have "t1= t2" by auto
thus "profundidad t1 = profundidad t2" by auto
qed
qed
qed
qed
qed
qed
qed
(*jeshorcob: sale directo como corolario de los anteriores*)
--"jeshorcob"
lemma "es_abc pr1 a = es_abc size a"
using cpr1_chojas and chojas_cnodos by simp_all
--"domcadgom"
corollary completo3: "es_abc profundidad a = es_abc size a"
using completo1 completo2 by simp
text {*
---------------------------------------------------------------------
Ejercicio 10. Demostrar que (abc n) es un árbol binario completo.
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma " es_abc f (abc n)"
apply (induct n, auto) done
--"jeshorcob,davoremar, domcadgom"
lemma "es_abc f (abc n)"
by (induct n, simp_all)
--"jeshorcob"
lemma "es_abc f (abc n)" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n assume h: "?P n"
have "es_abc f (abc (Suc n)) = es_abc f (N (abc n) (abc n))" by simp
also have "... = (f (abc n) = f (abc n) ∧
es_abc f (abc n) ∧ es_abc f (abc n))" by simp
also have "... = True" using h by simp
finally show "?P (Suc n)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que si a es un árbolo binario completo
respecto de la profundidad, entonces a es (abc (profundidad a)).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc profundidad a ==> (a= abc (profundidad a))"
apply (induct a, auto) done
--"jeshorcob"
lemma "es_abc pr1 a ⟹ (a = abc (pr1 a))"
by (induct a, simp_all)
--"davoremar, domcadgom"
lemma "es_abc profundidad a ⟹ (a = abc (profundidad a))"
by (induct a, simp_all)
text {*
---------------------------------------------------------------------
Ejercicio 12. Encontrar una medida f tal que (es_abc f) es distinto de
(es_abc size).
---------------------------------------------------------------------
*}
--"Pedrosrei:"
lemma "es_abc f = es_abc nodos
quickcheck
oops
text {*
El contraejemplo no es más que una medida constante, la trivial:
Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
f = λx. a⇣1
x = N H (N H H)
Evaluated terms:
es_abc f x = True
es_abc R8_Arboles_binarios_completos.size x = False
*}
(*jeshorcob: usando size en lugar de nodos, se encuentra el
mismo contraejemplo*)
--"jeshorcob, domcadgom"
lemma "es_abc f = es_abc size"
quickcheck
(*
el contraejemplo es:
f = λx. a⇩1
x = N H (N H H)
Evaluated terms:
es_abc f x = True
es_abc size x = False
*)
--"davoremar"
lemma "es_abc f t = es_abc size t"
quickcheck
oops
end