Relación 5
De Razonamiento automático (2014-15)
Revisión del 12:02 19 nov 2014 de Juacorvic (discusión | contribuciones)
header {* R5: Cuantificadores sobre listas *}
theory R5
imports Main
begin
text {*
---------------------------------------------------------------------
Ejercicio 1. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
todos (λx. 1<length x) [[2,1,4],[1,3]]
¬todos (λx. 1<length x) [[2,1,4],[3]]
Nota: La función todos es equivalente a la predefinida list_all.
---------------------------------------------------------------------
*}
--"jeshorcob,javrodviv1,juacorvic"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p [] = True"
|"todos p (x#xs) = (p x ∧ todos p xs)"
--"jeshorcob"
fun todos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos2 p xs = foldr (λx. op ∧ (p x)) xs True"
--"emimarriv"
fun todos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos3 p [] = True"
| "todos3 p (x#xs) = (if p x then (todos3 p xs) else False)"
text {*
---------------------------------------------------------------------
Ejercicio 2. Definir la función
algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (algunos p xs) se verifica si algunos elementos de la lista
xs cumplen la propiedad p. Por ejemplo, se verifica
algunos (λx. 1<length x) [[2,1,4],[3]]
¬algunos (λx. 1<length x) [[],[3]]"
Nota: La función algunos es equivalente a la predefinida list_ex.
---------------------------------------------------------------------
*}
(* Errata. Debe ser False el caso base seguro porque si no,
la función devuelve siempre True*)
--"jeshorcob,javrodviv1,juacorvic"
fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos p [] = False"
|"algunos p (x#xs) = (p x ∨ algunos p xs)"
--"jeshorcob"
fun algunos2 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos2 p xs = foldr (λx. op ∨ (p x)) xs False"
value "algunos (λx. x>10) [3::int,2]"
value "algunos2 (λx. x>10) [3::int,2]"
-- "javrodviv1"
fun algunos3 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos3 p [] = False"
|"algunos3 p (x#xs) = (p x ∨ todos p xs)"
(* Nota. Nos da igual que sea True o False, pero para una proposición
de más a delante necesitamos que sea False*)
(* jeshorcob: Debe ser False y la función tiene una errata en
la segunda linea porque la recursión la debe hacer sobre la función
algunos3 en lugar de todos *)
--"emimarriv"
fun algunos4 :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"algunos4 p [] =False"
| "algunos4 p (x#xs) = (if p x then True else (algunos4 p xs))"
text {*
---------------------------------------------------------------------
Ejercicio 3.1. Demostrar o refutar automáticamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}
--"jeshorcob,javrodviv1"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 3.2. Demostrar o refutar detalladamente
todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs) " by simp
also have "... = (P x∧Q x∧todos P xs∧todos Q xs)" using HI by simp
also have "... = ((P x∧todos P xs)∧(Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x#xs) ∧ (Q x ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x#xs) =
(todos P (x#xs) ∧ todos Q (x#xs))" by simp
qed
-- "juacorvic" (*Muy parecida a la solución anterior*)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x # xs) =
((P x ∧ Q x) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have "... = ((P x ∧ Q x) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
also have "... = (P x ∧ Q x ∧ todos P xs ∧ todos Q xs)" by simp
also have "... = ((P x ∧ todos P xs) ∧ (Q x ∧ todos Q xs))" by arith
also have "... = (todos P (x # xs) ∧ todos Q (x # xs))" by simp
finally show "todos (λx. P x ∧ Q x) (x # xs) = (todos P (x # xs) ∧ todos Q (x # xs))" by simp
qed
-- "javrodviv1"
lemma todo_append:
"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix a xs
assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (a # xs) = (((P a) ∧ (Q a)) ∧ todos (λx. P x ∧ Q x) xs)" by simp
also have " ... = ((P a) ∧ (Q a) ∧ todos P xs ∧ todos Q xs)" using HI by simp
finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))" by auto
qed
--"emimarriv"
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next
fix x xs
assume HI: "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
have "todos (λx. P x ∧ Q x) (x#xs) =((todos (λx. P x ∧ Q x) [x]) ∧ (todos (λx. P x ∧ Q x) xs))" by simp
also have "... = ((todos P [x] ∧ todos Q [x]) ∧ (todos P xs ∧ todos Q xs))" using HI by simp
also have "... = ((todos P [x] ∧ todos P xs) ∧ (todos Q [x] ∧ todos Q xs))" by simp
also have "... = (todos P (x#xs) ∧ todos Q (x#xs))" by simp (* emimarriv: Esta linea puede suprimirse, pero la dejo porque se sigue
mejor el proceso*)
finally show "todos (λx. P x ∧ Q x) (x#xs) = (todos P (x#xs) ∧ todos Q (x#xs))" by auto
qed
text {*
---------------------------------------------------------------------
Ejercicio 4.1. Demostrar o refutar automáticamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}
--"jeshorcob,javrodviv1,juacorvic"
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
by (induct x) auto
text {*
---------------------------------------------------------------------
Ejercicio 4.2. Demostrar o refutar detalladamente
todos P (x @ y) = (todos P x ∧ todos P y)
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma todos_append:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a#x)@y) = (P a ∧ todos P (x@y))" by simp
also have "... = (P a ∧ todos P x ∧ todos P y)" using HI by simp
also have "... = (todos P (a#x) ∧ todos P y)" by simp
finally show "todos P ((a#x)@y) =
(todos P (a#x) ∧ todos P y)" by simp
qed
-- "javrodviv1, emimarriv"
(* es igual que la de jeshorcob pero nos podemos ahorrar
una linea de comando*)
lemma todos_append2:
"todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI:"todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = ((P a) ∧ todos P (x @ y))" by simp
also have " ... = ((P a) ∧ todos P x ∧ todos P y)" using HI by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)"
by simp
qed
-- "juacorvic"
(* es igual que las anteriores pero salió con mayor nivel de detalle *)
lemma todos_append: "todos P (x @ y) = (todos P x ∧ todos P y)"
proof (induct x)
show "todos P ([] @ y) = (todos P [] ∧ todos P y)" by simp
next
fix a x
assume HI: "todos P (x @ y) = (todos P x ∧ todos P y)"
have "todos P ((a # x) @ y) = (P a ∧ todos P (x @ y))" by simp
also have "... = (P a ∧ (todos P x ∧ todos P y))" using HI by simp
also have "... = ((P a ∧ todos P x) ∧ todos P y)" by simp
also have "... = (todos P (a # x) ∧ todos P y)" by simp
finally show "todos P ((a # x) @ y) = (todos P (a # x) ∧ todos P y)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 5.1. Demostrar o refutar automáticamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma "todos P (rev xs) = todos P xs"
apply (induct xs)
apply (auto simp add: todos_append)
done
-- "javrodviv1, juacorvic"
lemma "todos P (rev xs) = todos P xs"
by (induct xs) (auto simp add: todos_append)
text {*
---------------------------------------------------------------------
Ejercicio 5.2. Demostrar o refutar detalladamente
todos P (rev xs) = todos P xs
---------------------------------------------------------------------
*}
--"jeshorcob, juacorvic"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show "todos P (rev []) = todos P []" by simp
next
fix x xs
assume HI: "todos P (rev xs) = todos P xs"
have "todos P (rev (x#xs)) = todos P ((rev xs) @ [x])" by simp
also have "... = (todos P (rev xs) ∧ todos P [x])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [x])" using HI by simp
also have "... = (todos P xs ∧ P x)" by simp
also have "... = (P x ∧ todos P xs)" by arith
also have "... = todos P (x#xs)" by simp
finally show "todos P (rev (x#xs)) = todos P (x#xs)" by simp
qed
-- "javrodviv1, emimarriv"
lemma "todos P (rev xs) = todos P xs"
proof (induct xs)
show " todos P (rev []) = todos P []" by simp
next
fix a xs
assume HI: "todos P (rev xs) = todos P xs "
have "todos P (rev (a # xs)) = todos P ((rev xs) @ [a])" by simp
also have " ... = (todos P (rev xs) ∧ todos P [a])"
by (simp add: todos_append)
also have "... = (todos P xs ∧ todos P [a])" using HI by simp
finally show " todos P (rev (a # xs)) = todos P (a # xs)" by auto
qed
text {*
---------------------------------------------------------------------
Ejercicio 6. Demostrar o refutar:
algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
---------------------------------------------------------------------
*}
(*Pedrosrei: No sé cómo has conseguido el contraejemplo,
probablemente algún fallo en los paréntesis, ya que la propiedad
resulta cierta como expongo abajo:
*)
(* jeshorcob: el contraejemplo existe. Fijate en lo siguiente: *)
fun p1 :: "int ⇒ bool" where
"p1 x = (x=3)"
fun q1 :: "int ⇒ bool" where
"q1 x = (x=2)"
value "algunos (λx. p1 x ∧ q1 x) [3,2]" -- "= False
(porque ningún elemento de la lista cumple a la vez p1 y q1)"
value "(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= True
(porque cada elemento de la lista cumple una sola de p1 y q1)"
(*Por tanto:*)
value "algunos (λx. p1 x ∧ q1 x) [3,2] =
(algunos p1 [3,2] ∧ algunos q1 [3,2])" -- "= False"
(*Esta es una instancia del contraejemplo que encuentra QuickCheck*)
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
by (metis (full_types) algunos.simps(1) algunos.simps(2) list_nonempty_induct)
(*Al cambiar la definición de algunos para que coincida con list_ex es cierto el
contraejemplo de Jesús
*)
-- "juacorvic"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
proof (induct xs)
show " algunos (λx. P x ∧ Q x) [] = (algunos P [] ∧ algunos Q [])" by simp
next
fix a xs
assume HI: "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
have "algunos (λx. P x ∧ Q x) (a # xs) = ((P a ∧ Q a) ∨ algunos (λx. P x ∧ Q x) xs)" by simp
also have "... = ((P a ∧ Q a) ∨ (algunos P xs ∧ algunos Q xs) )" using HI by simp
(* Ya no podemos seguir más ya que no se cuemple:
also have "... = ((P a ∨ algunos P xs) ∧ (Q a ∨ algunos Q xs))
Tenemos que buscar un contraejemplo:
*)
oops
--"jeshorcob, emimarriv, juacorvic"
lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
quickcheck
oops
text {* Encuentra el contraejemplo
P = {a⇩1}
Q = {a⇩2}
xs = [a⇩1, a⇩2]
*}
text {*
---------------------------------------------------------------------
Ejercicio 7.1. Demostrar o refutar automáticamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, juacorvic"
lemma "algunos P (map f xs) = algunos (P o f) xs"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 7.2. Demostrar o refutar datalladamente
algunos P (map f xs) = algunos (P ∘ f) xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, emimarriv, juacorvic"
lemma "algunos P (map f xs) = algunos (P o f) xs"
proof (induct xs)
show " algunos P (map f []) = algunos (P ∘ f) []" by simp
next
fix a xs
assume HI: "algunos P (map f xs) = algunos (P ∘ f) xs"
have "algunos P (map f (a # xs)) = ((P (f a)) ∨ algunos P (map f xs))" by simp
also have " ... = (((P ∘ f) a) ∨ algunos (P ∘ f) xs)" using HI by simp
finally show " algunos P (map f (a # xs)) = algunos (P ∘ f) (a # xs)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 8.1. Demostrar o refutar automáticamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}
(*Pedrosrei: Pongo la automática que parece se os resiste.*)
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (metis algunos.simps(1) algunos.simps(2) list_nonempty_induct)
(*Si corregís la definición de algunos sería: *)
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs, auto)
(*jeshorcob: Pedro, a la tuya no sé que le pasa que no me la coge bien.
Dejo la mía *)
--"jeshorcob,juacorvic"
lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 8.2. Demostrar o refutar detalladamente
algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, emimarriv"
lemma algunos_append:
"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
fix a xs
assume HI:"algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((a # xs) @ ys) = ((P a) ∨ algunos P (xs@ys))" by simp
also have "... = ((P a) ∨ (algunos P xs ∨ algunos P ys))"
using HI by simp
finally show "algunos P ((a # xs) @ ys) =
(algunos P (a # xs) ∨ algunos P ys)" by simp
qed
(*Igual que anterior, cambia uso de paréntesis y un paso más*)
-- "juacorvic"
lemma algunos_append: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
proof (induct xs)
show "algunos P ([] @ ys) = (algunos P [] ∨ algunos P ys)" by simp
next
fix a xs
assume HI: "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
have "algunos P ((a # xs) @ ys) = (P a ∨ algunos P (xs @ ys))" by simp
also have "... = (P a ∨ algunos P xs ∨ algunos P ys)" using HI by simp
also have "... = (algunos P (a # xs) ∨ algunos P ys)" by simp
finally show "algunos P ((a # xs) @ ys) = (algunos P (a # xs) ∨ algunos P ys)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 9.1. Demostrar o refutar automáticamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, juacorvic"
lemma "algunos P (rev xs) = algunos P xs"
by (induct xs) (auto simp add: algunos_append)
text {*
---------------------------------------------------------------------
Ejercicio 9.2. Demostrar o refutar detalladamente
algunos P (rev xs) = algunos P xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI:"algunos P (rev xs) = algunos P xs"
have "algunos P (rev (a # xs)) = algunos P (rev xs @[a])" by simp
also have "... = (algunos P xs ∨ (P a))" using HI using algunos_append by auto
finally show " algunos P (rev (a # xs)) = algunos P (a # xs)" by auto
qed
-- "emimarriv"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix x xs
assume HI: "algunos P (rev xs) = algunos P xs"
have "algunos P (rev (x#xs)) = algunos P ((rev xs)@[x])" by simp
also have "... = (algunos P (rev xs) ∨ (P x))" by (auto simp add: algunos_append)
also have "... = (algunos P xs ∨ (P x))" using HI by simp
finally show " algunos P (rev (x#xs)) = algunos P (x#xs)" by auto
qed
-- "juacorvic"
lemma "algunos P (rev xs) = algunos P xs"
proof (induct xs)
show "algunos P (rev []) = algunos P []" by simp
next
fix a xs
assume HI: "algunos P (rev xs) = algunos P xs"
have "algunos P (rev (a # xs)) = algunos P ((rev xs) @ [a])" by simp
also have "... = (algunos P (rev xs) ∨ algunos P [a])" by (simp add: algunos_append)
also have "... = (algunos P xs ∨ algunos P [a])" using HI by simp
also have "... = (algunos P [a] ∨ algunos P xs)" by arith
also have "... = algunos P (a # xs)" by simp
finally show "algunos P (rev (a # xs)) = algunos P (a # xs)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la
siguiente ecuación:
algunos (λx. P x ∨ Q x) xs = Z
y demostrar la equivalencia de forma automática y detallada.
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
by (induct xs) auto
--"jeshorcob"
lemma "algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
proof (induct xs)
show "algunos (λx. P x ∨ Q x) [] = (algunos P [] ∨ algunos Q [])" by simp
next
fix x xs
assume hi:"algunos (λx. P x ∨ Q x) xs = (algunos P xs ∨ algunos Q xs)"
have "algunos (λx. P x ∨ Q x) (x # xs) = ((P x ∨ Q x)
∨ algunos (λx. P x ∨ Q x) xs)" by simp
also have "... = ((P x ∨ Q x) ∨ (algunos P xs ∨ algunos Q xs))"
using hi by simp
also have "... = (P x ∨ algunos P xs ∨ Q x ∨ algunos Q xs)" by arith
finally show " algunos (λx. P x ∨ Q x) (x # xs) =
(algunos P (x # xs) ∨ algunos Q (x # xs))" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 11.1. Demostrar o refutar automáticamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}
(*Pedrosrei: Es falso.
Por ejemplo P= esVacio, xs = []. P es la propiedad de ser vacío
con nuestra construcción de algunos es cierto "algunos esVacio []"
Sin embargo, todos (λx. (¬ esVacio {})) [] es lo mismo que
todos _ [] = True, por lo que ¬(todos (λx. (¬ esVacio {})) []) = False,
siendo falsa nuestra definición. Podemos coger de todas maneras la propiedad
que queramos y sigue siendo falso porque
(algunos _ [] True) ∧ (¬(todos _ [])= False)
*)
lemma
shows "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
quickcheck
oops
(*Al corregir la definición de "algunos" deja de ser cierto lo dicho y
correcto lo de abajo.
*)
(*jeshorcob: está claro que el fallo en todo era la definición esa*)
-- "javrodviv1, jeshorcob, juacorvic"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 11.2. Demostrar o refutar datalladamente
algunos P xs = (¬ todos (λx. (¬ P x)) xs)
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show " algunos P [] = (¬ todos (λx. ¬ P x) [])" by simp
next
fix a xs
assume HI:"algunos P xs = (¬ todos (λx. ¬ P x) xs)"
have "algunos P (a # xs) = ((P a) ∨ algunos P xs)" by simp
also have "... = ((P a) ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
finally show "algunos P (a # xs) =(¬ todos (λx. ¬ P x) (a#xs))" by auto
qed
-- "juacorvic"
lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
proof (induct xs)
show "algunos P [] = (¬ todos (λx. ¬ P x) [])" by simp
next
fix a xs
assume HI: "algunos P xs = (¬ todos (λx. ¬ P x) xs)"
have "algunos P (a # xs) = (P a ∨ algunos P xs)" by simp
also have "... = (P a ∨ (¬ todos (λx. ¬ P x) xs))" using HI by simp
also have "... = (¬ todos (λx. ¬ P x) (a # xs))" by simp
(* Este paso lo he puesto por inercia de otras demostraciones
pero realmente no veo como hacerlo más detallado *)
finally show "algunos P (a # xs) = (¬ todos (λx. ¬ P x) (a # xs))" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 12. 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
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob"
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = False"
| "estaEn x (a#xs) = ((x=a) ∨ estaEn x xs)"
-- "juacorvic"
(*Si cambiamos el orden de la igualdad no tenemos que
utilizar auto en la demostración*)
fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
"estaEn x [] = 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"
text {*
---------------------------------------------------------------------
Ejercicio 13. Expresar la relación existente entre estaEn y algunos.
Demostrar dicha relación de forma automática y detallada.
---------------------------------------------------------------------
*}
--"jeshorcob,juacorvic"
lemma "algunos (λx. x=y) xs = estaEn y xs"
by (induct xs) auto
--"jeshorcob"
lemma "algunos (λx. x=y) xs = estaEn y xs" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix x xs
assume HI: "?P xs"
have "estaEn y (x#xs) = (y=x ∨ estaEn y xs)" by simp
also have "… = (y=x ∨ algunos (λx. (x=y)) xs)" using HI by simp
finally show "?P (x#xs)" by auto
qed
-- "juacorvic"
lemma "algunos (λx. x=y) xs = estaEn y xs"
proof (induct xs)
show "algunos (λx. x = y) [] = estaEn y []" by simp
next
fix a xs
assume HI: "algunos (λx. x = y) xs = estaEn y xs"
have "algunos (λx. x = y) (a # xs) = (a = y ∨ algunos (λx. x = y) xs)" by simp
also have "... = (a = y ∨ estaEn y xs)" using HI by simp
also have "... = (estaEn y (a # xs))" by simp
finally show "algunos (λx. x = y) (a # xs) = estaEn y (a # xs)" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 14. 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
---------------------------------------------------------------------
*}
-- "javrodviv1"
fun sinDuplicados :: "'a list ⇒ bool" where
"sinDuplicados [] = False"
| "sinDuplicados (x#xs) = (estaEn x xs ∨ sinDuplicados xs)"
(*jeshorcob: Esta definición no es correcta. Véanse:*)
value "sinDuplicados [1::nat,4,2]" -- "= True"
value "sinDuplicados [1::nat,4,2,4]" -- "= False"
--"jeshorcob, juacorvic"
fun sinDuplicados2 :: "'a list ⇒ bool" where
"sinDuplicados2 [] = True"
|"sinDuplicados2 (x#xs) = (¬(estaEn x xs) ∧ sinDuplicados2 xs)"
value "sinDuplicados2 [1::nat,4,2]" -- "= True"
value "sinDuplicados2 [1::nat,4,2,4]" -- "= False"
--"emimarriv"
fun sinDuplicados3 :: "'a list ⇒ bool" where
"sinDuplicados3 [] = True"
| "sinDuplicados3 (x#xs) = (if estaEn x xs then False else sinDuplicados3 xs )"
text {*
---------------------------------------------------------------------
Ejercicio 15. 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.
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, juacorvic"
fun borraDuplicados :: "'a list ⇒ 'a list" where
"borraDuplicados [] = []"
| "borraDuplicados (x#xs) = (if estaEn x xs then borraDuplicados xs else (x#(borraDuplicados xs)))"
text {*
---------------------------------------------------------------------
Ejercicio 16.1. Demostrar o refutar automáticamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob, juacorvic"
lemma "length (borraDuplicados xs) ≤ length xs"
by (induct xs) auto
text {*
---------------------------------------------------------------------
Ejercicio 16.2. Demostrar o refutar detalladamente
length (borraDuplicados xs) ≤ length xs
---------------------------------------------------------------------
*}
-- "javrodviv1, jeshorcob"
lemma length_borraDuplicados:
"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 "... = 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
-- "juacorvic"
(*Igual pero con 1 paso más*)
lemma length_borraDuplicados:
"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 "... ≤ 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
(*Nota: así conseguimos demostrar el caso de que el elemento 'a' no esté repetido
en la lista. Que pasa con la demostración para el caso de una lista cuyos los elementos
sean todos duplicados. Por ejemplo [1::1,1,1,1,1,1].
Esto no se reduce:
have "length (borraDuplicados (a # xs)) ≤ length (borraDuplicados xs)" by simp
*)
text {*
---------------------------------------------------------------------
Ejercicio 17.1. Demostrar o refutar automáticamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}
-- "javrodviv1, juacorvic"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
by (induct xs) auto
--"jeshorcob"
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
apply (induct xs, auto)
done
text {*
---------------------------------------------------------------------
Ejercicio 17.2. Demostrar o refutar detalladamente
estaEn a (borraDuplicados xs) = estaEn a xs
---------------------------------------------------------------------
*}
(*Pedrosrei: con esta definición de borraDuplicados es falso si cogemos
xs= []. Además del quickcheck, podemos hacer "apply (induct xs, auto)"
y ver que nos pide que demostremos False.
*)
lemma estaEn_borraDuplicados:
"estaEn a (borraDuplicados xs) = estaEn a xs"
oops
(*jeshorcob: dejo la prueba por inducción y casos*)
--"jeshorcob"
lemma estaEn_borraDuplicados:
"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 (cases)
assume a1:"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)" using a1 by auto
finally show ?thesis by simp
next
assume a2:"¬(estaEn x xs)"
then have "estaEn a (borraDuplicados (x#xs)) =
estaEn a (x#borraDuplicados xs)" by simp
also have "... = (a = x ∨ estaEn a (borraDuplicados xs))" by simp
finally show ?thesis using hi by simp
qed
qed
text {*
---------------------------------------------------------------------
Ejercicio 18.1. Demostrar o refutar automáticamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma "sinDuplicados2 (borraDuplicados xs)"
by (induct xs) (auto simp add: estaEn_borraDuplicados)
text {*
---------------------------------------------------------------------
Ejercicio 18.2. Demostrar o refutar detalladamente
sinDuplicados (borraDuplicados xs)
---------------------------------------------------------------------
*}
--"jeshorcob"
lemma sinDuplicados_borraDuplicados:
"sinDuplicados2 (borraDuplicados xs)"
proof (induct xs)
show "sinDuplicados2 (borraDuplicados [])" by simp
next
fix x::"'a"
fix xs::"'a list"
assume hi: "sinDuplicados2 (borraDuplicados xs)"
have "sinDuplicados2 (borraDuplicados (x#xs)) =
sinDuplicados2 ((if estaEn x xs then borraDuplicados xs
else x # borraDuplicados xs))" by simp
also have "... = (if estaEn x xs
then sinDuplicados2 (borraDuplicados xs)
else sinDuplicados2 (x#borraDuplicados xs))" by simp
also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs)
else (¬estaEn x (borraDuplicados xs)
∧ sinDuplicados2 (borraDuplicados xs)))" by simp
also have "...= (if estaEn x xs then sinDuplicados2 (borraDuplicados xs)
else (¬estaEn x xs ∧ sinDuplicados2 (borraDuplicados xs)))"
by (simp add: estaEn_borraDuplicados)
then show "sinDuplicados2 (borraDuplicados (x#xs))"
using hi by (simp add: estaEn_borraDuplicados)
qed
text {*
---------------------------------------------------------------------
Ejercicio 19. Demostrar o refutar:
borraDuplicados (rev xs) = rev (borraDuplicados xs)
---------------------------------------------------------------------
*}
(*Pedrosrei: es falso, como podemos ver si cogemos [1,2,1] y evaluamos:
*)
lemma "borraDuplicados' (rev xs) = rev (borraDuplicados' xs)"
quickcheck
oops
--"jeshorcob"
lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
quickcheck
oops
text {* Encuentra el contraejemplo
xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
borraDuplicados (rev xs) = [a⇩2, a⇩1]
rev (borraDuplicados xs) = [a⇩1, a⇩2]
*}
end