Diferencia entre revisiones de «Relación 5»
De Razonamiento automático (2016-17)
m (Texto reemplazado: «isar» por «isabelle») |
|||
| Línea 1: | Línea 1: | ||
| − | <source lang=" | + | <source lang="isabelle"> |
chapter {* R5: Eliminación de duplicados *} | chapter {* R5: Eliminación de duplicados *} | ||
Revisión actual del 13:11 16 jul 2018
chapter {* R5: Eliminación de duplicados *}
theory R5_Eliminacion_de_duplicados
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la funcion primitiva recursiva
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
---------------------------------------------------------------------
*}
(* crigomgom rubgonmar bowma wilmorort pablucoto serrodcal
anaprarod migtermor paupeddeg fraortmoy marpoldia1
danrodcha manmorjim1 jeamacpov marcarmor13*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn _ [] = False"
| "estaEn x (a#xs) = ((a = x) ∨ (estaEn x xs))"
value "estaEn (2::nat) [3,2,4] = True"
value "estaEn (1::nat) [3,2,4] = False"
(* ivamenjim ferrenseg josgarsan juacabsou dancorgar pabrodmac lucnovdos
fracorjim1 antsancab1 *)
(* Igual que la anterior pero con x en lugar de _ en el caso base *)
fun estaEn1 :: "'a ⇒ 'a list ⇒ bool" where
"estaEn1 x [] = False"
| "estaEn1 x (a#xs) = ((x=a) ∨ estaEn1 x xs)"
value "estaEn1 (2::nat) [3,2,4] = True"
value "estaEn1 (1::nat) [3,2,4] = False"
(* wilmorort *)
(* reutilizando la funcion "algunos" de R4.thy*)
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
| "algunos p (x#xs) = (p x ∨ algunos p xs)"
fun estaEn2 :: "'a ⇒ 'a list ⇒ bool" where
"estaEn2 a xs = algunos (λx. x = a) xs"
value "estaEn2 (2::nat) [3,2,4] = True"
value "estaEn2 (1::nat) [3,2,4] = False"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función primitiva recursiva
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
---------------------------------------------------------------------
*}
(* crigomgom rubgonmar ivamenjim wilmorort bowma pablucoto
serrodcal anaprarod migtermor paupeddeg fraortmoy marpoldia1
ferrenseg josgarsan danrodcha manmorjim1 juacabsou dancorgar
pabrodmac lucnovdos jeamacpov marcarmor13 antsancab1 *)
fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = True"
| "sinDuplicados (x#xs) = (¬ estaEn x xs ∧ sinDuplicados xs)"
value "sinDuplicados [1::nat,4,2] = True"
value "sinDuplicados [1::nat,4,2,4] = False"
(* fracorjim1 - La versión anterior no prueba el segundo enunciado. La
que propongo demuestra ambos. *)
fun sinDuplicados1 :: "'a list ⇒ bool" where
"sinDuplicados1 [] = True"
| "sinDuplicados1 (x#xs) = (¬(estaEn x xs ∧ sinDuplicados xs))"
value "sinDuplicados1 [1::nat,4,2] = True"
value "sinDuplicados1 [1::nat,4,2,4] = False"
(* Comentario: La definición sinDuplicados1 no cumple el segundo
ejemplo. *)
(* paupeddeg *)
(* Utilizando la función ∉ de Isabelle *)
fun sinDuplicados2 :: "'a list ⇒ bool" where
"sinDuplicados2 [] = True"
| "sinDuplicados2 (a#xs) = ((a ∉ set xs) ∧ sinDuplicados2 xs ) "
(* Comentario: Uso de ∉ y set *)
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función primitiva recursiva
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.
---------------------------------------------------------------------
*}
(* crigomgom rubgonmar wilmorort bowma pablucoto serrodcal
anaprarod migtermor paupeddeg fraortmoy marpoldia1 ferrenseg
josgarsan danrodcha juacabsou dancorgar manmorjim1 pabrodmac
lucnovdos jeamacpov marcarmor13 antsancab1 *)
fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if estaEn x xs
then borraDuplicados xs
else x#borraDuplicados xs)"
value "borraDuplicados0 [1::nat,2,4,2,3] = [1,4,2,3]"
(* rubgonmar *)
(* Otra forma Sin usar if
Utilizando case aunque se le sacaría más partido con más de 2 casos *)
fun borraDuplicados1 :: "'a list ⇒ 'a list" where
"borraDuplicados1 [] = []"
| "borraDuplicados1 (x#xs) = (case estaEn x xs of
False => x#borraDuplicados1 xs
| True => borraDuplicados1 xs )"
value "borraDuplicados1 [1::nat,2,4,2,3] = [1,4,2,3]"
(* rubgonmar *)
(* Otra forma utilizando let *)
fun borraDuplicados2 :: "'a list ⇒ 'a list" where
"borraDuplicados2 [] = []"
| "borraDuplicados2 (x#xs) =
(let condicion = estaEn x xs::bool in
if condicion
then borraDuplicados2 xs
else x # borraDuplicados2 xs)"
value "borraDuplicados2 [1::nat,2,4,2,3] = [1,4,2,3]"
(* ivamenjim *)
(* Utilizando la negación primero *)
fun borraDuplicados3 :: "'a list ⇒ 'a list" where
"borraDuplicados3 [] = []"
| "borraDuplicados3 (x#xs) = (if ¬(estaEn x xs)
then (x#(borraDuplicados3 xs))
else borraDuplicados3 xs)"
value "borraDuplicados3 [1::nat,2,4,2,3] = [1,4,2,3]"
(* fracorjim1. Utilizo un acumulador para optimizar la eficiencia *)
fun borraDuplicadosAc :: "'a list ⇒ 'a list ⇒ 'a list" where
"borraDuplicadosAc [] ys = ys"
| "borraDuplicadosAc (x#xs) ys = (if (estaEn x ys)
then (borraDuplicadosAc xs ys)
else (borraDuplicadosAc xs (x#ys)))"
(* fracorjim1. Uso un caso base *)
fun borraDuplicados4 :: "'a list ⇒ 'a list" where
"borraDuplicados4 xs = (if (sinDuplicados xs)
then xs
else borraDuplicadosAc xs [])"
value "borraDuplicados4 [1::nat,2,4,2,3] = [1,4,2,3]"
(* Comentario: Falla en el ejemplo anterior. Su valor es [3,4,2,1] *)
text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}
(* crigomgom anaprarod ferrenseg *)
lemma length_borraDuplicados:
"length (borraDuplicados xs) ≤ length xs"
by (induct xs, simp_all)
(* Comentario: Falla para borraDuplicados1. *)
(* rubgonmar wilmorort pablucoto serrodcal migtermor paupeddeg
fraortmoy marpoldia1 danrodcha juacabsou dancorgar josgarsan
pabrodmac lucnovdos antsancab1 *)
lemma length_borraDuplicados2:
"length ( borraDuplicados xs ) ≤ length xs"
by (induct xs) auto
(* manmorjim1 marcarmor13 *)
(* soy de ponerlo mejor por pasos *)
lemma length_borraDuplicados3:
"length ( borraDuplicados xs ) ≤ length xs"
apply (induct xs)
apply auto
done
(* ivamenjim *)
(* Demostrando objetivo a objetivo *)
lemma length_borraDuplicados4:
"length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply simp
apply auto
done
(* bowma anaprarod *)
lemma length_borraDuplicados5:
"length (borraDuplicados xs) ≤ length xs"
apply (induct xs)
apply (simp, simp) (* creo que es mejor poner aquí simp_all *)
done
(* ferrenseg *)
lemma length_borraDuplicados6:
"length (borraDuplicados xs) ≤ length xs"
by (induct xs) simp_all (* Creo que se puede poner simp_all fuera de
paréntesis *)
text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}
(* crigomgom *)
lemma length_borraDuplicados_2:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix x xs
assume HI: "length (borraDuplicados xs) ≤ length xs"
show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"
proof (cases)
assume "estaEn x xs"
then have "length (borraDuplicados (x#xs)) =
length (borraDuplicados xs)" by simp
also have "... ≤ length xs" using HI by simp
also have "... ≤ length (x#xs)" by simp
finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"
by simp
next
assume "(¬ estaEn x xs)"
then have "length (borraDuplicados (x#xs)) =
length (x#borraDuplicados xs)" by simp
also have "... = 1 + length (borraDuplicados xs)" by simp
also have "... ≤ 1 + length xs" using HI by simp
also have "... = length (x#xs)" by simp
finally show "length (borraDuplicados (x#xs)) ≤ length (x#xs)"
by simp
qed
qed
(* ivamenjim wilmorort ferrenseg rubgonmar juacabsou dancorgar
josgarsan lucnovdos *)
lemma length_borraDuplicados_2b:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "length (borraDuplicados xs) ≤ length xs"
have "length (borraDuplicados (a # xs)) ≤
1+length (borraDuplicados xs)" by simp
also have "... ≤ 1+length xs" using HI by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)"
by simp
qed
(* serrodcal anaprarod danrodcha *)
lemma length_borraDuplicados_2c:
"length (borraDuplicados xs) ≤ length xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix a xs
assume HI: "?P xs"
have "length (borraDuplicados (a # xs)) ≤
1+length (borraDuplicados xs)" by simp
also have "... ≤ 1+length xs" using HI by simp
finally show "?P (a # xs)" by simp
qed
(* pablucoto jeamacpov marcarmor13*)
lemma length_borraDuplicados_2d:
"length (borraDuplicados xs) ≤ length xs"
proof(induct xs)
show "length (borraDuplicados []) ≤ length [] " by simp
next
fix a xs
assume HI: " length (borraDuplicados xs) ≤ length xs "
have "length (borraDuplicados (a # xs)) ≤
1 + length(borraDuplicados xs)" by simp
also have "... ≤ 1 + length xs" using HI by simp
also have "... ≤ length (a#xs)" by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs) "
by simp
qed
(* bowma *)
lemma length_borraDuplicados_2f:
"length (borraDuplicados xs) ≤ length xs" (is "?p xs")
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "?p xs"
have c1: "1+length xs = length (a#xs)" by simp
also have "length(borraDuplicados (a#xs)) ≤
1 + length(borraDuplicados xs)" by simp
also have "... ≤ 1+length xs" using HI by simp
then show "length(borraDuplicados (a#xs)) ≤ length (a#xs)"
using c1 by simp
(* ¿Aquí porqué no puedo usar "finally show "?p (a # xs)" using c1 by simp?
Y porque no puedo añadir "finally show "?p (a # xs)" by simp al final? *)
qed
(* Comentario: Responder la pregunta. *)
(* migtermor *)
lemma length_borraDuplicados_2g:
"length (borraDuplicados xs) ≤ length xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix a xs
assume HI: "?P xs"
have "length (borraDuplicados (a#xs)) ≤ (length (a#xs))"
proof (cases)
assume "(estaEn a xs)"
then have Aux: "length (borraDuplicados (a#xs)) =
length (borraDuplicados xs)" by simp
also have "… ≤ length (a#xs)" using HI by simp
then show "length (borraDuplicados (a#xs)) ≤ (length (a#xs))"
using Aux by simp
next
assume "¬ (estaEn a xs)"
then have Aux: "length (borraDuplicados (a#xs)) =
1+ length (borraDuplicados xs)" by simp
also have "… ≤ length (a#xs)" using HI by simp
then show "length (borraDuplicados (a#xs)) ≤ (length (a#xs))"
using Aux by simp
qed
then show "?P (a#xs)" by simp
qed
(* paupeddeg marpoldia1 pabrodmac*)
lemma length_borraDuplicados_2h:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "length (borraDuplicados xs) ≤ length xs"
have "length (borraDuplicados (a # xs)) ≤
length [a] + length (borraDuplicados xs) " by simp
also have "... ≤ 1 + length (borraDuplicados xs)" by simp
also have "... ≤ 1 + length xs" using HI by simp
finally show "length (borraDuplicados (a # xs)) ≤
length (a # xs)" by simp
qed
(* fraortmoy *)
(* muy parecida a alguna anterior, pero yo dí más pasos *)
lemma length_borraDuplicados_2i:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume H1: "length (borraDuplicados xs) ≤ length xs"
have "length (borraDuplicados (a # xs)) ≤
length(borraDuplicados [a])+length (borraDuplicados xs)"
by simp
also have "… ≤ 1 + length (borraDuplicados xs)" by simp
also have "… ≤ 1 + length xs" using H1 by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs)"
by simp
qed
(* antsancab1 *)
(* En este ejercicio probé a mantener el elemento 'a' dentro del métodos length y funciona
Para no tener que hacer 1 + length xs *)
(* Duda:
¿Por qué aparece este mensaje en Isabelle al asumir la hipótesis de inducción?
Introduced fixed type variable(s): 'b in "xsa__" *)
lemma length_borraDuplicados_2j: "length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
show "length (borraDuplicados []) ≤ length []" by simp
next
fix a xs
assume HI: "length (borraDuplicados xs) ≤ length xs"
have "length (borraDuplicados (a # xs)) ≤ length (a # borraDuplicados (xs))" by simp
also have "... ≤ length (a # xs)" using HI by simp
finally show "length (borraDuplicados (a # xs)) ≤ length (a # xs) " by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}
(* crigomgom rubgonmar wilmorort pablucoto serrodcal bowma
migtermor fraortmoy marpoldia1 ferrenseg danrodcha juacabsou
paupeddeg pabrodmac lucnovdos dancorgar jeamacpov marcarmor13 antsancab1 *)
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto
(* ivamenjim manmorjim1 *)
lemma estaEn_borraDuplicados2:
"estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply auto
done
(* anaprarod *)
lemma estaEn_borraDuplicados3:
"estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs, simp_all, blast)
(* anaprarod *)
lemma estaEn_borraDuplicados4:
"estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply (cases "estaEn x xs")
apply (simp_all)
apply blast
done
(* bowma *)
lemma estaEn_borraDuplicados5:
"estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs)
apply simp
apply (simp, blast)
done
text {*
---------------------------------------------------------------------
Ejercicio 5.2. Demostrar o refutar detalladamente
estaEn a (borraDuplicados xs) = estaEn a xs
Nota: Para la demostración de la equivalencia se puede usar
proof (rule iffI)
La regla iffI es
⟦P ⟹ Q ; Q ⟹ P⟧ ⟹ P = Q
---------------------------------------------------------------------
*}
(* wilmorort *)
lemma estaEn_borraDuplicados_2:
"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 (rule iffI)
assume H1: "estaEn a (borraDuplicados (b#xs))"
show "estaEn a (b#xs)"
proof (cases)
assume "estaEn b xs"
then have "estaEn a (borraDuplicados xs)" using H1 by simp
then have "estaEn a xs" using HI by simp
then show "estaEn a (b#xs)" by simp
next
assume "¬ estaEn b xs"
then have "estaEn a (b#(borraDuplicados xs))" using H1 by simp
then have "a=b ∨ (estaEn a (borraDuplicados xs))" by simp
then have " a=b ∨ (estaEn a xs)" using HI by simp
then show "estaEn a (b#xs)" by simp
qed
next
assume H2: "estaEn a (b#xs)"
show "estaEn a (borraDuplicados (b#xs))"
proof (cases)
assume "a=b"
then have "estaEn b (borraDuplicados xs) = estaEn b xs"
using HI by simp
then have "(estaEn b xs ⟶ estaEn b (borraDuplicados xs)) ∧
(¬ estaEn b xs ⟶ estaEn b (b # borraDuplicados xs))"
by simp
then have "estaEn b (borraDuplicados (b#xs))" by simp
then show "estaEn a (borraDuplicados (b#xs))" using `a=b` by simp
next
assume "a≠b"
then have "estaEn a (b#xs)" using H2 by simp
then have "a = b ∨ estaEn a xs" by simp
then have "False ∨ estaEn a xs " using `a≠b` by simp
then have "estaEn a xs" by simp
then have "estaEn a (borraDuplicados xs)" using HI by simp
then show "estaEn a (borraDuplicados (b#xs))" using `a≠b` by simp
qed
qed
qed
(* Comentario: Tiene pasos incompletos.*)
(* anaprarod marpoldia1 ferrenseg juacabsou *)
lemma estaEn_borraDuplicados_2b:
"estaEn a (borraDuplicados xs) = estaEn a xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
show "?P (x#xs)"
proof (cases)
assume "estaEn x xs"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (borraDuplicados xs)" by simp
also have "...= estaEn a xs" using HI by simp
finally show "?P (x#xs)" by auto
next
assume "¬estaEn x xs"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (x#borraDuplicados xs)" by simp
also have "...= (x = a ∨ estaEn a (borraDuplicados xs))" by simp
finally show "?P (x#xs)" using HI by simp
qed
qed
(* migtermor *)
lemma estaEn_borraDuplicados_2c:
"estaEn a (borraDuplicados xs) = estaEn a xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix aa xs
assume HI: "?P xs"
have P1: "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)"
proof (cases)
assume C1: "(estaEn aa xs)"
have "estaEn a (borraDuplicados (aa#xs)) =
estaEn a (borraDuplicados xs)"
using C1 by simp
also have P3: "… = estaEn a xs" using HI by simp
also have "… = estaEn a (aa#xs)"
proof (cases)
assume "(a=aa)"
then show "estaEn a xs = estaEn a (aa#xs)" using C1 by simp
next
assume "¬(a=aa)"
then show "estaEn a xs = estaEn a (aa#xs)" by simp
qed
then show "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)"
using P3 by simp
next
assume C2: "¬(estaEn aa xs)"
then show "estaEn a (borraDuplicados (aa#xs)) =
estaEn a (aa#xs)" using HI by simp
qed
also have Conc: "estaEn a (borraDuplicados (aa#xs)) = estaEn a (aa#xs)"
using P1 by simp
finally show "?P (aa#xs)" using Conc by simp
qed
(* crigomgom paupeddeg pabrodmac marcarmor13*)
lemma estaEn_borraDuplicados_2d:
"estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix x xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
proof (rule iffI)
assume a1: "estaEn a (borraDuplicados (x#xs))"
show "estaEn a (x#xs)"
proof (cases)
assume "estaEn x xs"
then have "estaEn a (borraDuplicados xs)" using a1 by simp
then have "estaEn a xs" using HI by simp
then show "estaEn a (x#xs)" by simp
next
assume "¬ estaEn x xs"
then have "estaEn a (x#(borraDuplicados xs))" using a1 by simp
then have " x=a ∨ (estaEn a (borraDuplicados xs))" by simp
then have " x=a ∨ (estaEn a xs)" using HI by simp
then show "estaEn a (x#xs)" by simp
qed
next
assume a2: "estaEn a (x#xs)"
show "estaEn a (borraDuplicados (x#xs))"
proof (cases)
assume "a=x"
then show "estaEn a (borraDuplicados (x#xs))" using HI by simp
next
assume b1: "a≠x"
then have "estaEn a (x#xs)" using a2 by simp
then have "x = a ∨ estaEn a xs" by simp
then have "estaEn a xs " using b1 by simp
then have "estaEn a (borraDuplicados xs)" using HI by simp
then show "estaEn a (borraDuplicados (x#xs))" using b1 by simp
qed
qed
qed
(* rubgonmar jeamacpov *)
lemma estaEn_borraDuplicados_2e:
"estaEn a ( borraDuplicados xs ) = estaEn a xs"
proof (induct xs)
show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
fix x
fix xs
assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
show "estaEn a (borraDuplicados (x#xs)) = estaEn a (x#xs)"
proof (rule iffI) (* usamos proof de la regla dada iffI*)
assume cprim: "estaEn a (borraDuplicados (x#xs))"
show "estaEn a (x#xs)"
proof (cases)
assume "estaEn x xs"
then show "estaEn a (x#xs)" using cprim HI by simp
next
assume "¬ estaEn x xs"
then show "estaEn a (x#xs)" using cprim HI by simp
qed
next
assume cseg: "estaEn a (x#xs)"
show "estaEn a (borraDuplicados (x#xs))"
proof (cases)
assume "a=x"
then show "estaEn a (borraDuplicados (x#xs))" using HI by auto
next
assume "a≠x"
then show "estaEn a (borraDuplicados (x#xs))" using `a≠x`
cseg HI by simp
qed
qed
qed
(*
Aplico la regla iffI:
⟦P ⟹ Q ; Q ⟹ P⟧ ⟹ P = Q
Así:
[estaEn a (borraDuplicados (x # xs))
⟹ estaEn a (x # xs); estaEn a (x # xs)
⟹ estaEn a (borraDuplicados (x # xs))]
⟹ estaEn a (borraDuplicados (x # xs)) = estaEn a (x # xs)
*)
(* bowma ivamenjim *)
lemma estaEn_borraDuplicados_2f:
"estaEn a (borraDuplicados xs) = estaEn a xs" (is "?p xs")
proof (induct xs)
show "?p []" by simp
next
fix x xs
assume HI: "?p xs"
show "?p (x#xs)"
proof (cases)
assume H1:"estaEn x xs"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (borraDuplicados xs)" by simp
also have "... = estaEn a xs" using HI by simp
also have "... = estaEn a (x#xs)"
proof(cases)
assume "x=a"
then show "estaEn a xs = estaEn a (x#xs)" using H1 by simp
next
assume "x≠a"
then show "estaEn a xs = estaEn a (x#xs)" by simp
qed
finally show "?p (x#xs)" by simp
next
assume H2:"¬estaEn x xs"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (x#borraDuplicados xs)" by simp
also have "... = ((x=a) ∨ estaEn a (borraDuplicados xs))" by simp
also have "... = ((x=a) ∨ estaEn a xs)" using HI by simp
also have "... = estaEn a (x#xs)" by simp
finally show "?p (x#xs)" by simp
qed
oops
(* Comentario: Demostración incompleta. *)
(* danrodcha pablucoto *)
(* es como la de ruben pero con diferencias de estilo *)
lemma estaEn_borraDuplicados_2g:
"estaEn a (borraDuplicados xs) = estaEn a xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs assume HI: "?P xs"
show "?P (x#xs)"
proof (rule iffI)
assume H1: "estaEn a (borraDuplicados (x # xs))"
show "estaEn a (x#xs)"
proof (cases "estaEn x xs")
case True
then show "estaEn a (x#xs)" using H1 HI by simp
next
case False
then show "estaEn a (x#xs)" using H1 HI by simp
qed
next
assume H2: "estaEn a (x#xs)"
show "estaEn a (borraDuplicados (x # xs))"
proof (cases "x=a")
case True
then show "estaEn a (borraDuplicados (x # xs))" using HI by simp
next
case False
then show "estaEn a (borraDuplicados (x # xs))" using H2 HI
by simp
qed
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 6.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}
(* ivamenjim wilmorort serrodcal crigomgom anaprarod fraortmoy
marpoldia1 ferrenseg danrodcha juacabsou paupeddeg josgarsan
pabrodmac dancorgar jeamacpov rubgonmar marcarmor13 *)
lemma sinDuplicados_borraDuplicados:
"sinDuplicados (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)
(* migtermor bowma *)
lemma sinDuplicados_borraDuplicados_2:
"sinDuplicados (borraDuplicados xs)"
by (induct xs, simp_all add: estaEn_borraDuplicados_2)
(* manmorjim1 no caí en usar la demostración anterior y he realizado
la demostración de que si un elemento no estaba en una lista seguirá
sin estar después de eliminar los duplicados en esa lista... *)
lemma noEsta_tras_borrarDuplicados:
"(¬estaEn x xs) ⟶ (¬estaEn x (borraDuplicados xs))"
apply (induct xs)
apply auto
done
lemma sinDuplicados_borraDuplicados_3:
"sinDuplicados (borraDuplicados xs)"
apply (induct xs)
apply simp
apply (induct xs)
apply auto
apply (simp add: noEsta_tras_borrarDuplicados)
done
(* antsancab1 *)
lemma sinDuplicados_borraDuplicados_4:
"sinDuplicados (borraDuplicados xs)"
apply (induct xs)
apply simp
apply (simp add:estaEn_borraDuplicados)
done
text {*
---------------------------------------------------------------------
Ejercicio 6.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}
(* wilmorort pablucoto marcarmor13*)
lemma sinDuplicados_borraDuplicados_2a:
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados xs)"
show "sinDuplicados (borraDuplicados (a # xs))"
proof (cases)
assume "estaEn a xs"
then show "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
next
assume"¬ estaEn a xs"
then have "¬ (estaEn a xs) ∧ sinDuplicados (borraDuplicados xs)"
using HI by simp
then have "¬ estaEn a (borraDuplicados xs) ∧
sinDuplicados (borraDuplicados xs)"
by (simp add: estaEn_borraDuplicados)
then have " sinDuplicados (a#borraDuplicados xs)" by simp
then show " sinDuplicados (borraDuplicados(a #xs))" by simp
qed
qed
(* ivamenjim migtermor crigomgom rubgonmar fraortmoy marpoldia1
ferrenseg bowma juacabsou serrodcal josgarsan pabrodmac dancorgar
jeamacpov lucnovdos antsancab1 *)
lemma sinDuplicados_borraDuplicados_2b:
"sinDuplicados (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados (borraDuplicados [])" by simp
next
fix a xs
assume HI: "sinDuplicados (borraDuplicados xs)"
show "sinDuplicados (borraDuplicados (a # xs))"
proof (cases)
assume "estaEn a xs"
then show "sinDuplicados (borraDuplicados (a # xs))"
using HI by simp
next
assume "¬(estaEn a xs)"
then show "sinDuplicados (borraDuplicados (a # xs))"
using HI by (simp add: estaEn_borraDuplicados)
qed
qed
(* anaprarod paupeddeg*)
lemma sinDuplicados_borraDuplicados_2c:
"sinDuplicados (borraDuplicados xs)" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
show "?P (x#xs)"
proof (cases)
assume c1: "estaEn x xs"
then show "sinDuplicados (borraDuplicados (x#xs))" using HI by simp
next
assume c2: "¬ estaEn x xs"
then have "sinDuplicados (borraDuplicados (x#xs)) =
sinDuplicados (x#borraDuplicados xs)" by simp
also have "…= (¬estaEn x (borraDuplicados xs) ∧
sinDuplicados (borraDuplicados xs))" by simp
also have "… = (¬estaEn x (borraDuplicados xs))" using HI by simp
also have "… = (¬(estaEn x xs))"
by (simp add:estaEn_borraDuplicados)
also have "… = True" using c2 by simp
finally show "?P (x#xs)" by simp
qed
qed
(* danrodcha *)
lemma sinDuplicados_borraDuplicados_2d:
"sinDuplicados (borraDuplicados xs)" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs assume HI: "?P xs"
show "?P (x#xs)"
proof (cases "estaEn x xs")
case True
then have 1: "sinDuplicados (borraDuplicados (x#xs))
= sinDuplicados (borraDuplicados xs)"
by (simp add: estaEn_borraDuplicados_2)
show "?P (x#xs)" using HI 1 by simp
next
case False
then have "sinDuplicados (borraDuplicados (x#xs))
= sinDuplicados (x#borraDuplicados xs)" by simp
also have "… = (¬ (estaEn x (borraDuplicados xs)) ∧
sinDuplicados (borraDuplicados xs))" by simp
also have "… = True" using `¬ estaEn x xs`
using HI by (simp add:estaEn_borraDuplicados)
finally show "?P (x#xs)" by simp
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 7. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
*}
(* crigomgom rubgonmar ivamenjim wilmorort pablucoto migtermor
anaprarod fraortmoy ferrenseg marpoldia1 bowma danrodcha juacabsou
paupeddeg manmorjim1 serrodcal josgarsan pabrodmac lucnovdos
dancorgar jeamacpov marcarmor13 antsancab1 *)
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
quickcheck
oops
(* ivamenjim: Quickcheck encuentra el siguiente contraejemplo:
xs = [a1, a2, a1]
Por lo que:
· "borraDuplicados (rev xs) = [a2, a1]"
· "rev (borraDuplicados xs) = [a1, a2]" *)
end