Razonamiento por casos y por inducci¢n
De Lógica matemática y fundamentos (2018-19)
Revisión del 10:22 2 may 2019 de Jalonso (discusión | contribuciones)
chapter {* Tema 7: Razonamiento por casos y por inducción *}
theory T7_Razonamiento_por_casos_y_por_induccion
imports Main HOL.Parity
begin
text {*
En este tema se amplían los métodos de demostración por casos y por
inducción iniciados en el tema anterior.
*}
section {* Razonamiento por distinción de casos *}
subsection {* Distinción de casos booleanos *}
text {*
Ejemplo de demostración por distinción de casos booleanos:
Demostrar "¬A ∨ A".
*}
― ‹La demostración aplicativa es›
lemma "¬A ∨ A"
apply cases (* 1. ?P ⟹ ¬ A ∨ A
2. ¬ ?P ⟹ ¬ A ∨ A *)
apply (erule disjI2) (* 1. ¬ A ⟹ ¬ A ∨ A *)
apply (erule disjI1) (* No subgoals! *)
done
― ‹La demostración semiautomática es›
lemma "¬A ∨ A"
apply cases (* 1. ?P ⟹ ¬ A ∨ A
2. ¬ ?P ⟹ ¬ A ∨ A *)
apply simp_all (* No subgoals! *)
done
― ‹La demostración automática es›
lemma "¬A ∨ A"
by simp
― ‹La demostración estructurada es›
lemma "¬A ∨ A"
proof cases
assume "A"
then show "¬A ∨ A" ..
next
assume "¬A"
then show "¬A ∨ A" ..
qed
text {*
Comentarios de la demostración anterior:
· "proof cases" indica que el método de demostración será por
distinción de casos.
· Se generan 2 casos:
1. ?P ⟹ ¬A ∨ A
2. ¬?P ⟹ ¬A ∨ A
donde ?P es una variable sobre las fórmulas.
· (assume "A") indica que se está usando "A" en lugar de la variable
?P.
· "then" indica usando la fórmula anterior.
· ".." indica usando la regla lógica necesaria (las reglas lógicas se
estudiarán en los siguientes temas).
· "next" indica el siguiente caso (se puede observar cómo ha
sustituido ¬?P por ¬A.
*}
text {*
Ejemplo de demostración por distinción de casos booleanos con nombres:
Demostrar "¬A ∨ A".
*}
― ‹La demostración aplicativa es›
lemma "¬A ∨ A"
apply (cases "A") (* 1. A ⟹ ¬ A ∨ A
2. ¬ A ⟹ ¬ A ∨ A *)
apply (erule disjI2) (* 1. ¬ A ⟹ ¬ A ∨ A *)
apply (erule disjI1) (* No subgoals! *)
done
― ‹La demostración semiautomática es›
lemma "¬A ∨ A"
apply (cases "A") (* 1. A ⟹ ¬ A ∨ A
2. ¬ A ⟹ ¬ A ∨ A *)
apply simp_all (* No subgoals! *)
done
― ‹La demostración automática es›
lemma "¬A ∨ A"
by simp
― ‹La demostración estructurada es›
lemma "¬A ∨ A"
proof (cases "A")
case True
then show "¬A ∨ A" ..
next
case False
thus "¬A ∨ A" ..
qed
text {*
Comentarios sobre la demostración anterior:
· (cases "A") indica que la demostración se hará por casos según los
distintos valores de "A".
· Como "A" es una fórmula, sus posibles valores son verdadero o falso.
· "case True" indica que se está suponiendo que A es verdadera. Es
equivalente a "assume A".
· "case False" indica que se está suponiendo que A es falsa. Es
equivalente a "assume ¬A".
· En general,
· el método (cases F) es una abreviatura de la aplicación de la regla
⟦F ⟹ Q; ¬F ⟹ Q⟧ ⟹ Q
· La expresión "case True" es una abreviatura de F.
· La expresión "case False" es una abreviatura de ¬F.
· Ventajas de "cases" con nombre:
· reduce la escritura de la fórmula y
· es independiente del orden de los casos.
*}
subsection {* Distinción de casos sobre otros tipos de datos *}
text {*
Ejemplo de distinción de casos sobre listas:
Demostrar que la longitud del resto de una lista es la longitud de la
lista menos 1.
*}
― ‹La demostración aplicativa es›
lemma "length (tl xs) = length xs - 1"
apply (cases xs)
(* 1. xs = [] ⟹ length (tl xs) = length xs - 1
2. ⋀a list. xs = a # list ⟹
length (tl xs) = length xs - 1*)
apply simp_all
(* No subgoals! *)
done
― ‹La demostración semiautomática es›
lemma "length (tl xs) = length xs - 1"
by (cases xs) simp_all
― ‹La demostración automática es›
lemma "length (tl xs) = length xs - 1"
by auto
― ‹La demostración detallada es›
lemma "length (tl xs) = length xs - 1"
proof (cases xs)
assume "xs = []"
then show "length (tl xs) = length xs - 1" by simp
next
fix y ys
assume "xs = y#ys"
then show "length(tl xs) = length xs - 1" by simp
qed
text {*
Comentarios sobre la demostración anterior:
· "(cases xs)" indica que la demostración se hará por casos sobre los
posibles valores de xs.
· Como xs es una lista, sus posibles valores son la lista vacía ([]) o
una lista no vacía (de la forma (y#ys)).
· Se generan 2 casos:
1. xs = [] ⟹ length (tl xs) = length xs - 1
2. ⋀a list. xs = a # list ⟹ length (tl xs) = length xs - 1
*}
― ‹La demostración simplificada es›
lemma "length (tl xs) = length xs - 1"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case Cons
then show ?thesis by simp
qed
text {*
Comentarios sobre la demostración anterior:
· "case Nil" es una abreviatura de
"assume xs =[]".
· "case Cons" es una abreviatura de
"fix y ys assume xs = y#ys"
· ?thesis es una abreviatura de la conclusión del lema.
*}
text {*
En el siguiente ejemplo vamos a demostrar una propiedad de la función
drop que está definida en la teoría List de forma que (drop n xs) la
lista obtenida eliminando en xs} los n primeros elementos. Su
definición es la siguiente
drop_Nil: "drop n [] = []"
drop_Cons: "drop n (x#xs) = (case n of
0 => x#xs |
Suc(m) => drop m xs)"
*}
text {*
Ejemplo de análisis de casos:
Demostrar que el resultado de eliminar los n+1 primeros elementos de
xs es el mismo que eliminar los n primeros elementos del resto de xs.
*}
― ‹La demostración aplicativa es›
lemma "drop (n + 1) xs = drop n (tl xs)"
apply (cases xs)
(* 1. xs = [] ⟹ drop (n + 1) xs = drop n (tl xs)
2. ⋀a list. xs = a # list ⟹
drop (n + 1) xs = drop n (tl xs) *)
apply simp_all
(* No subgoals! *)
done
― ‹La demostración automática es›
lemma "drop (n + 1) xs = drop n (tl xs)"
by (cases xs) auto
― ‹La demostración detallada es›
lemma "drop (n + 1) xs = drop n (tl xs)"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case Cons
then show ?thesis by simp
qed
section {* Inducción matemática *}
text {*
[Principio de inducción matemática]
Para demostrar una propiedad P para todos los números naturales basta
probar que el 0 tiene la propiedad P y que si n tiene la propiedad P,
entonces n+1 también la tiene.
⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m
En Isabelle el principio de inducción matemática está formalizado en
el teorema nat.induct y puede verse con
thm nat.induct
*}
text {*
Ejemplo de demostración por inducción: Usaremos el principio de
inducción matemática para demostrar que
1 + 3 + ... + (2n-1) = n^2
Definición. [Suma de los primeros impares]
(suma_impares n) la suma de los n números impares. Por ejemplo,
suma_impares 3 = 9
*}
fun suma_impares :: "nat ⇒ nat" where
"suma_impares 0 = 0"
| "suma_impares (Suc n) = (2*(Suc n) - 1) + suma_impares n"
value "suma_impares 3"
text {*
Ejemplo de demostración por inducción matemática:
Demostrar que la suma de los n primeros números impares es n^2.
*}
― ‹La demostración aplicativa es›
lemma "suma_impares n = n * n"
apply (induct n)
(* 1. suma_impares 0 = 0 * 0
2. ⋀n. suma_impares n = n * n ⟹
suma_impares (Suc n) = Suc n * Suc n*)
apply simp_all
(* No subgoals! *)
done
― ‹La demostración automática es›
lemma "suma_impares n = n * n"
by (induct n) simp_all
― ‹Demostración del lema anterior por inducción y razonamiento
ecuacional›
lemma "suma_impares n = n * n"
proof (induct n)
show "suma_impares 0 = 0 * 0" by simp
next
fix n assume HI: "suma_impares n = n * n"
have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n"
by simp
also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
also have "… = n * n + 2 * n + 1" by simp
finally show "suma_impares (Suc n) = (Suc n) * (Suc n)" by simp
qed
― ‹Demostración del lema anterior con patrones y razonamiento
ecuacional›
lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n
assume HI: "?P n"
have "suma_impares (Suc n) = (2 * (Suc n) - 1) + suma_impares n"
by simp
also have "… = (2 * (Suc n) - 1) + n * n" using HI by simp
also have "… = n * n + 2 * n + 1" by simp
finally show "?P (Suc n)" by simp
qed
text {*
Comentario sobre la demostración anterior:
· Con la expresión
"suma_impares n = n * n" (is "?P n")
se abrevia "suma_impares n = n * n" como "?P n". Por tanto,
"?P 0" es una abreviatura de "suma_impares 0 = 0 * 0"
"?P (Suc n)" es una abreviatura de "suma_impares (Suc n) =
(Suc n) * (Suc n)"
· En general, cualquier fórmula seguida de (is patrón) equipara el
patrón con la fórmula.
*}
― ‹La demostración usando patrones es›
lemma "suma_impares n = n * n" (is "?P n")
proof (induct n)
show "?P 0" by simp
next
fix n
assume "?P n"
then show "?P (Suc n)" by simp
qed
text {*
Ejemplo de definición con existenciales.
Un número natural n es par si existe un natural m tal que n=m+m.
*}
definition par :: "nat ⇒ bool" where
"par n ≡ ∃m. n=m+m"
text {*
Ejemplo de inducción y existenciales:
Demostrar que para todo número natural n, se verifica que n*(n+1) par.
*}
― ‹Demostración aplicativa›
lemma
shows "par (n*(n+1))"
apply (induct n)
(* par (0 * (0 + 1))
⋀n. par (n * (n + 1)) ⟹ par (Suc n * (Suc n + 1)) *)
apply (simp add: par_def)
(* ⋀n. par (n * (n + 1)) ⟹ par (Suc n * (Suc n + 1)) *)
apply (simp add: par_def)
(* ⋀n. ∃m. n + n * n = m + m ⟹
∃m. Suc (Suc (n + (n + (n + n * n)))) = m + m *)
apply (erule exE)
(* ⋀n m. n + n * n = m + m ⟹
∃m. Suc (Suc (n + (n + (n + n * n)))) = m + m*)
apply (rule_tac x="m+n+1" in exI)
(* ⋀n m. n + n * n = m + m ⟹
Suc (Suc (n + (n + (n + n * n)))) =
m + n + 1 + (m + n + 1)*)
apply simp
(* *)
done
― ‹Demostración aplicativa con arith›
lemma
shows "par (n*(n+1))"
apply (induct n)
(* par (0 * (0 + 1))
⋀n. par (n * (n + 1)) ⟹ par (Suc n * (Suc n + 1)) *)
apply (simp add: par_def)
(* ⋀n. par (n * (n + 1)) ⟹ par (Suc n * (Suc n + 1)) *)
apply (simp add: par_def)
(* ⋀n. ∃m. n + n * n = m + m ⟹
∃m. Suc (Suc (n + (n + (n + n * n)))) = m + m *)
apply arith
(* *)
done
― ‹Demostración automática›
lemma
fixes n :: "nat"
shows "par (n*(n+1))"
by (induct n) (auto simp add: par_def, arith)
― ‹Demostración declarativa›
lemma
fixes n :: "nat"
shows "par (n*(n+1))"
proof (induct n)
show "par (0*(0+1))" by (simp add: par_def)
next
fix n
assume "par (n*(n+1))"
then have "∃m. n*(n+1) = m+m" by (simp add:par_def)
then obtain m where m: "n*(n+1) = m+m" ..
then have "(Suc n)*((Suc n)+1) = (m+n+1)+(m+n+1)" by auto
then have "∃m. (Suc n)*((Suc n)+1) = m+m" ..
then show "par ((Suc n)*((Suc n)+1))" by (simp add:par_def)
qed
text {*
Comentarios sobre la demostración anterior:
· (fixes n :: "nat") es una abreviatura de "sea n un número natural".
*}
text {*
En Isabelle puede demostrarse de manera más simple un lema equivalente
usando en lugar de la función "par" la función "even" definida en la
teoría Parity por
even x ⟷ x mod 2 = 0"
*}
lemma
fixes n :: "nat"
shows "even (n*(n+1))"
by auto
text {*
Comentarios sobre la demostración anterior:
· Para poder usar la función "even" de la librería Parity es necesario
importar dicha librería. Por ello, antes del inicio de la teoría
aparece
imports Main HOL.Parity
*}
text {*
Para completar la demostración basta demostrar la equivalencia de las
funciones "par" y "even".
*}
― ‹Demostración aplicativa›
lemma
shows "par n = even n"
apply (simp add: par_def) (* (∃m. n = m + m) = even n *)
apply presburger (* *)
done
― ‹Demostración automática›
lemma
shows "par n = even n"
by (simp add: par_def, presburger)
― ‹Demostración declarativa›
lemma
fixes n :: "nat"
shows "par n = even n"
proof -
have "par n = (∃m. n = m+m)" by (simp add:par_def)
then show "par n = even n" by presburger
qed
text {*
Comentarios sobre la demostración anterior:
· "by presburger" indica que se use como método de demostración el
algoritmo de decisión de la aritmética de Presburger.
*}
section {* Inducción estructural *}
text {*
Inducción estructural:
· En Isabelle puede hacerse inducción estructural sobre cualquier tipo
recursivo.
· La inducción matemática es la inducción estructural sobre el tipo de
los naturales.
· El esquema de inducción estructural sobre listas es
· list.induct: ⟦P []; ⋀x ys. P ys ⟹ P (x # ys)⟧ ⟹ P zs
· Para demostrar una propiedad para todas las listas basta demostrar
que la lista vacía tiene la propiedad y que al añadir un elemento a una
lista que tiene la propiedad se obtiene una lista que también tiene la
propiedad.
· En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct que puede verse con
thm list.induct
*}
text {*
Concatenación de listas:
En la teoría List.thy está definida la concatenación de listas (que
se representa por @) como sigue
append_Nil: "[]@ys = ys"
append_Cons: "(x#xs)@ys = x#(xs@ys)"
*}
text {*
Lema. [Ejemplo de inducción sobre listas]
Demostrar que la concatenación de listas es asociativa.
*}
― ‹La demostración automática es›
lemma conc_asociativa: "xs @ (ys @ zs) = (xs @ ys) @ zs"
apply (induct xs)
(* 1. [] @ (ys @ zs) = ([] @ ys) @ zs
2. ⋀a xs. xs @ (ys @ zs) = (xs @ ys) @ zs ⟹
(a # xs) @ (ys @ zs) = ((a # xs) @ ys) @ zs*)
apply simp_all
(* *)
done
― ‹La demostración automática es›
lemma conc_asociativa_2: "xs @ (ys @ zs) = (xs @ ys) @ zs"
by (induct xs) simp_all
― ‹La demostración estructurada es›
lemma conc_asociativa_3: "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
show "[] @ (ys @ zs) = ([] @ ys) @ zs"
proof -
have "[] @ (ys @ zs) = ys @ zs" by simp
also have "… = ([] @ ys) @ zs" by simp
finally show ?thesis .
qed
next
fix x xs
assume HI: "xs @ (ys @ zs) = (xs @ ys) @ zs"
show "(x#xs) @ (ys @ zs) = ((x#xs) @ ys) @ zs"
proof -
have "(x#xs) @ (ys @ zs) = x#(xs @ (ys @ zs))" by simp
also have "… = x#((xs @ ys) @ zs)" using HI by simp
also have "… = (x#(xs @ ys)) @ zs" by simp
also have "… = ((x#xs) @ ys) @ zs" by simp
finally show ?thesis .
qed
qed
section {* Recursión general. La función de Ackermann *}
text {*
El objetivo de esta sección es mostrar el uso de las definiciones
recursivas generales y sus esquemas de inducción. Como ejemplo se usa la
función de Ackermann (se puede consultar información sobre dicha función en
http://en.wikipedia.org/wiki/Ackermann_function).
Definición. La función de Ackermann se define por
A(m,n) = n+1, si m=0,
A(m-1,1), si m>0 y n=0,
A(m-1,A(m,n-1)), si m>0 y n>0
para todo los números naturales.
La función de Ackermann es recursiva, pero no es primitiva recursiva.
*}
fun ack :: "nat ⇒ nat ⇒ nat" where
"ack 0 n = n+1"
| "ack (Suc m) 0 = ack m 1"
| "ack (Suc m) (Suc n) = ack m (ack (Suc m) n)"
― ‹Ejemplo de evaluación›
value "ack 2 3" (* devuelve 9 *)
text {*
Esquema de inducción correspondiente a una función:
· Al definir una función recursiva general se genera una regla de
inducción. En la definición anterior, la regla generada es
ack.induct:
⟦⋀n. P 0 n;
⋀m. P m 1 ⟹ P (Suc m) 0;
⋀m n. ⟦P (Suc m) n; P m (ack (Suc m) n)⟧ ⟹ P (Suc m) (Suc n)⟧
⟹ P a b
*}
text {*
Ejemplo de demostración por la inducción correspondiente a una función:
Demostrar que para todos m y n, A(m,n) > n.
*}
― ‹Demostración aplicativa›
lemma "ack m n > n"
apply (induct m n rule: ack.induct)
(* 1. ⋀n. n < ack 0 n
2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0
3. ⋀m n. ⟦n < ack (Suc m) n;
ack (Suc m) n < ack m (ack (Suc m) n)⟧
⟹ Suc n < ack (Suc m) (Suc n) *)
apply simp_all
done
― ‹Demostración automática›
lemma "ack m n > n"
by (induct m n rule: ack.induct) simp_all
― ‹Demostración declarativa›
lemma "ack m n > n"
proof (induct m n rule: ack.induct)
fix n
show "ack 0 n > n" by simp
next
fix m
assume "ack m 1 > 1"
then show "ack (Suc m) 0 > 0" by simp
next
fix m n
assume "n < ack (Suc m) n" and
"ack (Suc m) n < ack m (ack (Suc m) n)"
then show "Suc n < ack (Suc m) (Suc n)" by simp
qed
text {*
Comentarios sobre la demostración anterior:
· (induct m n rule: ack.induct) indica que el método de demostración
es el esquema de recursión correspondiente a la definición de
(ack m n).
· Se generan 3 casos:
1. ⋀n. n < ack 0 n
2. ⋀m. 1 < ack m 1 ⟹ 0 < ack (Suc m) 0
3. ⋀m n. ⟦n < ack (Suc m) n;
ack (Suc m) n < ack m (ack (Suc m) n)⟧
⟹ Suc n < ack (Suc m) (Suc n)
*}
end