Examen 4
De Lógica matemática y fundamentos (2018-19)
Revisión del 13:13 11 sep 2019 de Jalonso (discusión | contribuciones)
text ‹Examen de Lógica Matemática y Fundamentos (10 septiembre 2019)›
theory examen_4_10_sep_sol
imports Main
begin
text ‹Nota: En las demostraciones se pueden las reglas básicas de
deducción natural de la lógica proposicional, de los cuantificadores
y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_middle: (¬P ∨ P)
· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ c = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
También se pueden usar las reglas notnotI y mt que demostramos a
continuación.
›
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
text ‹-----------------------------------------------------------------
Ejercicio 1. (2.5 puntos) Demostrar detalladamente que la siguiente
fórmula es una tautología:
((p ⟶ r) ∨ (q ⟶ s)) ⟶ ((p ∧ q) ⟶ (r ∨ s))
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
--------------------------------------------------------------------›
(* Demostración aplicativa *)
lemma "((p ⟶ r) ∨ (q ⟶ s)) ⟶ ((p ∧ q) ⟶ (r ∨ s))"
proof
assume 1: "(p ⟶ r) ∨ (q ⟶ s)"
show "(p ∧ q) ⟶ (r ∨ s)"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
have "q" using `p ∧ q` by (rule conjunct2)
note 1
then show "r ∨ s"
proof
assume "p ⟶ r"
then have "r" using `p` by (rule mp)
then show "r ∨ s" by (rule disjI1)
next
assume "q ⟶ s"
then have "s" using `q` by (rule mp)
then show "r ∨ s" by (rule disjI2)
qed
qed
qed
(* Demostración aplicativa. *)
lemma "((p ⟶ r) ∨ (q ⟶ s)) ⟶ ((p ∧ q) ⟶ (r ∨ s))"
apply (rule impI)+
apply (erule disjE)
apply (rule disjI1)
apply (erule mp)
apply (erule conjunct1)
apply (rule disjI2)
apply (erule mp)
apply (erule conjunct2)
done
text ‹-----------------------------------------------------------------
Ejercicio 2. (2.5 puntos) Demostrar por deducción natural que la
fórmula ∀x. (∃y. ((P(x,y) ∨ Q(x,x)))) es consecuencia
lógica de ∀x. (P(x,x) ∨ ∀y. Q(x,y)).
Nota: No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis
--------------------------------------------------------------------›
(* Demostración declarativa. *)
lemma
assumes "∀x. (P(x,x) ∨ (∀y. Q(x,y)))"
shows "∀x. (∃y. (P(x,y) ∨ Q(x,x)))"
proof
fix a
have "P(a,a) ∨ (∀y. Q(a,y))" using assms by (rule allE)
then show "∃y. (P(a,y) ∨ Q(a,a))"
proof
assume "P(a,a)"
then have "P(a,a) ∨ Q(a,a)" by (rule disjI1)
then show "∃y. (P(a,y) ∨ Q(a,a))" by (rule exI)
next
assume "∀y. Q(a,y)"
then have "Q(a,a)" by (rule allE)
then have "P(a,a) ∨ Q(a,a)" by (rule disjI2)
then show "∃y. (P(a,y) ∨ Q(a,a))" by (rule exI)
qed
qed
(* Demostración aplicativa. *)
lemma "⟦∀x. (P(x,x) ∨ (∀y. Q(x,y)))⟧ ⟹ ∀x. (∃y. (P(x,y) ∨ Q(x,x)))"
apply (rule allI)
apply (erule_tac x = x in allE)
apply (erule disjE)
apply (rule_tac x = x in exI)
apply (rule disjI1, simp)
apply (erule_tac x = x in allE)
apply (rule_tac x = x in exI)
apply (rule disjI2, simp)
done
text ‹-----------------------------------------------------------------
Ejercicio 3 (2.5 puntos) Consideremos el árbol binario
definido por
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
Por ejemplo, el árbol
e
/ \
/ \
c g
/ \ / \
se representa por "N e (N c H H) (N g H H)".
Se define las funciones
fun nNodos :: "'a arbol ⇒ nat" where
"nNodos H = 0"
| "nNodos (N x i d) = 1 + nNodos i + nNodos d"
fun nNodosAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nNodosAaux H n = n"
| "nNodosAaux (N x i d) n = 1 + nNodosAaux i (nNodosAaux d n)"
definition nNodosA :: "'a arbol ⇒ nat" where
"nNodosA a ≡ nNodosAaux a 0"
tales que
+ (nNodos a) es el número de nodos del árbol a. Por ejemplo,
nNodos (N e (N c H H) (N g H H)) = 3
+ (nNodosAA a) es el número de nodos del árbol a, calculado
con la función auxiliar nNodosAaux que usa un acumulador. Por
ejemplo,
nNodosA (N e (N c H H) (N g H H)) = 3
Demostrar estructuradamente (es decir, mediante una demostración
declarativa) que las funciones nNodos y nNodosA son equivalentes;
es decir,
nNodosA a = nNodos a
Notas:
1. Los únicos métodos que se pueden usar son induct, (simp only: ...)
y this.
2. En las demostraciones por introducción del cuantificador universal
hay que explicitar el tipo de las variables introducidas con fix.
Por ejemplo, en lugar de
fix x t n
hay que escribir
fix x :: 'a and t :: "'a arbol" and and n :: nat
-------------------------------------------------------------------›
datatype 'a arbol = H
| N "'a" "'a arbol" "'a arbol"
fun nNodos :: "'a arbol ⇒ nat" where
"nNodos H = 0"
| "nNodos (N x i d) = 1 + nNodos i + nNodos d"
fun nNodosAaux :: "'a arbol ⇒ nat ⇒ nat" where
"nNodosAaux H n = n"
| "nNodosAaux (N x i d) n = 1 + nNodosAaux i (nNodosAaux d n)"
definition nNodosA :: "'a arbol ⇒ nat" where
"nNodosA a ≡ nNodosAaux a 0"
value "nNodos (N e (N c H H) (N g H H)) = 3"
value "nNodosA (N e (N c H H) (N g H H)) = 3"
(* Demostración declarativa. *)
lemma nNodosA:
"nNodosAaux a n = (nNodos a) + n"
proof (induct a arbitrary: n)
fix n
have "nNodosAaux H n = n" by (simp only: nNodosAaux.simps(1))
also have "… = nNodos H + n" by (simp only: nNodos.simps(1))
finally show "nNodosAaux H n = nNodos H + n" by this
next
fix x :: 'a and
i :: "'a arbol" and
d :: "'a arbol" and
n :: nat
assume HI1: "⋀n. nNodosAaux i n = nNodos i + n"
and HI2: "⋀n. nNodosAaux d n = nNodos d + n"
have "nNodosAaux (N x i d) n = 1 + nNodosAaux i (nNodosAaux d n)"
by (simp only: nNodosAaux.simps(2))
also have "… = 1 + nNodosAaux i (nNodos d + n)"
by (simp only: HI2)
also have "… = 1 + nNodos i + (nNodos d + n)"
by (simp only: HI1)
also have "… = nNodos (N x i d) + n"
by (simp only: nNodos.simps(2))
finally show "nNodosAaux (N x i d) n = nNodos (N x i d) + n"
by this
qed
(* Demostración aplicativa del lema anterior *)
lemma "nNodosAaux a n = (nNodos a) + n"
apply (induct a arbitrary: n)
apply (simp only: nNodosAaux.simps(1))
apply (simp only: nNodos.simps(1))
apply (simp only: nNodosAaux.simps(2))
apply (simp only: nNodos.simps(2))
done
lemma "nNodosA a = nNodos a"
proof -
have "nNodosA a = nNodosAaux a 0" by (simp only: nNodosA_def)
also have "… = (nNodos a)" by (simp only: nNodosA)
finally show "nNodosA a = nNodos a" by this
qed
text ‹---------------------------------------------------------------
Ejercicio 4. (2.5 puntos) Demostrar que si en un grupo se cumple la siguente
propiedad cancelativa
∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = z
entonces el grupo es abeliano.
Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
fast, arith o metis
Nota: Los únicos métodos que se pueden usar son (simp only: ...) o
rule.
------------------------------------------------------------------›
locale grupo =
fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
and neutro ("𝟭")
and inverso ("_^" [100] 100)
assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
and neutro_i: "𝟭 ⋅ x = x"
and neutro_d: "x ⋅ 𝟭 = x"
and inverso_i: "x^ ⋅ x = 𝟭"
(* Notas sobre notación:
* El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos).
* El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
* El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)
context grupo
begin
(* Demostración declarativa. *)
lemma
assumes "∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = z"
shows "∀x. ∀y. x ⋅ y = y ⋅ x"
proof (rule allI)+
fix a b
have "b ⋅ (a ⋅ b) = (b ⋅ a) ⋅ b ⟶ a ⋅ b = b ⋅ a"
proof -
have "∀y. ∀z. b ⋅ y = z ⋅ b ⟶ y = z" using assms by (rule allE)
then have "∀z. b ⋅ (a ⋅ b) = z ⋅ b ⟶ a ⋅ b = z" by (rule allE)
then show "b ⋅ (a ⋅ b) = (b ⋅ a) ⋅ b ⟶ a ⋅ b = b ⋅ a" by (rule allE)
qed
moreover
have "b ⋅ (a ⋅ b) = (b ⋅ a) ⋅ b" by (simp only: asociativa)
ultimately show "a ⋅ b = b ⋅ a" by (rule mp)
qed
(* Demostración aplicativa. *)
lemma
"⟦∀x. ∀y. ∀z. x ⋅ y = z ⋅ x ⟶ y = z⟧ ⟹
∀x. ∀y. x ⋅ y = y ⋅ x"
apply (rule allI)+
apply (erule_tac x = y in allE)
apply (erule_tac x = "x ⋅ y" in allE)
apply (erule_tac x = "y ⋅ x" in allE)
apply (erule mp)
apply (simp add: asociativa)
done
end
end