Lógica matemática y fundamentos [Curso 2019-20] - Contribuciones del usuario [es]

Ejercicios

2021-07-25T15:07:15Z

Jalonso:

Ejercicios

2021-07-25T15:01:47Z

Jalonso:

Ejercicios

2021-07-25T15:00:09Z

Jalonso:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]] y [[Rel 2 |solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]] y [[Rel 3 |solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]] y [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]] y [[Rel 5 |solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]] y [[Rel 6 |solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]] y [[Rel 8 (sol) |solución]]).
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]] y [Rel 9 (sol) |solución]]).
* '''Ejercicio evaluable 1 (24-04-2020)''': ([[T1 |Enunciado]] y [[T1 sol |solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]] y [[Rel 10 (sol) |solución]]).
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]] y [[Rel 11 (sol) |solución]]).
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]] y [[Rel 12 (sol) |solución]]).
* '''Ejercicio evaluable 2 (12-05-2020)''': ([[T2 |Enunciado]] y [[T2 sol |solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]] y [[Rel 13 (sol) |solución]]).
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomatización de la Geometría.] ([[R14 |Enunciado]] y [[Rel 14 (sol) |solución]]).
* '''Ejercicio evaluable 3 (19-05-2020)''': ([[T3 |Enunciado]] y [[T3 sol |solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]] y [[Rel 15 (sol) |solución]]
* '''Ejercicio evaluable 4 (26-05-2020)''': ([[T4 |Enunciado]] y [[T4 sol |solución]]).
* '''Ejercicio evaluable 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]] y [[T5-1 sol |solución]]).
** ([[T5-2 |Enunciado (2)]] y [[T5-2 sol |solución]]).
* '''Trabajo final''': ([[TF |Enunciado]] y [[TF sol |solución]]).
* '''Examen (2-07-2020)''': ([[Examen 1C |Enunciado]] y [[Examen 1C sol |solución]]).
* '''Examen (9-09-2020)''': ([[Examen 2C |Enunciado]] y [[Examen 2C sol |solución]]).

Ejercicios

2021-07-25T14:48:32Z

Jalonso:

En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF-2019-20.pdf libro de ejercicios].

* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]], [[Relación 1 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R1_sol.pdf Una solución]).
* '''Relación 2''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R2.thy Deducción natural proposicional con Isabelle] ([[R2 |Enunciado]], [[Relación 2 |Solución colaborativa]], [[Rel 2 |Una solución]]).
* '''Relación 3''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R3.thy Deducción natural proposicional con Isabelle (II)] ([[R3 |Enunciado]], [[Relación 3 |Solución colaborativa]], [[Rel 3 |Una solución]]).
* '''Relación 4''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4.thy Sintaxis y semántica de la lógica de primer orden.] ([[R4 |Enunciado]], [[Relación 4 |Solución colaborativa]], [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R4_sol.pdf Una solución]).).
* '''Relación 5''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R5.thy Deducción natural en lógica de primer orden.] ([[R5 |Enunciado]], [[Relación 5 |Solución colaborativa]], [[Rel 5 |Una solución]]).
* '''Relación 6''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R6.thy Formalización y argumentación con Isabelle/HOL.] ([[R6 |Enunciado]], [[Relación 6 |Solución colaborativa]] , [[Rel 6 |Una solución]]).
* '''Relación 7''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R7.thy Deducción natural,formalización y argumentación en LPO con Isabelle/HOL.] ([[R7 |Enunciado]], [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R8.thy Programación funcional en Isabelle/HOL.] ([[R8 |Enunciado]], [[Relación 8 |Solución colaborativa]]).
** [[Rel 8 (rev 1) | Primera corrección]]
** [[Rel 8 (sol) | Una solución]]
* '''Relación 9''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R9.thy Programación funcional en Isabelle/HOL (II).] ([[R9 |Enunciado]], [[Relación 9 |Solución colaborativa]]).
** [[Rel 9 (rev 1) | Primera corrección]]
** [[Rel 9 (sol) | Una solución]]
* '''Ejercicio 1 (24-04-2020)''': ([[T1 |Enunciado]], [[T1 sol |Una solución]]).
* '''Relación 10''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R10.thy Razonamiento sobre programas en Isabelle/HOL.] ([[R10 |Enunciado]], [[Relación 10 |Solución colaborativa]]).
** [[Rel 10 (sol) | Una solución]]
* '''Relación 11''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R11.thy Razonamiento sobre programas en Isabelle/HOL(II).] ([[R11 |Enunciado]], [[Relación 11 |Solución colaborativa]]).
** [[Rel 11 (sol) | Una solución]]
* '''Relación 12''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R12.thy Razonamiento sobre programas en Isabelle/HOL(III).] ([[R12 |Enunciado]], [[Relación 12 |Solución colaborativa]]).
** [[Rel 12 (sol) | Una solución]]
* '''Ejercicio 2 (12-05-2020)''': ([[T2 |Enunciado]], [[T2 sol |Una solución]]).
* '''Relación 13''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R13.thy Recorridos de árboles.] ([[R13 |Enunciado]], [[Relación 13 |Solución colaborativa]]).
** [[Rel 13 (sol) | Una solución]]
* '''Relación 14''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R14.thy Una axiomatización de la Geometría.] ([[R14 |Enunciado]], [[Relación 14 |Solución colaborativa]]).
** [[Rel 14 (sol) | Una solución]]
* '''Ejercicio 3 (19-05-2020)''': ([[T3 |Enunciado]], [[T3 sol |Una solución]]).
* '''Relación 15''': [https://www.cs.us.es/~mjoseh/cursos/lmf-19/relaciones-ejercicios/R15.thy Definiciones inductivas: clausuras.] ([[R15 |Enunciado]], [[Relación 15 |Solución colaborativa]]).
** [[Rel 15 (sol) | Una solución]]
* '''Ejercicio 4 (26-05-2020)''': ([[T4 |Enunciado]], [[T4 sol |Una solución]]).
* '''Ejercicio 5 (02-06-2020)''':
** ([[T5-1 |Enunciado (1)]], [[T5-1 sol |Una solución]]).
** ([[T5-2 |Enunciado (2)]], [[T5-2 sol |Una solución]]).
* '''Trabajo final''': ([[TF |Enunciado]], [[TF sol |Una solución]]).
* '''Examen (2-07-2020)''': ([[Examen 1C |Enunciado]], [[Examen 1C sol |Una solución]]).
* '''Examen (9-09-2020)''': ([[Examen 2C |Enunciado]], [[Examen 2C sol |Una solución]]).
-->

Rel 11 (sol)

2020-05-12T10:05:02Z

Jalonso:

<source lang="isabelle">
chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)›

theory R11_sol
imports Main
begin

text ‹ ---------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
+ automática
+ en el ejercicio 1.2, la prueba detallada usando "simp only:..."
(bien de forma declarativa o aplicativa)
+ en los ejercicios 5, 6 y 7 sólo es necesario hacer la demostración
detallada usando "simp", sin llegar al detalle de usar "simp only:..."
------------------------------------------------------------------ ›

text ‹ ---------------------------------------------------------------
Ejercicio 1.1. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ ›

fun factR :: "nat ⇒ nat" where
"factR 0 = 1"
| "factR (Suc n) = Suc n * factR n"

value "factR 4" ― ‹= 24›

text ‹ ---------------------------------------------------------------
Ejercicio 1.2. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- ›

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (x* (Suc n))"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

― ‹Demostración automática:›
lemma "factI' n x = x * factR n"
by (induct n arbitrary: x)
(auto simp del: mult_Suc)

― ‹Demostración en lenguaje natural:
Por inducción en n con x arbitrario, hay que probar
∀n. (∀x. factI' n x = x * factR n)

+ Caso base: hay que probar ∀x. factI' 0 x = x * factR 0
En efecto, para cualquier x, se tiene factI' 0 x = x * factR 0,
aplicando directamenta las definiciones de ambas funciones.

+ Paso inductivo:
+ HI: ∀x. factI' n x = x * factR n
+ Hay que probar ∀x. factI' (n+1) x = x * factR (n+1)
En efecto, sea a cualquiera
factI' (n+1) a = (por def. de factI')
factI' n (a*(n+1)) = (por HI, para x = a*(n+1))
(a*(n+1))*(factR n) = (asociativa de *)
a*((n+1)*(factR n)) = (def. de factR)
a*(factR (n+1))
›

― ‹Demostración estructurada:›
lemma "factI' n x = x * factR n"
proof (induct n arbitrary: x)
show "⋀x. factI' 0 x = x * factR 0" by simp
next
fix n
assume HI: "⋀x. factI' n x = x * factR n"
show "⋀x. factI' (Suc n) x = x * factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
also have "... = (x * Suc n) * factR n" using HI by simp
also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc)
also have "... = x * factR (Suc n)" by simp
finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
qed
qed

― ‹Demostración detallada declarativa:›
lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
fix x
have "factI' 0 x = x"
by (simp only: factI'.simps(1))
also have "... = x * 1"
by (simp only: mult_1_right)
also have "... = x * factR 0"
by (simp only: factR.simps(1))
finally show "factI' 0 x= x* factR 0"
by this
next
fix n
assume HI: " ⋀x. factI' n x = x *factR n"
show "⋀x. factI' (Suc n) x = x*factR (Suc n)"
proof -
fix x
have "factI' (Suc n) x = factI' n (x*Suc n)"
by (simp only: factI'.simps(2))
also have "... = (x*Suc n)*factR n"
by (simp only: HI)
also have "... = x*(Suc n*factR n)"
by (simp only: mult.assoc)
also have "... = x*factR (Suc n)"
by (simp only: factR.simps(2))
finally show "factI' (Suc n) x= x*factR (Suc n)"
by this
qed
qed

― ‹Demostración detallada aplicativa:›
lemma "factI' n x = x * factR n"
apply (induct n arbitrary: x)
apply (simp only: factI'.simps(1))
apply (simp only: factR.simps(1))
apply (simp only: factI'.simps(2))
apply (simp only: factR.simps(2))
done

text ‹ ---------------------------------------------------------------
Ejercicio 1.3. Demostrar que
factI n = factR n
------------------------------------------------------------------- ›

― ‹Demostración automática:›
corollary "factI n = factR n"
by (simp add: fact)

― ‹Demostración en lenguaje natural:

factI n = (def. de factI)
factI' n 1 = (lema fact)
1 * (factR n) = (1 es elemento neutro de *)
factR n
›

― ‹Demostración estructurada:›
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1"
by simp
also have "… = 1 * factR n"
by (simp add: fact)
also have "… = factR n"
by simp
finally show "factI n = factR n"
by this
qed

― ‹Demostración detallada declarativa:›
corollary "factI n = factR n"
proof -
have "factI n = factI' n 1"
by (simp only: factI.simps)
also have "… = 1 * factR n"
by (simp only: fact)
also have "… = factR n"
by (simp only: nat_mult_1)
finally show "factI n = factR n"
by this
qed

text ‹
---------------------------------------------------------------------
Ejercicio 2. Definir la función
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------
›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"

text ‹
---------------------------------------------------------------------
Ejercicio 3. Definir la función
sinDuplicados :: 'a list ⇒ bool
tal que (sinDuplicados xs) se verifica si la lista xs no contiene
duplicados. Por ejemplo,
sinDuplicados [1::nat,4,2] = True
sinDuplicados [1::nat,4,2,4] = False
---------------------------------------------------------------------
›

fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = True"
| "sinDuplicados (a#xs) = ((¬ estaEn a xs) ∧ sinDuplicados xs)"

text ‹
---------------------------------------------------------------------
Ejercicio 4. Definir la función
borraDuplicados :: 'a list ⇒ bool
tal que (borraDuplicados xs) es la lista obtenida eliminando los
elementos duplicados de la lista xs. Por ejemplo,
borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

Nota: La función borraDuplicados es equivalente a la predefinida
remdups.
---------------------------------------------------------------------
›

fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (a#xs) = (if estaEn a xs
then borraDuplicados xs
else (a#borraDuplicados xs))"

text ‹
---------------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) simp_all

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base:
length (borraDuplicados []) ≤ length [], directamente por las definciones.

+ Paso inductivo:
+ HI: length (borraDuplicados xs) ≤ length xs
+ Hay que probar: length (borraDuplicados (a#xs)) ≤ length (a#xs)
La demostración se realiza por casos:

+ Caso 1: estaEn a xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
length (borraDuplicados xs) ≤ (por HI)
length xs ≤ (aritmética)
1 + length xs = (por def. de length)
length (a#xs)

+ Caso 2: ¬ (estaEn a xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = a#(borraDuplicados xs). Por tanto,
length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
length (a#(borraDuplicados xs)) = (def. de length)
1 + length (borraDuplicados xs) ≤ (por HI)
1 + length xs = (por def. de length)
length (a#xs)

›

― ‹Demostración estructurada:›

lemma
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
proof (cases)
assume "estaEn a xs"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
using HI by simp
next
assume "(¬ estaEn a xs)"
thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
using HI by simp
qed
qed

― ‹Auxiliares para la demostración detallada:›
lemma estaEnBD1:
assumes "estaEn b xs"
shows "borraDuplicados (b#xs) = borraDuplicados xs"
using assms by (simp only:borraDuplicados.simps(2) if_P)

lemma estaEnBD2:
assumes "¬ (estaEn b xs)"
shows "borraDuplicados (b#xs) = b#(borraDuplicados xs)"
proof-
have "borraDuplicados (b#xs) = (if estaEn b xs
then borraDuplicados xs
else (b#borraDuplicados xs))"
by (simp only: borraDuplicados.simps(2))
also have "…= (b#borraDuplicados xs)" using assms by (rule if_not_P)
finally show "borraDuplicados (b # xs) = b # borraDuplicados xs" by this
qed

― ‹Demostración detallada declarativa:›
lemma length_borraDuplicados_d:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []"
by (simp only: borraDuplicados.simps(1) list.size)
next
fix a xs
assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
show "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
proof (cases)
assume "estaEn a xs"
then have "borraDuplicados (a#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "length (borraDuplicados (a#xs)) = length (borraDuplicados xs)"
by (rule arg_cong)
also have "... ≤ length xs" using HI by this
also have "... ≤ length (a#xs)" by (simp only: list.size)
finally show ?thesis by this
next
assume "(¬ estaEn a xs)"
then have "borraDuplicados (a#xs) = a#(borraDuplicados xs)"
by (rule estaEnBD2)
then have "length (borraDuplicados (a#xs)) = length (a#(borraDuplicados xs))"
by (rule arg_cong)
also have "... = 1 + length (borraDuplicados xs)" by (simp only: list.size)
also have "... ≤ 1 + length xs" using HI by (simp only: add_left_mono)
also have "... = length (a#xs)" by (simp only: list.size)
finally show ?thesis by this
qed
qed

― ‹Demostración aplicativa detallada:›
lemma length_borraDuplicados_a:
"length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply (simp only: borraDuplicados.simps(1) list.size)
apply (simp only: borraDuplicados.simps(2))
apply(split if_split)
apply (rule conjI)
apply (rule impI)
apply (drule estaEnBD1)
apply (simp only:list.size)
apply (rule impI)
apply (drule estaEnBD2)
apply (simp only:list.size)
done

text ‹
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base:
estaEn a (borraDuplicados []) = estaEn a [], directamente por las definiciones.

+ Paso inductivo:
+ HI: estaEn a (borraDuplicados xs) = estaEn a xs
+ Hay que probar: estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs).
La demostración se realiza por casos.

+ Caso 1: estaEn b xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (b#xs) = borraDuplicados xs. Por tanto,
estaEn a (borraDuplicados (b#xs)) = (def. de borraDuplicados)
estaEn a (borraDuplicados xs) = (por HI)
estaEn a xs = (por (estaEn b xs))
estaEn a (b#xs)

+ Caso 2: ¬ (estaEn b xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (b#xs) = b # (borraDuplicados xs). Por tanto,
estaEn a (borraDuplicados (b#xs)) = (def. de borraDuplicados)
estaEn a ( b # (borraDuplicados xs)) = (def. de estaEn)
(a = b) ∨ (estaEn a (borraDuplicados xs) = (por HI)
(a = b) ∨ (estaEn a xs = (def. de estaEn)
estaEn a (b#xs)
›

― ‹Demostración estructurada:›
lemma
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix b xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)"
proof (cases)
assume "estaEn b xs"
then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (borraDuplicados xs)" by (rule arg_cong)
also have "… = estaEn a xs" using HI by this
also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by auto
finally show ?thesis by this
next
assume " ¬ estaEn b xs"
then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
by (simp only: estaEn.simps(2))
also have "… = ((a = b) ∨ (estaEn a xs))" using HI by simp
also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
finally show ?thesis by this
qed
qed

― ‹Auxiliar:›

lemma estaEnCons:
assumes "estaEn b xs"
shows "estaEn a xs = estaEn a (b#xs)"
proof (rule iffI)
assume " estaEn a xs "
then have "((a = b) ∨ (estaEn a xs))" by (rule disjI2)
then show "estaEn a (b # xs)" by (simp only:estaEn.simps(2))
next
assume "estaEn a (b # xs)"
then have "((a = b) ∨ (estaEn a xs))" by (simp only:estaEn.simps(2))
then show "estaEn a xs"
proof
assume "a = b" then show "estaEn a xs" using assms by (rule ssubst)
next
assume "estaEn a xs" then show "estaEn a xs" by this
qed
qed

― ‹Demostración detallada declarativa:›
lemma estaEn_borraDuplicados_d:
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []"
by (simp only:borraDuplicados.simps(1))
next
fix b xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)"
proof (cases)
assume "estaEn b xs"
then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (borraDuplicados xs)" by (rule arg_cong)
also have "… = estaEn a xs" using HI by this
also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by (rule estaEnCons)
finally show ?thesis by this
next
assume " ¬ estaEn b xs"
then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
then have "estaEn a (borraDuplicados (b#xs)) =
estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
by (simp only: estaEn.simps(2))
also have "… = ((a = b) ∨ (estaEn a xs))" using HI by simp
also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
finally show ?thesis by this
qed
qed

― ‹Demostración detallada aplicativa:›
lemma
"estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply (simp only: borraDuplicados.simps(1))
apply (simp only: borraDuplicados.simps(2))
apply(split if_split)
apply (rule conjI)
apply (rule impI)
apply (simp only: estaEnCons)
apply (rule impI)
apply (simp only: estaEn.simps(2))
done

text ‹
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
›

― ‹Demostración automática:›
lemma "sinDuplicados (borraDuplicados xs)"
by (induct xs)
(auto simp add: estaEn_borraDuplicados_d)

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base:
sinDuplicados (borraDuplicados []), directamente por las definiciones.

+ Paso inductivo:
+ HI: sinDuplicados (borraDuplicados xs)
+ Hay que probar: sinDuplicados (borraDuplicados (a#xs))
La demostración se realiza por casos.

+ Caso 1: estaEn a xs
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
sinDuplicados (borraDuplicados (a#xs)) = (def.de borraDuplicados)
sinDuplicados (borraDuplicados xs) (cierto, por HI)

+ Caso 2: ¬ (estaEn a xs)
En este caso, por la definición de borraDuplicados,
borraDuplicados (a#xs) = a # (borraDuplicados xs). Por tanto,
sinDuplicados (borraDuplicados (a#xs)) = (def. de borraDuplicados)
sinDuplicados (a#(borraDuplicados xs)) = (def. de sinDuplicados)
((¬ estaEn a (borraDuplicados xs)) ∧
sinDuplicados (borraDuplicados xs)) = (por hI)
¬ estaEn a (borraDuplicados xs) (cierto por la hipótesis del
caso 2 y el ejercicio 6)
›

― ‹Demostración estructurada:›
lemma
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados (xs :: 'a list))"
show "sinDuplicados (borraDuplicados (a#xs))"
proof (cases)
assume "estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
next
assume "¬ estaEn a xs"
thus "sinDuplicados (borraDuplicados (a#xs))"
using `¬ estaEn a xs` HI by (auto simp add: estaEn_borraDuplicados_d)
qed
qed

― ‹Demostración detallada declarativa:›
lemma sinDuplicados_borraDuplicados_d:
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])"
by (simp only: borraDuplicados.simps(1)
sinDuplicados.simps(1))
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados (xs:: 'a list))"
show "sinDuplicados (borraDuplicados (a#xs))"
proof (cases)
assume "estaEn a xs"
then have "borraDuplicados (a#xs) = borraDuplicados xs"
by (rule estaEnBD1)
then show "sinDuplicados (borraDuplicados (a#xs))" using HI
by (rule ssubst)
next
assume 1: "¬ estaEn a xs"
then have 2: "borraDuplicados (a#xs) = a#(borraDuplicados xs)"
by (rule estaEnBD2)
have "¬ estaEn a (borraDuplicados xs)" using 1
by (simp add: estaEn_borraDuplicados_d)
then have "¬ (estaEn a (borraDuplicados xs))
∧ sinDuplicados (borraDuplicados xs)"
using HI by (rule conjI)
then have "sinDuplicados (a#(borraDuplicados xs))"
by (simp only: sinDuplicados.simps(2)[THEN sym])
with 2 show "sinDuplicados (borraDuplicados (a#xs))"
by (rule ssubst)
qed
qed

text ‹
---------------------------------------------------------------------
Ejercicio 8. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
›

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
oops
(*
Auto Quickcheck found a counterexample:
xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
borraDuplicados (rev xs) = [a⇩2, a⇩1]
rev (borraDuplicados xs) = [a⇩1, a⇩2]
*)

end
</source>

Rel 11 (sol)

2020-05-12T10:04:21Z

Jalonso:

R12

2020-05-07T15:22:31Z

Jalonso:

<source lang = "isabelle">
chapter ‹ R12: Razonamiento sobre programas en Isabelle/HOL (III)›

theory R12
imports Main
begin

text ‹------------------------------------------------------------------
En toda la relación de ejercicios las demostraciones han de realizarse
de las formas siguientes:
+ en lenguaje natural
+ aplicativa o declarativa usando "simp"
+ aplicativa o declarativa usando "simp only: ..."
+ automática

Además, se recomienda el uso de lemas auxiliares (nuevos o de los
ejercicios anteriores) para que las demostraciones sean más cortas y
claras.
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Ejercicio 1. Definir la función
estaEn :: 'a ⇒ 'a list ⇒ bool
tal que (estaEn x xs) se verifica si el elemento x está en la lista
xs. Por ejemplo,
estaEn (2::nat) [3,2,4] = True
estaEn (1::nat) [3,2,4] = False
---------------------------------------------------------------------›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = (a=x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------
Ejercicio 2. Definir la función
sublista :: "'a list ⇒ 'a list ⇒ bool
tal que (sublista xs ys) se verifica si todos los elementos de la
lista xs están en la lista ys. Por ejemplo,
sublista [(1::nat),2,3] [3,2,1,2] = True
sublista [(1::nat),2,3] [2,1,2] = False
----------------------------------------------------------------------›

fun sublista :: "'a list ⇒ 'a list ⇒ bool" where
"sublista [] ys = True"
| "sublista (x#xs) ys = (estaEn x ys ∧ sublista xs ys )"

text ‹------------------------------------------------------------------
Ejercicio 3. Demostrar la siguiente propiedad: si xs es sublista de
ys, entonces xs también es sublista de la lista (y#ys). Es decir,
sublista xs ys ⟹ sublista xs (y#ys)
----------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaMono_d:
"sublista xs ys ⟶ sublista xs (y#ys)"
oops

― ‹Demostración aplicativa:›

lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y#ys)"
oops

text ‹------------------------------------------------------------------
Ejercicio 4. Demostrar que la relación sublista es reflexiva. Es
decir,
sublista xs xs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaReflexiva_d: "sublista xs xs"
oops

― ‹Demostración aplicativa:›

lemma sublistaReflexiva: "sublista xs xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 5. Probar, como corolario, que
sublista xs (x#xs)
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

corollary sublistaInc_d: "sublista xs (x#xs)"
oops

― ‹Demostración aplicativa:›

corollary sublistaInc: "sublista xs (x#xs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 6. Probar que la relación sublista es transitiva. Es decir,
sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaTransitiva_d:
"sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
oops

― ‹Demostración aplicativa:›

lemma sublistaTransitiva:
"sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
oops

text ‹------------------------------------------------------------------
Ejercicio 7. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ ›

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e] = [a,c]"

text ‹------------------------------------------------------------------
Ejercicio 8. Probar que
coge 0 xs = []
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma coge0_d: "coge 0 xs = []"
oops

― ‹Demostración aplicativa:›

lemma coge0: "coge 0 xs = []"
oops

text ‹------------------------------------------------------------------
Ejercicio 9. Probar que
length xs ≤ n ⟹ coge n xs = xs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeTodos_d:
"length xs ≤ n ⟶ coge n xs = xs"
oops

― ‹Demostración aplicativa:›

lemma cogeTodos: "length xs ≤ n ⟹ coge n xs = xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 10. Probar que
length (coge n xs) ≤ n
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeLongN_d: "length (coge n xs) ≤ n"
oops

― ‹Demostración aplicativa:›

lemma cogeLongN: "length (coge n xs) ≤ n"
oops

text ‹------------------------------------------------------------------
Ejercicio 11. Probar que
length (coge n xs) ≤ length xs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma cogeLongL_d: "length (coge n xs) ≤ length xs"
oops

― ‹Demostración aplicativa:›

lemma cogeLongL: "length (coge n xs) ≤ length xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 12. Probar que
length (coge n xs) = min n (length xs)
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma lengthCogeMin_d:"length (coge n xs) = min n (length xs)"
oops

― ‹Demostración aplicativa:›

lemma lengthCogeMin: "length (coge n xs) = min n (length xs)"
oops

text ‹------------------------------------------------------------------
Ejercicio 13. Probar que
estaEn x (coge n xs) ⟹ estaEn x xs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma estaEnCoge_d:
"estaEn x (coge n xs) ⟶ estaEn x xs"
oops

― ‹Demostración aplicativa:›

lemma estaEnCoge:
"estaEn x (coge n xs) ⟹ estaEn x xs"
oops

text ‹------------------------------------------------------------------
Ejercicio 14. Probar que
sublista (coge n xs) xs
---------------------------------------------------------------------›

text ‹------------------------------------------------------------------
Demostración en lenguaje natural:

----------------------------------------------------------------------›

― ‹Demostración declarativa:›

lemma sublistaCoge_d: "sublista (coge n xs) xs"
oops

― ‹Demostración aplicativa:›

lemma sublistaCoge: "sublista (coge n xs) xs"
oops

end
</source>

MediaWiki:Sidebar

2020-04-25T18:27:24Z

Jalonso:

* navigation
** mainpage|mainpage-description
** Ejercicios|Ejercicios
** recentchanges-url|recentchanges
* Ayudas
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX|Ayuda de LaTeX
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX#L%C3%B3gica|Lógica en LaTeX
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX#Conjuntos|Conjuntos en LaTeX
* SEARCH
* TOOLBOX
* LANGUAGES

Ejercicios

2020-03-26T06:17:05Z

Jalonso:

Ejercicios

2020-03-17T16:24:29Z

Jalonso:

Ejercicios

2020-03-08T07:04:06Z

Jalonso:

Lógica matemática y fundamentos (3º Matemáticas)

2020-02-07T11:11:42Z

Jalonso:

Este sitio contiene materiales del curso [https://www.cs.us.es/~jalonso/cursos/lmf-19 '''Lógica matemática y fundamentos'''] de 3º del [http://www.us.es/estudios/grados/plan_171?p=7 Grado en Matemáticas] de la [http://www.us.es Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Transparencias de los temas y teorías.
* [[Ejercicios]]: Relaciones de ejercicios.

Ejercicios

2020-02-07T11:10:50Z

Jalonso: Página creada con «En esta página se encuentran los ejercicios para resolver de manera colaborativa que complementan al [https://www.cs.us.es/~jalonso/cursos/lmf-19/ejercicios/ejercicios-LMF…»

Lógica matemática y fundamentos (3º Matemáticas)

2020-02-07T11:05:18Z

Jalonso: Página creada con «Este sitio contiene materiales del curso [https://www.cs.us.es/~jalonso/cursos/lmf/temas.php '''Lógica matemática y fundamentos'''] de 3º del [http://www.us.es/estudios/…»

Este sitio contiene materiales del curso [https://www.cs.us.es/~jalonso/cursos/lmf/temas.php '''Lógica matemática y fundamentos'''] de 3º del [http://www.us.es/estudios/grados/plan_171?p=7 Grado en Matemáticas] de la [http://www.us.es Universidad de Sevilla].

== Material para el curso ==
* [[Temas]]: Transparencias de los temas y teorías.
* [[Ejercicios]]: Relaciones de ejercicios.

MediaWiki:Mainpage

2020-02-07T11:03:56Z

Jalonso: Página creada con «Lógica matemática y fundamentos (3º Matemáticas)»

Lógica matemática y fundamentos (3º Matemáticas)

MediaWiki:Sidebar

2020-02-07T11:01:59Z

Jalonso: Página creada con «* navigation ** mainpage|mainpage-description ** Temas|Temas ** Ejercicios|Ejercicios ** recentchanges-url|recentchanges * Ayudas ** https://es.wikipedia.org/wiki/Ayuda:Uso…»

* navigation
** mainpage|mainpage-description
** Temas|Temas
** Ejercicios|Ejercicios
** recentchanges-url|recentchanges
* Ayudas
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX|Ayuda de LaTeX
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX#L%C3%B3gica|Lógica en LaTeX
** https://es.wikipedia.org/wiki/Ayuda:Uso_de_TeX#Conjuntos|Conjuntos en LaTeX
* SEARCH
* TOOLBOX
* LANGUAGES

MediaWiki:Common.css

2020-02-07T10:57:23Z

Jalonso: Página creada con «/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */ @import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");»

/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */
@import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");