Lógica matemática y fundamentos (2014-15) - Contribuciones del usuario [es]

Relación 5

2015-04-04T11:06:02Z

Adrguede:

<source lang="isar">
header {* R5: Argumentación en lógica de primer orden *}

theory R5_sol
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio1
assumes "H(s)"
"H(x) ⟶ M(x)"
shows "M(s)"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio2
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. I(x) ∧ T(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}
lemma ejercicio3:
assumes 1: "∀x. (P(x)⟶V(x))" and
2: "(¬(∃x. V(x))) ∨ (∃x. (V(x) ∧ (∀y. (V(y) ⟶ x=y))))" and
3: "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))"
shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
proof -
obtain a where 4: "(Co(a) ∧ E(a)) ∧ (∀y. (Ca(y,a)⟶Co(y)))" using 2 by (rule exE)
have 5: "Co(a) ∧ E(a)" using 4 by (rule conjunct1)
have 6: "Co(a)" using 5 by (rule conjunct1)
have 7: "E(a)" using 5 by (rule conjunct2)
have 8: "∀y. (Ca(y,a)⟶Co(y))" using 4 by (rule conjunct2)
have 9: "Co(a) ⟶ ¬V(a)" using 3 by (rule allE)
have 10: "¬V(a)" using 9 6 by (rule mp)
have 11: "(E(a)∧ ¬V(a)) ⟶ (∃y. (A(y) ∧ Ca(y,a)))" using 1 by (rule allE)
have 12: "E(a) ∧ ¬V(a)" using 7 10 by (rule conjI)
have 13: "∃y. (A(y) ∧ Ca(y,a))" using 11 12 by (rule mp)
obtain b where 14: "A(b) ∧ Ca(b,a)" using 13 by (rule exE)
have 15: "A(b)" using 14 by (rule conjunct1)
have 16: "Ca(b,a)⟶Co(b)" using 8 by (rule allE)
have 17: "Ca(b,a)" using 14 by (rule conjunct2)
have 18: "Co(b)" using 16 17 by (rule mp)
have 19: "A(b) ∧ Co(b)" using 15 18 by (rule conjI)
show 20: "∃x. (A(x) ∧ Co(x))" using 19 by (rule exI)
qed

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}
lemma ejercicio4:
assumes 1: "∀x. ((E(x) ∧ ¬V(x)) ⟶ (∃y. (A(y) ∧ Ca(y,x))))" and
2: "∃x. ((Co(x) ∧ E(x)) ∧ (∀y. (Ca(y,x) ⟶ Co(y))))" and
3: "∀x. (Co(x)⟶ ¬V(x))"
shows "∃x. (A(x) ∧ Co(x))"
oops

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio5
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio6
assumes "∀x y z. H(x,y) ⟶ P(z,x) ∧ P(z,y)"
"H(x,y) → H(y,x)"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_7:
assumes "∀x. ∀y. (Pu x ∧ Pr y ⟶ A y)"
"∀x. ∀y. (A x ∧ D y x) ⟶ S y"
"∃x. Pu x"
"Pr t"
shows "∀x. D x t ⟶ S x"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
Quien intente entrar en un país y no tenga pasaporte, encontrará
algún aduanero que le impida el paso. A algunas personas
motorizadas que intentan entrar en un país le impiden el paso
únicamente personas motorizadas. Ninguna persona motorizada tiene
pasaporte. Por tanto, ciertos aduaneros están motorizados.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio8
assumes "∀x. E(x) ∧ ¬P(x) ⟶ ∃z. A(z) ∧ I(z,x)"
"∃x. M(x) ⟶ ∃z. M(z) ∧ I(z,x)"
"M(x) ⟶ ¬P(x)"
shows "∃x. A(x) ∧ M(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio9
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_11:
assumes "∀x. ∀y. (C x y ⟶ (A x y ∨ I x))"
"∀x. (I x ⟶ ¬(R x))"
"∀x. (E x ⟶ (C x m ∧ ¬(A x m)))"
shows "∀x. (¬(E x) ∨ (C x m ∧ ¬(R x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

-- Adrian Guerra

lemma ejercicio_12:
assumes "∀x. ¬(R x) ⟶ R (p x)"
shows "∃x. (R x ∧ R(p (p x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_13:
assumes "∀x. ∀y. ((D x ∧ S y ∧ E x y) ⟶ L x)"
"∀x. (E x x ⟶ L x)"
"¬(∃x. (D x ∧ E x x))"
shows "¬(∃x. ∃y. (D x ∧ S y ∧ E x y))"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

-- Adrian Guerra

lemma ejercicio_14:
assumes "∀x. ∀y. ((A x ∧ R y) ⟶ Ob y x)"
"A a"
"¬(Ob b a)"
shows "¬(R b)"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_15:
assumes "∃x. (∀y. (¬(C x y) ⟶ (∃z. (T z ∨ P z y))))"
"¬(∃x. (∀y. C x y))"
"¬(∃x. (∃y. P x y))"
shows "∃x. T x"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_16:
assumes "(∀x. (A x a)) ⟶ (∀y.(A x b))"
"(∃x. (D x ∧ A x a ∧ A x b)) ⟶ (∀y. A y a)"
"¬(∃x. A x b) ⟶ ¬((∃y. (D y ∧ A y a)))"
"¬(A m b) ⟶ ¬(∃x. A x b)"
shows "(D m ∧ A m a) ⟶ (∀x. (A x a ∧ A x b))"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_18:
assumes "∀x. ∀y. (He x y ⟷ He y x)"
"∀x. (∃y. Hi y x)"
"¬(∃x y z. (He x y ∧ Hi z x ∧ Hi z y))"
"∀x y z. ((Hi y x ∧ He y z) ⟶ Hi z x)"
"¬(∃x. (He x x ∨ Hi x x))"
"He A L"
"He a m"
"Hi a A"
shows "¬(Hi m L)"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_20:
assumes "∀x. ((C x ∧ ¬(A x x)) ⟷ A c x)"
"C c"
shows "¬(∃x. A c x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_22:
assumes "∀x. ∀y. ((P x ∧ H y ∧ P y) ⟶ A x y)"
shows "∀x. ((H x ∧ P x) ⟶ A x x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_23:
assumes "¬(∃x. (P x ∧ R x))"
"∀x. ((P x ∧ ¬(Q x))⟶ R x)"
shows "P a ⟶ Q a"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 5

2015-04-04T11:03:10Z

Adrguede:

<source lang="isar">
header {* R5: Argumentación en lógica de primer orden *}

theory R5_sol
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio1
assumes "H(s)"
"H(x) ⟶ M(x)"
shows "M(s)"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio2
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. I(x) ∧ T(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}
lemma ejercicio3:
assumes 1: "∀x. (P(x)⟶V(x))" and
2: "(¬(∃x. V(x))) ∨ (∃x. (V(x) ∧ (∀y. (V(y) ⟶ x=y))))" and
3: "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))"
shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
proof -
obtain a where 4: "(Co(a) ∧ E(a)) ∧ (∀y. (Ca(y,a)⟶Co(y)))" using 2 by (rule exE)
have 5: "Co(a) ∧ E(a)" using 4 by (rule conjunct1)
have 6: "Co(a)" using 5 by (rule conjunct1)
have 7: "E(a)" using 5 by (rule conjunct2)
have 8: "∀y. (Ca(y,a)⟶Co(y))" using 4 by (rule conjunct2)
have 9: "Co(a) ⟶ ¬V(a)" using 3 by (rule allE)
have 10: "¬V(a)" using 9 6 by (rule mp)
have 11: "(E(a)∧ ¬V(a)) ⟶ (∃y. (A(y) ∧ Ca(y,a)))" using 1 by (rule allE)
have 12: "E(a) ∧ ¬V(a)" using 7 10 by (rule conjI)
have 13: "∃y. (A(y) ∧ Ca(y,a))" using 11 12 by (rule mp)
obtain b where 14: "A(b) ∧ Ca(b,a)" using 13 by (rule exE)
have 15: "A(b)" using 14 by (rule conjunct1)
have 16: "Ca(b,a)⟶Co(b)" using 8 by (rule allE)
have 17: "Ca(b,a)" using 14 by (rule conjunct2)
have 18: "Co(b)" using 16 17 by (rule mp)
have 19: "A(b) ∧ Co(b)" using 15 18 by (rule conjI)
show 20: "∃x. (A(x) ∧ Co(x))" using 19 by (rule exI)
qed

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}
lemma ejercicio4:
assumes 1: "∀x. ((E(x) ∧ ¬V(x)) ⟶ (∃y. (A(y) ∧ Ca(y,x))))" and
2: "∃x. ((Co(x) ∧ E(x)) ∧ (∀y. (Ca(y,x) ⟶ Co(y))))" and
3: "∀x. (Co(x)⟶ ¬V(x))"
shows "∃x. (A(x) ∧ Co(x))"
oops

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio5
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio6
assumes "∀x y z. H(x,y) ⟶ P(z,x) ∧ P(z,y)"
"H(x,y) → H(y,x)"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_7:
assumes "∀x. ∀y. (Pu x ∧ Pr y ⟶ A y)"
"∀x. ∀y. (A x ∧ D y x) ⟶ S y"
"∃x. Pu x"
"Pr t"
shows "∀x. D x t ⟶ S x"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
Quien intente entrar en un país y no tenga pasaporte, encontrará
algún aduanero que le impida el paso. A algunas personas
motorizadas que intentan entrar en un país le impiden el paso
únicamente personas motorizadas. Ninguna persona motorizada tiene
pasaporte. Por tanto, ciertos aduaneros están motorizados.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio8
assumes "∀x. E(x) ∧ ¬P(x) ⟶ ∃z. A(z) ∧ I(z,x)"
"∃x. M(x) ⟶ ∃z. M(z) ∧ I(z,x)"
"M(x) ⟶ ¬P(x)"
shows "∃x. A(x) ∧ M(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio9
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_11:
assumes "∀x. ∀y. (C x y ⟶ (A x y ∨ I x))"
"∀x. (I x ⟶ ¬(R x))"
"∀x. (E x ⟶ (C x m ∧ ¬(A x m)))"
shows "∀x. (¬(E x) ∨ (C x m ∧ ¬(R x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

-- Adrian Guerra

lemma ejercicio_12:
assumes "∀x. ¬(R x) ⟶ R (p x)"
shows "∃x. (R x ∧ R(p (p x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 1

2015-02-15T16:55:25Z

Adrguede:

<source lang = "haskell">
-- LMF 2014-15: Rel_1.hs (9 de Febrero de 2015)
-- Introducción a la programación con Haskell.
-- Departamento de Ciencias de la Computación e I.A.
-- Universidad de Sevilla
-- =====================================================================

-- ---------------------------------------------------------------------
-- Introducción --
-- ---------------------------------------------------------------------

-- En esta relación de ejercicios hacemos una introducción a Haskell, en
-- la que se recuerdan:
-- * las definiciones elementales de funciones,
-- * las definiciones de funciones por comprensión,
-- * las definiciones de funciones por recursión y
-- * los tipos de datos.

-- ---------------------------------------------------------------------
-- Importación de librerías auxiliares
-- ---------------------------------------------------------------------

import Test.QuickCheck
import Data.Char
import Control.Monad

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función media3 tal que (media3 x y z) es
-- la media aritmética de los números x, y y z. Por ejemplo,
-- media3 1 3 8 == 4.0
-- media3 (-1) 0 7 == 2.0
-- media3 (-3) 0 3 == 0.0
-- ---------------------------------------------------------------------

media3 x y z = (x+y+z)/3

-- Miriam R.
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 2. Definir la función ultimaCifra tal que (ultimaCifra x)
-- es la última cifra del nímero x. Por ejemplo,
-- ultimaCifra 325 == 5
-- ---------------------------------------------------------------------

ultimaCifra x = rem x 10

-- Miriam R.
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 3. Definir la función rota tal que (rota n xs) es la lista
-- obtenida poniendo los n primeros elementos de xs al final de la
-- lista. Por ejemplo,
-- rota 1 [3,2,5,7] == [2,5,7,3]
-- rota 2 [3,2,5,7] == [5,7,3,2]
-- rota 3 [3,2,5,7] == [7,3,2,5]
-- ---------------------------------------------------------------------

rota n xs= (drop n xs) ++ (take n xs)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- Ejercicio 4.1. La disyunción excluyente xor de dos fórmulas se
-- verifica si una es verdadera y la otra es falsa.
--
-- Definir la función xor_1 que calcule la disyunción excluyente a
-- partir de la tabla de verdad. Usar 4 ecuaciones, una por cada línea
-- de la tabla.
-- ---------------------------------------------------------------------

xor_1 :: Bool -> Bool -> Bool
xor_1 True True = False
xor_1 True False = True
xor_1 False True = True
xor_1 False False = False

-- Pablo José Gerlach Mena
-- Rocio Rodriguez

xor_1 :: Bool -> Bool -> Bool
xor_1 x y |x== True && y== True = False
|x== True && y== False = True
|x== False && y== True = True
|x== False && y== False = False
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 4.2. Definir la función xor_2 que calcule la disyunción
-- excluyente a partir de la tabla de verdad y patrones. Usar 2
-- ecuaciones, una por cada valor del primer argumento.
-- ---------------------------------------------------------------------

xor_2 :: Bool -> Bool -> Bool
xor_2 True x = if x then False else True
xor_2 False x = if x then True else False

-- Pablo José Gerlach Mena

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

xor_2' True x = not x
xor_2' False x = x

-- Jaime Alberto
xor_2'' :: Bool -> Bool -> Bool
xor_2'' x y | x== True && y== True || x==False && y== False = False
| x== True && y== False || x== False && y== True = True

-- Elisa Mazuelos Jiménez:

xor_2 :: Bool -> Bool -> Bool
xor_2 True x | x == True = False
| otherwise = True
xor_2 False x | x == False = False
| otherwise = True

-- Esta última no es correcta (10/02/2015).
-- Corregida, gracias (10/02/2015).

-- ---------------------------------------------------------------------
-- Ejercicio 4.3. Definir la función xor_3 que calcule la disyunción
-- excluyente a partir de la disyunción (||), conjunción (&&) y negación
-- (not). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_3 :: Bool -> Bool -> Bool
xor_3 x y = (x && (not y)) || ((not x) && y)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-----------------------------------------------------
-- Ejercicio 4.4. Definir la función xor_4 que calcule la disyunción
-- excluyente a partir de desigualdad (/=). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_4 :: Bool -> Bool -> Bool
xor_4 x y = x /= y

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- Ejercicio 5. Definir, por comprensión, la función
-- sumaDeCuadrados :: Integer -> Integer
-- tal que (sumaDeCuadrados n) es la suma de los cuadrados de los
-- primeros n números; es decir, 1^2 + 2^2 + ... + 100^2. Por ejemplo,
-- sumaDeCuadrados 3 == 14
-- sumaDeCuadrados 100 == 338350
-- ---------------------------------------------------------------------

sumaDeCuadrados n = sum [x^2 | x <- [1..n]]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 6. Una terna (x,y,z) de enteros positivos es pitagórica si
-- x^2 + y^2 = z^2. Usando una lista por comprensión, definir la función
-- pitagoricas :: Int -> [(Int, Int, Int)]
-- tal que (pitagoricas n) es la lista de todas las ternas pitagóricas
-- cuyas componentes están entre 1 y n. Por ejemplo,
-- *Main> pitagoricas 10
-- [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]
-- ---------------------------------------------------------------------

pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [(x,y,z) | x <- [1..n], y <- [1..n], z <- [1..n], x^2+y^2 == z^2]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- Luis Curquejo. Solución acotando ligeramente los elementos x e y.

pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [ (x,y,z) | z <- [1..n], x <- [1..z], y <- [1..z] , x^2 + y^2 == z^2]

-- ---------------------------------------------------------------------
-- Ejercicio 7. Un entero positivo es perfecto si es igual a la suma de
-- sus factores, excluyendo el propio número. Usando una lista por
-- comprensión y la función factores (del tema), definir la función
-- perfectos :: Int -> [Int]
-- tal que (perfectos n) es la lista de todos los números perfectos
-- menores que n. Por ejemplo:
-- *Main> perfectos 500
-- [6,28,496]
-- ---------------------------------------------------------------------

perfectos :: Int -> [Int]
perfectos n = [x | x <- [1..n], esPerfecto x]

-- Definimos las funciones auxiliares:

factores :: Int -> [Int]
factores n = [x | x <- [1..n], n `mod` x == 0]

esPerfecto :: Int -> Bool
esPerfecto n = sum (factores n) == 2*n

-- También podríamos definirla como:

perfectos2 :: Int -> [Int]
perfectos2 n = filter (esPerfecto) [1..n]

-- Podemos comprobar que ambas definiciones son equivalentes:

prop_perfectos n = perfectos n == perfectos2 n

-- Si queremos podemos comparar ambos algoritmos:

-- *Main> perfectos 500
-- [6,28,496]
-- (1.44 secs, 15935120 bytes)

-- *Main> perfectos2 500
-- [6,28,496]
-- (0.22 secs, 14803544 bytes)

-- Es decir, el segundo es más eficiente.

-- Pablo José Gerlach Mena

-- Rocio Rodriguez
perfectos x = [y|y<-[1..x-1], serPerfecto y]
serPerfecto x = x==sum (factores' x)
factores x = [y|y<-[1..x], rem x y == 0]
factores' x = init (factores x)

-- Luis Curquejo

perfectos :: Int -> [Int]
perfectos n = [ x | x <- [1..n], x == sum (factoresred x)]
where factoresred x = [ y | y <- [1..x-1], rem x y == 0]

-- Francisco Javier Carmona

perfectos1 :: Int -> [Int]
perfectos1 n = [ x | x <- [1..n],
x == sum (tail(reverse (factores x)))]

factores1 n = [x | x <- [1..n], rem n x == 0]

-- ---------------------------------------------------------------------
-- Ejercicio 8.1. Definir, por comprensión, la función
-- cuadradosC :: [Integer] -> [Integer]
-- tal que (cuadradosC xs) es la lista de los cuadrados de xs. Por
-- ejemplo,
-- cuadradosC [1,2,3] == [1,4,9]
-- ---------------------------------------------------------------------

cuadradosC :: [Integer] -> [Integer]
cuadradosC xs = [x^2 | x <- xs]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 8.2. Definir, por recursión, la función
-- cuadradosR :: [Integer] -> [Integer]
-- tal que (cuadradosR xs) es la lista de los cuadrados de xs. Por
-- ejemplo,
-- cuadradosR [1,2,3] == [1,4,9]
-- ---------------------------------------------------------------------

cuadradosR :: [Integer] -> [Integer]
cuadradosR [] = []
cuadradosR (x:xs) = (x^2):(cuadradosR xs)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.1. Definir, por comprensión, la función
-- imparesC :: [Integer] -> [Integer]
-- tal que (imparesC xs) es la lista de los números impares de xs. Por
-- ejemplo,
-- imparesC [1,2,3] == [1,3]
-- ---------------------------------------------------------------------

imparesC :: [Integer] -> [Integer]
imparesC xs = [x | x <- xs, odd x]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.2. Definir, por recursión, la función
-- imparesR :: [Integer] -> [Integer]
-- tal que (imparesR xs) es la lista de los números impares de xs. Por
-- ejemplo,
-- imparesR [1,2,3] == [1,3]
-- ---------------------------------------------------------------------

imparesR :: [Integer] -> [Integer]
imparesR [] = []
imparesR (x:xs) | odd x = x:(imparesR xs)
| otherwise = imparesR xs

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 10. Definir, por comprensión, la función
-- sumaConsecutivos :: [Int] -> [Int]
-- tal que (sumaConsecutivos xs) es la suma de los pares de elementos
-- consecutivos de la lista xs. Por ejemplo,
-- sumaConsecutivos [3,1,5,2] == [4,6,7]
-- sumaConsecutivos [3] == []
-- ---------------------------------------------------------------------

sumaConsecutivos :: [Int] -> [Int]
sumaConsecutivos xs = [x+y | (x,y) <- zip xs (tail xs)]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto

-- Francisco Javier Carmona

sumaConsecutivos1 :: [Int] -> [Int]
sumaConsecutivos1 (x:xs) = [ (x+y) | (x,y) <- zip (x:xs) xs]

-- ---------------------------------------------------------------------
-- Ejercicio 11. La distancia de Hamming entre dos listas es el número
-- de posiciones en que los correspondientes elementos son
-- distintos. Por ejemplo, la distancia de Hamming entre "roma" y "loba"
-- es 2 (porque hay 2 posiciones en las que los elementos
-- correspondientes son distintos: la 1ª y la 3ª).
--
-- Definir la función distancia tal que (distancia xs ys) es la
-- distancia de Hamming entre xs e ys. Por ejemplo,
-- distancia "romano" "comino" == 2
-- distancia "romano" "camino" == 3
-- distancia "roma" "comino" == 2
-- distancia "roma" "camino" == 3
-- distancia "romano" "ron" == 1
-- distancia "romano" "cama" == 2
-- distancia "romano" "rama" == 1
-- ---------------------------------------------------------------------

distancia :: Eq a => [a] -> [a] -> Int
distancia xs ys = length (distanciaAux xs ys)

-- Definimos la función auxiliar:

distanciaAux :: Eq a => [a] -> [a] -> [Int]
distanciaAux xs [] = []
distanciaAux [] ys = []
distanciaAux (x:xs) (y:ys) | x == y = distanciaAux xs ys
| otherwise = [1]++(distanciaAux xs ys)

-- Pablo José Gerlach Mena

-- María Dolores Mateo Ceballos
-- Francisco Javier Carmona
-- Aunque es parecido al anterior, sin usar función auxiliar:

distancia :: Eq a => [a] -> [a] -> Int
distancia [] _ = 0
distancia _ [] = 0
distancia (x:xs) (y:ys) | x==y = distancia xs ys
| otherwise = 1 + distancia xs ys

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

distancia' :: Eq a => [a] -> [a] -> Int
distancia' xs ys = sum [ 1 | (a,b)<-zip xs ys, a/=b]
-- Jaime Alberto
-- ---------------------------------------------------------------------
-- Ejercicio 12. Definir la función
-- factoriales :: [Integer]
-- tal que factoriales es la lista de los factoriales. Por ejemplo,
-- take 10 factoriales == [1,1,2,6,24,120,720,5040,40320,362880]
-- ---------------------------------------------------------------------

-- Por comprensión:

factoriales1 :: [Integer]
factoriales1 = [1]++[product [1..n] | n <-[1..]]

-- Pablo José Gerlach Mena
-- Francisco Javier Carmona

-- Rocio Rodriguez
factoriales1 = [fact x|x<-[0..]]
fact 0 = 1
fact x = x*fact (x-1)
-- Jaime Alberto
-- Usando zipWith:

factoriales2 :: [Integer]
factoriales2 = [1]++(zipWith f [1..] [2..])
where f n y = product ([1..n]++[y])

-- Emilio Martinez

-- Por recursiÃ³n:

factoriales3 :: [Integer]
factoriales3 = 1:(aux 1 [1..])
where aux n (x:xs)= (n*x):(aux (n*x) xs)

-- Emilio Martinez

-- Usando scanl1:

factoriales4 :: [Integer]
factoriales4 = scanl (*) 1 [1..]

-- Emilio Martinez

-- Usando iterate:
-- Fran Franco
factoriales5 :: [Integer]
factoriales5 = map snd (iterate (\(x,y)->(x+1,x*y)) (1,1))

-- Comparación de los tiempos de evaluación:

-- *Main> take 10 factoriales1
-- [1,1,2,6,24,120,720,5040,40320,362880]

-- (0.02 secs, 0 bytes)

-- *Main> take 10 factoriales2
-- [1,2,6,24,120,720,5040,40320,362880,3628800]
-- (0.00 secs, 0 bytes)

-- *Main> take 10 factoriales3
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 528020 bytes)

-- *Main> take 10 factoriales4
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 0 bytes)

-- Pablo José Gerlach Mena

-- ---------------------------------------------------------------------
-- Ejercicio 13.0. En los siguientes ejercicios se demostrarán
-- propiedades de los árboles binarios definidos como sigue
-- data Arbol a = Hoja
-- | Nodo a (Arbol a) (Arbol a)
-- deriving (Show, Eq)
-- Como ejemplos se usarán los árboles
-- ---------------------------------------------------------------------

data Arbol a = Hoja
| Nodo a (Arbol a) (Arbol a)
deriving (Show, Eq)

arbol_1 = Nodo 9
(Nodo 3
(Nodo 2 Hoja Hoja)
(Nodo 4 Hoja Hoja))
(Nodo 7 Hoja Hoja)

-- ---------------------------------------------------------------------
-- Ejercicio 13.1. Definir la función
-- espejo :: Arbol a -> Arbol a
-- tal que (espejo x) es la imagen especular del árbol x. Por ejemplo,
-- *Main> espejo arbol_1
-- Nodo 9
-- (Nodo 7 Hoja Hoja)
-- (Nodo 3
-- (Nodo 4 Hoja Hoja)
-- (Nodo 2 Hoja Hoja))
-- ---------------------------------------------------------------------

espejo :: Arbol a -> Arbol a
espejo Hoja = Hoja
espejo (Nodo a i d)= Nodo a (espejo d) (espejo i)

-- Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.2. Comprobar con QuickCheck que para todo Ã¡rbol x,
-- espejo (espejo x) = x
-- ---------------------------------------------------------------------

prop_espejo :: Arbol Int -> Bool
prop_espejo n = (espejo . espejo) n == n

-- quickCheck prop_espejo
-- +++ OK passed 100 tests.

-- Emilio Martinez
-- Jaime Alberto
-- Rocio Rodriguez
prop_espejo x = espejo (espejo x)==x
quickCheck prop_espejo
+++ OK, passed 100 tests.
-- ---------------------------------------------------------------------
-- Ejercicio 13.3. Demostrar por inducciÃ³n que para todo Ã¡rbol x,
-- espejo (espejo x) = x
-- ---------------------------------------------------------------------
{-
DemostraciÃ³n por inducciÃ³n en x

[Caso base: Hoja]

espejo (espejo Hoja) = espejo (Hoja) por definicion de espejo Hoja
espejo (Hoja) = Hoja por definicion de espejo Hoja

Luego espejo (espejo Hoja)= Hoja
qed

[Suponemos que espejo (espejo x) = x , para todo x arbol]

[Sea N a i d con i, d arboles]

espejo (espejo (N a i d))= espejo (N a (espejo d) (espejo i)) por def
espejo (N a (espejo d)(espejo i)) = N a (espejo (espejo i))
(espejo(espejo
d)) por def

como i, d son arboles por hipótesis de induccion

= N a (espejo (espejo i)) (espejo (espejo d))
= N a i d

Luego espejo (espejo (N a i d)) = N a i d.
qed

Emilio Martinez
-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.4. Definir la funciÃ³n
-- preorden :: Arbol a -> [a]
-- tal que (preorden x) es la lista correspondiente al recorrido
-- preorden del Ã¡rbol x; es decir, primero visita la raÃz del Ã¡rbol, a
-- continuaciÃ³n recorre el subÃ¡rbol izquierdo y, finalmente, recorre el
-- subÃ¡rbol derecho. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> preorden arbol_1
-- [9,3,2,4,7]
-- ---------------------------------------------------------------------

preorden :: Arbol a -> [a]
preorden Hoja = []
preorden (Nodo a i d)= [a]++(preorden i)++(preorden d)

--Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.5. Definir la funciÃ³n
-- postorden :: Arbol a -> [a]
-- tal que (postorden x) es la lista correspondiente al recorrido
-- postorden del Ã¡rbol x; es decir, primero recorre el subÃ¡rbol
-- izquierdo, a continuaciÃ³n el subÃ¡rbol derecho y, finalmente, la raÃz
-- del Ã¡rbol. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> postorden arbol_1
-- [2,4,3,7,9]
-- ---------------------------------------------------------------------

postorden :: Arbol a -> [a]
postorden Hoja = []
postorden (Nodo a i d)= postorden i ++ [a]++ postorden d

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

postorden' :: Arbol a -> [a]
postorden' Hoja = []
postorden' (Nodo a i d) = postorden' i ++ postorden' d ++ [a]
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.6. Comprobar con QuickCheck que para todo Ã¡rbol x,
-- postorden (espejo x) = reverse (postorden x)
-- ---------------------------------------------------------------------

-- La propiedad es
prop_recorrido :: Arbol Int -> Bool
prop_recorrido x = (postorden . espejo) x == (reverse . postorden) x

-- La comprobaciÃ³n es
--quickCheck prop_recorrido
-- +++ OK, passed 100 tests.

--Emilio Martinez Rivero
-- Jaime Alberto
-- ---------------------------------------------------------------------
-- Ejercicio 13.7. Demstrar por inducción que para todo árbol x,
-- postorden (espejo x) = reverse (preorden x)
-- ---------------------------------------------------------------------

{-
Demostración por inducción en x.

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.8. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
-- reverse (preorden (espejo x)) = postorden x
-- ---------------------------------------------------------------------

-- La propiedad es
prop_reverse_preorden_espejo :: Arbol Int -> Bool
prop_reverse_preorden_espejo x =
reverse (preorden (espejo x)) == postorden x

-- La comprobación es
-- *Main> quickCheck prop_reverse_preorden_espejo
-- OK, passed 100 tests.

-- ---------------------------------------------------------------------
-- Ejercicio 13.9. Demostrar que para todo árbol binario x, se tiene que
-- reverse (preorden (espejo x)) = preorden x
-- ---------------------------------------------------------------------

{-
Demostración:
reverse (preorden (espejo x))
= postorden (espejo (espejo x)) [por ejercicio 13.7]
= postorden x [por ejercicio 13.3]
-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.10. Definir la función
-- nNodos :: Arbol a -> Int
-- tal que (nNodos x) es el número de nodos del árbol x. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> nNodos arbol_1
-- 5
-- ---------------------------------------------------------------------

nNodos :: Arbol a -> Int
nNodos Hoja = 0
nNodos (Nodo _ i d)= 1+(nNodos i)+(nNodos d)

--Emilio Martinez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.11. Comprobar con QuickCheck que el nÃºmero de nodos de la
-- imagen especular de un Ã¡rbol es el mismo que el nÃºmero de nodos del
-- Ã¡rbol.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodos_espejo :: Arbol Int -> Bool
prop_nNodos_espejo x = nNodos x == (nNodos . espejo) x

-- La comprobaciÃ³n es

-- quickCheck prop_nNodos_espejo
-- +++ OK, passed 100 tests.

--Emilio Martinez

-- ---------------------------------------------------------------------
-- Ejercicio 13.12. Demostrar por inducción que el número de nodos de la
-- imagen especular de un árbol es el mismo que el número de nodos del
-- árbol.
-- ---------------------------------------------------------------------

{-
Demostración:

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.13. Comprobar con QuickCheck que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_length_preorden :: Arbol Int -> Bool
prop_length_preorden x = length (preorden x)== nNodos x

-- La comprobación es

-- quickCheck prop_length_preorden
-- +++ OK, passed 100 tests.

-- Adrian Guerra
-- ---------------------------------------------------------------------
-- Ejercicio 13.14. Demostrar por inducción que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

{-
Demostración:

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.15. Definir la función
-- profundidad :: Arbol a -> Int
-- tal que (profundidad x) es la profundidad del árbol x. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> profundidad arbol_1
-- 3
-- ---------------------------------------------------------------------

profundidad :: Arbol a -> Int
profundidad Hoja = 0
profundidad (Nodo _ i d) = 1+ max(profundidad i) (profundidad d)

--Emilio Martinez
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.16. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
-- nNodos x <= 2^(profundidad x) - 1
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodosProfundidad :: Arbol Int -> Bool
prop_nNodosProfundidad x = nNodos x <= 2^(profundidad x) - 1

-- La comprobación es
-- quickCheck prop_nNodosProfundidad
-- +++ OK, passed 100 tests.

-- Adrian Guerra
-- ---------------------------------------------------------------------
-- Nota. Para comprobar propiedades de árboles con QuickCheck se
-- utilizará el siguiente generador.
-- ---------------------------------------------------------------------

instance Arbitrary a => Arbitrary (Arbol a) where
arbitrary = sized arbol
where
arbol 0 = return Hoja
arbol n | n>0 = oneof [return Hoja,
liftM3 Nodo arbitrary subarbol subarbol]
where subarbol = arbol (div n 2)

</source>

Relación 1

2015-02-15T16:48:48Z

Adrguede:

<source lang = "haskell">
-- LMF 2014-15: Rel_1.hs (9 de Febrero de 2015)
-- Introducción a la programación con Haskell.
-- Departamento de Ciencias de la Computación e I.A.
-- Universidad de Sevilla
-- =====================================================================

-- ---------------------------------------------------------------------
-- Introducción --
-- ---------------------------------------------------------------------

-- En esta relación de ejercicios hacemos una introducción a Haskell, en
-- la que se recuerdan:
-- * las definiciones elementales de funciones,
-- * las definiciones de funciones por comprensión,
-- * las definiciones de funciones por recursión y
-- * los tipos de datos.

-- ---------------------------------------------------------------------
-- Importación de librerías auxiliares
-- ---------------------------------------------------------------------

import Test.QuickCheck
import Data.Char
import Control.Monad

-- ---------------------------------------------------------------------
-- Ejercicio 1. Definir la función media3 tal que (media3 x y z) es
-- la media aritmética de los números x, y y z. Por ejemplo,
-- media3 1 3 8 == 4.0
-- media3 (-1) 0 7 == 2.0
-- media3 (-3) 0 3 == 0.0
-- ---------------------------------------------------------------------

media3 x y z = (x+y+z)/3

-- Miriam R.
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 2. Definir la función ultimaCifra tal que (ultimaCifra x)
-- es la última cifra del nímero x. Por ejemplo,
-- ultimaCifra 325 == 5
-- ---------------------------------------------------------------------

ultimaCifra x = rem x 10

-- Miriam R.
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 3. Definir la función rota tal que (rota n xs) es la lista
-- obtenida poniendo los n primeros elementos de xs al final de la
-- lista. Por ejemplo,
-- rota 1 [3,2,5,7] == [2,5,7,3]
-- rota 2 [3,2,5,7] == [5,7,3,2]
-- rota 3 [3,2,5,7] == [7,3,2,5]
-- ---------------------------------------------------------------------

rota n xs= (drop n xs) ++ (take n xs)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- Ejercicio 4.1. La disyunción excluyente xor de dos fórmulas se
-- verifica si una es verdadera y la otra es falsa.
--
-- Definir la función xor_1 que calcule la disyunción excluyente a
-- partir de la tabla de verdad. Usar 4 ecuaciones, una por cada línea
-- de la tabla.
-- ---------------------------------------------------------------------

xor_1 :: Bool -> Bool -> Bool
xor_1 True True = False
xor_1 True False = True
xor_1 False True = True
xor_1 False False = False

-- Pablo José Gerlach Mena
-- Rocio Rodriguez

xor_1 :: Bool -> Bool -> Bool
xor_1 x y |x== True && y== True = False
|x== True && y== False = True
|x== False && y== True = True
|x== False && y== False = False
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 4.2. Definir la función xor_2 que calcule la disyunción
-- excluyente a partir de la tabla de verdad y patrones. Usar 2
-- ecuaciones, una por cada valor del primer argumento.
-- ---------------------------------------------------------------------

xor_2 :: Bool -> Bool -> Bool
xor_2 True x = if x then False else True
xor_2 False x = if x then True else False

-- Pablo José Gerlach Mena

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

xor_2' True x = not x
xor_2' False x = x

-- Jaime Alberto
xor_2'' :: Bool -> Bool -> Bool
xor_2'' x y | x== True && y== True || x==False && y== False = False
| x== True && y== False || x== False && y== True = True

-- Elisa Mazuelos Jiménez:

xor_2 :: Bool -> Bool -> Bool
xor_2 True x | x == True = False
| otherwise = True
xor_2 False x | x == False = False
| otherwise = True

-- Esta última no es correcta (10/02/2015).
-- Corregida, gracias (10/02/2015).

-- ---------------------------------------------------------------------
-- Ejercicio 4.3. Definir la función xor_3 que calcule la disyunción
-- excluyente a partir de la disyunción (||), conjunción (&&) y negación
-- (not). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_3 :: Bool -> Bool -> Bool
xor_3 x y = (x && (not y)) || ((not x) && y)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-----------------------------------------------------
-- Ejercicio 4.4. Definir la función xor_4 que calcule la disyunción
-- excluyente a partir de desigualdad (/=). Usar 1 ecuación.
-- ---------------------------------------------------------------------

xor_4 :: Bool -> Bool -> Bool
xor_4 x y = x /= y

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona

-- ---------------------------------------------------------------------
-- Ejercicio 5. Definir, por comprensión, la función
-- sumaDeCuadrados :: Integer -> Integer
-- tal que (sumaDeCuadrados n) es la suma de los cuadrados de los
-- primeros n números; es decir, 1^2 + 2^2 + ... + 100^2. Por ejemplo,
-- sumaDeCuadrados 3 == 14
-- sumaDeCuadrados 100 == 338350
-- ---------------------------------------------------------------------

sumaDeCuadrados n = sum [x^2 | x <- [1..n]]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 6. Una terna (x,y,z) de enteros positivos es pitagórica si
-- x^2 + y^2 = z^2. Usando una lista por comprensión, definir la función
-- pitagoricas :: Int -> [(Int, Int, Int)]
-- tal que (pitagoricas n) es la lista de todas las ternas pitagóricas
-- cuyas componentes están entre 1 y n. Por ejemplo,
-- *Main> pitagoricas 10
-- [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]
-- ---------------------------------------------------------------------

pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [(x,y,z) | x <- [1..n], y <- [1..n], z <- [1..n], x^2+y^2 == z^2]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- Luis Curquejo. Solución acotando ligeramente los elementos x e y.

pitagoricas :: Int -> [(Int, Int, Int)]
pitagoricas n = [ (x,y,z) | z <- [1..n], x <- [1..z], y <- [1..z] , x^2 + y^2 == z^2]

-- ---------------------------------------------------------------------
-- Ejercicio 7. Un entero positivo es perfecto si es igual a la suma de
-- sus factores, excluyendo el propio número. Usando una lista por
-- comprensión y la función factores (del tema), definir la función
-- perfectos :: Int -> [Int]
-- tal que (perfectos n) es la lista de todos los números perfectos
-- menores que n. Por ejemplo:
-- *Main> perfectos 500
-- [6,28,496]
-- ---------------------------------------------------------------------

perfectos :: Int -> [Int]
perfectos n = [x | x <- [1..n], esPerfecto x]

-- Definimos las funciones auxiliares:

factores :: Int -> [Int]
factores n = [x | x <- [1..n], n `mod` x == 0]

esPerfecto :: Int -> Bool
esPerfecto n = sum (factores n) == 2*n

-- También podríamos definirla como:

perfectos2 :: Int -> [Int]
perfectos2 n = filter (esPerfecto) [1..n]

-- Podemos comprobar que ambas definiciones son equivalentes:

prop_perfectos n = perfectos n == perfectos2 n

-- Si queremos podemos comparar ambos algoritmos:

-- *Main> perfectos 500
-- [6,28,496]
-- (1.44 secs, 15935120 bytes)

-- *Main> perfectos2 500
-- [6,28,496]
-- (0.22 secs, 14803544 bytes)

-- Es decir, el segundo es más eficiente.

-- Pablo José Gerlach Mena

-- Rocio Rodriguez
perfectos x = [y|y<-[1..x-1], serPerfecto y]
serPerfecto x = x==sum (factores' x)
factores x = [y|y<-[1..x], rem x y == 0]
factores' x = init (factores x)

-- Luis Curquejo

perfectos :: Int -> [Int]
perfectos n = [ x | x <- [1..n], x == sum (factoresred x)]
where factoresred x = [ y | y <- [1..x-1], rem x y == 0]

-- Francisco Javier Carmona

perfectos1 :: Int -> [Int]
perfectos1 n = [ x | x <- [1..n],
x == sum (tail(reverse (factores x)))]

factores1 n = [x | x <- [1..n], rem n x == 0]

-- ---------------------------------------------------------------------
-- Ejercicio 8.1. Definir, por comprensión, la función
-- cuadradosC :: [Integer] -> [Integer]
-- tal que (cuadradosC xs) es la lista de los cuadrados de xs. Por
-- ejemplo,
-- cuadradosC [1,2,3] == [1,4,9]
-- ---------------------------------------------------------------------

cuadradosC :: [Integer] -> [Integer]
cuadradosC xs = [x^2 | x <- xs]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 8.2. Definir, por recursión, la función
-- cuadradosR :: [Integer] -> [Integer]
-- tal que (cuadradosR xs) es la lista de los cuadrados de xs. Por
-- ejemplo,
-- cuadradosR [1,2,3] == [1,4,9]
-- ---------------------------------------------------------------------

cuadradosR :: [Integer] -> [Integer]
cuadradosR [] = []
cuadradosR (x:xs) = (x^2):(cuadradosR xs)

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.1. Definir, por comprensión, la función
-- imparesC :: [Integer] -> [Integer]
-- tal que (imparesC xs) es la lista de los números impares de xs. Por
-- ejemplo,
-- imparesC [1,2,3] == [1,3]
-- ---------------------------------------------------------------------

imparesC :: [Integer] -> [Integer]
imparesC xs = [x | x <- xs, odd x]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 9.2. Definir, por recursión, la función
-- imparesR :: [Integer] -> [Integer]
-- tal que (imparesR xs) es la lista de los números impares de xs. Por
-- ejemplo,
-- imparesR [1,2,3] == [1,3]
-- ---------------------------------------------------------------------

imparesR :: [Integer] -> [Integer]
imparesR [] = []
imparesR (x:xs) | odd x = x:(imparesR xs)
| otherwise = imparesR xs

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 10. Definir, por comprensión, la función
-- sumaConsecutivos :: [Int] -> [Int]
-- tal que (sumaConsecutivos xs) es la suma de los pares de elementos
-- consecutivos de la lista xs. Por ejemplo,
-- sumaConsecutivos [3,1,5,2] == [4,6,7]
-- sumaConsecutivos [3] == []
-- ---------------------------------------------------------------------

sumaConsecutivos :: [Int] -> [Int]
sumaConsecutivos xs = [x+y | (x,y) <- zip xs (tail xs)]

-- Pablo José Gerlach Mena
-- Rocio Rodriguez
-- Jaime Alberto

-- Francisco Javier Carmona

sumaConsecutivos1 :: [Int] -> [Int]
sumaConsecutivos1 (x:xs) = [ (x+y) | (x,y) <- zip (x:xs) xs]

-- ---------------------------------------------------------------------
-- Ejercicio 11. La distancia de Hamming entre dos listas es el número
-- de posiciones en que los correspondientes elementos son
-- distintos. Por ejemplo, la distancia de Hamming entre "roma" y "loba"
-- es 2 (porque hay 2 posiciones en las que los elementos
-- correspondientes son distintos: la 1ª y la 3ª).
--
-- Definir la función distancia tal que (distancia xs ys) es la
-- distancia de Hamming entre xs e ys. Por ejemplo,
-- distancia "romano" "comino" == 2
-- distancia "romano" "camino" == 3
-- distancia "roma" "comino" == 2
-- distancia "roma" "camino" == 3
-- distancia "romano" "ron" == 1
-- distancia "romano" "cama" == 2
-- distancia "romano" "rama" == 1
-- ---------------------------------------------------------------------

distancia :: Eq a => [a] -> [a] -> Int
distancia xs ys = length (distanciaAux xs ys)

-- Definimos la función auxiliar:

distanciaAux :: Eq a => [a] -> [a] -> [Int]
distanciaAux xs [] = []
distanciaAux [] ys = []
distanciaAux (x:xs) (y:ys) | x == y = distanciaAux xs ys
| otherwise = [1]++(distanciaAux xs ys)

-- Pablo José Gerlach Mena

-- María Dolores Mateo Ceballos
-- Francisco Javier Carmona
-- Aunque es parecido al anterior, sin usar función auxiliar:

distancia :: Eq a => [a] -> [a] -> Int
distancia [] _ = 0
distancia _ [] = 0
distancia (x:xs) (y:ys) | x==y = distancia xs ys
| otherwise = 1 + distancia xs ys

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

distancia' :: Eq a => [a] -> [a] -> Int
distancia' xs ys = sum [ 1 | (a,b)<-zip xs ys, a/=b]
-- Jaime Alberto
-- ---------------------------------------------------------------------
-- Ejercicio 12. Definir la función
-- factoriales :: [Integer]
-- tal que factoriales es la lista de los factoriales. Por ejemplo,
-- take 10 factoriales == [1,1,2,6,24,120,720,5040,40320,362880]
-- ---------------------------------------------------------------------

-- Por comprensión:

factoriales1 :: [Integer]
factoriales1 = [1]++[product [1..n] | n <-[1..]]

-- Pablo José Gerlach Mena
-- Francisco Javier Carmona

-- Rocio Rodriguez
factoriales1 = [fact x|x<-[0..]]
fact 0 = 1
fact x = x*fact (x-1)
-- Jaime Alberto
-- Usando zipWith:

factoriales2 :: [Integer]
factoriales2 = [1]++(zipWith f [1..] [2..])
where f n y = product ([1..n]++[y])

-- Emilio Martinez

-- Por recursiÃ³n:

factoriales3 :: [Integer]
factoriales3 = 1:(aux 1 [1..])
where aux n (x:xs)= (n*x):(aux (n*x) xs)

-- Emilio Martinez

-- Usando scanl1:

factoriales4 :: [Integer]
factoriales4 = scanl (*) 1 [1..]

-- Emilio Martinez

-- Usando iterate:
-- Fran Franco
factoriales5 :: [Integer]
factoriales5 = map snd (iterate (\(x,y)->(x+1,x*y)) (1,1))

-- Comparación de los tiempos de evaluación:

-- *Main> take 10 factoriales1
-- [1,1,2,6,24,120,720,5040,40320,362880]

-- (0.02 secs, 0 bytes)

-- *Main> take 10 factoriales2
-- [1,2,6,24,120,720,5040,40320,362880,3628800]
-- (0.00 secs, 0 bytes)

-- *Main> take 10 factoriales3
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 528020 bytes)

-- *Main> take 10 factoriales4
-- [1,1,2,6,24,120,720,5040,40320,362880]
-- (0.00 secs, 0 bytes)

-- Pablo José Gerlach Mena

-- ---------------------------------------------------------------------
-- Ejercicio 13.0. En los siguientes ejercicios se demostrarán
-- propiedades de los árboles binarios definidos como sigue
-- data Arbol a = Hoja
-- | Nodo a (Arbol a) (Arbol a)
-- deriving (Show, Eq)
-- Como ejemplos se usarán los árboles
-- ---------------------------------------------------------------------

data Arbol a = Hoja
| Nodo a (Arbol a) (Arbol a)
deriving (Show, Eq)

arbol_1 = Nodo 9
(Nodo 3
(Nodo 2 Hoja Hoja)
(Nodo 4 Hoja Hoja))
(Nodo 7 Hoja Hoja)

-- ---------------------------------------------------------------------
-- Ejercicio 13.1. Definir la función
-- espejo :: Arbol a -> Arbol a
-- tal que (espejo x) es la imagen especular del árbol x. Por ejemplo,
-- *Main> espejo arbol_1
-- Nodo 9
-- (Nodo 7 Hoja Hoja)
-- (Nodo 3
-- (Nodo 4 Hoja Hoja)
-- (Nodo 2 Hoja Hoja))
-- ---------------------------------------------------------------------

espejo :: Arbol a -> Arbol a
espejo Hoja = Hoja
espejo (Nodo a i d)= Nodo a (espejo d) (espejo i)

-- Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.2. Comprobar con QuickCheck que para todo Ã¡rbol x,
-- espejo (espejo x) = x
-- ---------------------------------------------------------------------

prop_espejo :: Arbol Int -> Bool
prop_espejo n = (espejo . espejo) n == n

-- quickCheck prop_espejo
-- +++ OK passed 100 tests.

-- Emilio Martinez
-- Jaime Alberto
-- Rocio Rodriguez
prop_espejo x = espejo (espejo x)==x
quickCheck prop_espejo
+++ OK, passed 100 tests.
-- ---------------------------------------------------------------------
-- Ejercicio 13.3. Demostrar por inducciÃ³n que para todo Ã¡rbol x,
-- espejo (espejo x) = x
-- ---------------------------------------------------------------------
{-
DemostraciÃ³n por inducciÃ³n en x

[Caso base: Hoja]

espejo (espejo Hoja) = espejo (Hoja) por definicion de espejo Hoja
espejo (Hoja) = Hoja por definicion de espejo Hoja

Luego espejo (espejo Hoja)= Hoja
qed

[Suponemos que espejo (espejo x) = x , para todo x arbol]

[Sea N a i d con i, d arboles]

espejo (espejo (N a i d))= espejo (N a (espejo d) (espejo i)) por def
espejo (N a (espejo d)(espejo i)) = N a (espejo (espejo i))
(espejo(espejo
d)) por def

como i, d son arboles por hipótesis de induccion

= N a (espejo (espejo i)) (espejo (espejo d))
= N a i d

Luego espejo (espejo (N a i d)) = N a i d.
qed

Emilio Martinez
-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.4. Definir la funciÃ³n
-- preorden :: Arbol a -> [a]
-- tal que (preorden x) es la lista correspondiente al recorrido
-- preorden del Ã¡rbol x; es decir, primero visita la raÃz del Ã¡rbol, a
-- continuaciÃ³n recorre el subÃ¡rbol izquierdo y, finalmente, recorre el
-- subÃ¡rbol derecho. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> preorden arbol_1
-- [9,3,2,4,7]
-- ---------------------------------------------------------------------

preorden :: Arbol a -> [a]
preorden Hoja = []
preorden (Nodo a i d)= [a]++(preorden i)++(preorden d)

--Emilio Martinez
-- Rocio Rodriguez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.5. Definir la funciÃ³n
-- postorden :: Arbol a -> [a]
-- tal que (postorden x) es la lista correspondiente al recorrido
-- postorden del Ã¡rbol x; es decir, primero recorre el subÃ¡rbol
-- izquierdo, a continuaciÃ³n el subÃ¡rbol derecho y, finalmente, la raÃz
-- del Ã¡rbol. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> postorden arbol_1
-- [2,4,3,7,9]
-- ---------------------------------------------------------------------

postorden :: Arbol a -> [a]
postorden Hoja = []
postorden (Nodo a i d)= postorden i ++ [a]++ postorden d

-- Realizado por Nikola Drousie:
-- Rocio Rodriguez

postorden' :: Arbol a -> [a]
postorden' Hoja = []
postorden' (Nodo a i d) = postorden' i ++ postorden' d ++ [a]
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.6. Comprobar con QuickCheck que para todo Ã¡rbol x,
-- postorden (espejo x) = reverse (postorden x)
-- ---------------------------------------------------------------------

-- La propiedad es
prop_recorrido :: Arbol Int -> Bool
prop_recorrido x = (postorden . espejo) x == (reverse . postorden) x

-- La comprobaciÃ³n es
--quickCheck prop_recorrido
-- +++ OK, passed 100 tests.

--Emilio Martinez Rivero
-- Jaime Alberto
-- ---------------------------------------------------------------------
-- Ejercicio 13.7. Demstrar por inducción que para todo árbol x,
-- postorden (espejo x) = reverse (preorden x)
-- ---------------------------------------------------------------------

{-
Demostración por inducción en x.

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.8. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
-- reverse (preorden (espejo x)) = postorden x
-- ---------------------------------------------------------------------

-- La propiedad es
prop_reverse_preorden_espejo :: Arbol Int -> Bool
prop_reverse_preorden_espejo x =
reverse (preorden (espejo x)) == postorden x

-- La comprobación es
-- *Main> quickCheck prop_reverse_preorden_espejo
-- OK, passed 100 tests.

-- ---------------------------------------------------------------------
-- Ejercicio 13.9. Demostrar que para todo árbol binario x, se tiene que
-- reverse (preorden (espejo x)) = preorden x
-- ---------------------------------------------------------------------

{-
Demostración:
reverse (preorden (espejo x))
= postorden (espejo (espejo x)) [por ejercicio 13.7]
= postorden x [por ejercicio 13.3]
-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.10. Definir la función
-- nNodos :: Arbol a -> Int
-- tal que (nNodos x) es el número de nodos del árbol x. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> nNodos arbol_1
-- 5
-- ---------------------------------------------------------------------

nNodos :: Arbol a -> Int
nNodos Hoja = 0
nNodos (Nodo _ i d)= 1+(nNodos i)+(nNodos d)

--Emilio Martinez
-- Jaime Alberto
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.11. Comprobar con QuickCheck que el nÃºmero de nodos de la
-- imagen especular de un Ã¡rbol es el mismo que el nÃºmero de nodos del
-- Ã¡rbol.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodos_espejo :: Arbol Int -> Bool
prop_nNodos_espejo x = nNodos x == (nNodos . espejo) x

-- La comprobaciÃ³n es

-- quickCheck prop_nNodos_espejo
-- +++ OK, passed 100 tests.

--Emilio Martinez

-- ---------------------------------------------------------------------
-- Ejercicio 13.12. Demostrar por inducción que el número de nodos de la
-- imagen especular de un árbol es el mismo que el número de nodos del
-- árbol.
-- ---------------------------------------------------------------------

{-
Demostración:

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.13. Comprobar con QuickCheck que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

-- La propiedad es
prop_length_preorden :: Arbol Int -> Bool
prop_length_preorden x = length (preorden x)== nNodos x

-- La comprobación es

-- quickCheck prop_length_preorden
-- +++ OK, passed 100 tests.

-- Adrian Guerra
-- ---------------------------------------------------------------------
-- Ejercicio 13.14. Demostrar por inducción que la longitud de la lista
-- obtenida recorriendo un árbol en sentido preorden es igual al número
-- de nodos del árbol.
-- ---------------------------------------------------------------------

{-
Demostración:

-}

-- ---------------------------------------------------------------------
-- Ejercicio 13.15. Definir la función
-- profundidad :: Arbol a -> Int
-- tal que (profundidad x) es la profundidad del árbol x. Por ejemplo,
-- *Main> arbol_1
-- Nodo 9 (Nodo 3 (Nodo 2 Hoja Hoja) (Nodo 4 Hoja Hoja)) (Nodo 7 Hoja Hoja)
-- *Main> profundidad arbol_1
-- 3
-- ---------------------------------------------------------------------

profundidad :: Arbol a -> Int
profundidad Hoja = 0
profundidad (Nodo _ i d) = 1+ max(profundidad i) (profundidad d)

--Emilio Martinez
-- Francisco Javier Carmona
-- ---------------------------------------------------------------------
-- Ejercicio 13.16. Comprobar con QuickCheck que para todo árbol binario
-- x, se tiene que
-- nNodos x <= 2^(profundidad x) - 1
-- ---------------------------------------------------------------------

-- La propiedad es
prop_nNodosProfundidad :: Arbol Int -> Bool
prop_nNodosProfundidad = undefined

-- La comprobación es

-- ---------------------------------------------------------------------
-- Nota. Para comprobar propiedades de árboles con QuickCheck se
-- utilizará el siguiente generador.
-- ---------------------------------------------------------------------

instance Arbitrary a => Arbitrary (Arbol a) where
arbitrary = sized arbol
where
arbol 0 = return Hoja
arbol n | n>0 = oneof [return Hoja,
liftM3 Nodo arbitrary subarbol subarbol]
where subarbol = arbol (div n 2)

</source>