Diferencia entre revisiones de «Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL»
De Razonamiento automático (2018-19)
(Página creada con «<source lang="isabelle"> chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *} theory R2_Razonamiento_automatico_sobre_programas imports Main begin declare na…») |
m (Protegió «Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))) |
||
(No se muestran 2 ediciones intermedias del mismo usuario) | |||
Línea 1: | Línea 1: | ||
<source lang="isabelle"> | <source lang="isabelle"> | ||
− | chapter {* | + | chapter {* Tema 3: Razonamiento estructurado sobre programas *} |
− | theory | + | theory T3_Razonamiento_sobre_programas |
imports Main | imports Main | ||
begin | begin | ||
+ | |||
+ | text {* | ||
+ | En este tema se demuestra con Isabelle las propiedades de los | ||
+ | programas funcionales como se expone en el tema 2a y se demostraron | ||
+ | automáticamente en el tema 2b. A diferencia del tema 2b, ahora | ||
+ | nos fijamos no sólo en el método de demostración sino en la estructura | ||
+ | de la prueba resaltando su semejanza con las del tema 2a. *} | ||
declare [[names_short]] | declare [[names_short]] | ||
+ | |||
+ | section {* Razonamiento ecuacional *} | ||
+ | |||
+ | text {* ---------------------------------------------------------------- | ||
+ | Ejemplo 1. Definir, por recursión, la función | ||
+ | longitud :: 'a list ⇒ nat | ||
+ | tal que (longitud xs) es la longitud de la listas xs. Por ejemplo, | ||
+ | longitud [a,c,d] = 3 | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | fun longitud :: "'a list ⇒ nat" where | ||
+ | "longitud [] = 0" | ||
+ | | "longitud (x#xs) = 1 + longitud xs" | ||
+ | |||
+ | value "longitud [a,c,d] = 3" | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 2. Demostrar que | |
− | + | longitud [a,c,d] = 3 | |
− | tal que ( | + | ------------------------------------------------------------------- *} |
− | + | ||
− | + | lemma "longitud [a,c,d] = 3" | |
+ | by simp | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 3. Definir la función | ||
+ | fun intercambia :: 'a × 'b ⇒ 'b × 'a | ||
+ | tal que (intercambia p) es el par obtenido intercambiando las | ||
+ | componentes del par p. Por ejemplo, | ||
+ | intercambia (u,v) = (v,u) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | + | fun intercambia :: "'a × 'b ⇒ 'b × 'a" where | |
− | fun | + | "intercambia (x,y) = (y,x)" |
− | " | ||
− | |||
− | + | value "intercambia (u,v) = (v,u)" | |
− | |||
− | |||
− | |||
− | + | text {* | |
− | + | La definición de la función intercambia genera una regla de | |
− | + | simplificación | |
+ | · intercambia.simps: intercambia (x,y) = (y,x) | ||
+ | |||
+ | Se puede ver con | ||
+ | · thm intercambia.simps | ||
+ | *} | ||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 4. (p.6) Demostrar que | ||
+ | intercambia (intercambia (x,y)) = (x,y) | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* Demostración aplicativa *) | ||
+ | lemma "intercambia (intercambia (x,y)) = (x,y)" | ||
+ | apply (simp only: intercambia.simps) | ||
+ | done | ||
+ | |||
+ | (* Demostración declarativa *) | ||
+ | lemma "intercambia (intercambia (x,y)) = (x,y)" | ||
+ | proof - | ||
+ | have "intercambia (intercambia (x,y)) = intercambia (y,x)" | ||
+ | by (simp only: intercambia.simps) | ||
+ | also have "... = (x,y)" | ||
+ | by (simp only: intercambia.simps) | ||
+ | finally show "intercambia (intercambia (x,y)) = (x,y)" | ||
+ | by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Notas sobre el lenguaje: En la demostración anterior se ha usado | ||
+ | · "proof" para iniciar la prueba, | ||
+ | · "-" (después de "proof") para no usar el método por defecto, | ||
+ | · "have" para establecer un paso, | ||
+ | · "by (simp only: intercambia.simps)" para indicar que sólo se usa | ||
+ | como regla de escritura la correspondiente a la definición de | ||
+ | intercambia, | ||
+ | · "also" para encadenar pasos ecuacionales, | ||
+ | · "..." para representar la derecha de la igualdad anterior en un | ||
+ | razonamiento ecuacional, | ||
+ | · "finally" para indicar el último pasa de un razonamiento ecuacional, | ||
+ | · "show" para establecer la conclusión. | ||
+ | · "by simp" para indicar el método de demostración por simplificación y | ||
+ | · "qed" para terminar la pruebas, | ||
+ | *} | ||
+ | |||
+ | (* Demostración declarativa simplificada *) | ||
+ | lemma "intercambia (intercambia (x,y)) = (x,y)" | ||
+ | proof - | ||
+ | have "intercambia (intercambia (x,y)) = intercambia (y,x)" by simp | ||
+ | also have "... = (x,y)" by simp | ||
+ | finally show "intercambia (intercambia (x,y)) = (x,y)" by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Nota: La diferencia entre las dos demostraciones es que en los dos | ||
+ | primeros pasos no se explicita la regla de simplificación. | ||
+ | *} | ||
+ | |||
+ | (* Demostración automática *) | ||
+ | lemma "intercambia (intercambia (x,y)) = (x,y)" | ||
+ | by simp | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 5. Definir, por recursión, la función | ||
+ | inversa :: 'a list ⇒ 'a list | ||
+ | tal que (inversa xs) es la lista obtenida invirtiendo el orden de los | ||
+ | elementos de xs. Por ejemplo, | ||
+ | inversa [a,d,c] = [c,d,a] | ||
+ | ------------------------------------------------------------------ *} | ||
+ | |||
+ | fun inversa :: "'a list ⇒ 'a list" where | ||
+ | "inversa [] = []" | ||
+ | | "inversa (x#xs) = inversa xs @ [x]" | ||
+ | |||
+ | value "inversa [a,d,c] = [c,d,a]" | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 6. (p. 9) Demostrar que | |
− | + | inversa [x] = [x] | |
------------------------------------------------------------------- *} | ------------------------------------------------------------------- *} | ||
− | (* | + | (* La demostración aplicativa es *) |
− | lemma " | + | lemma "inversa [x] = [x]" |
− | apply | + | apply simp |
− | |||
done | done | ||
− | (* | + | text {* |
− | lemma " | + | En la demostración anterior se usaron las siguientes reglas: |
− | apply( | + | · inversa.simps(1): inversa [] = [] |
− | + | · inversa.simps(2): inversa (x#xs) = inversa xs @ [x] | |
− | apply simp | + | · append_Nil: [] @ ys = ys |
+ | Vamos a explicitar su aplicación. | ||
+ | *} | ||
+ | |||
+ | (* La demostración aplicativa detallada es *) | ||
+ | lemma "inversa [x] = [x]" | ||
+ | apply (simp only: inversa.simps(2)) | ||
+ | apply (simp only: inversa.simps(1)) | ||
+ | apply (simp only: append_Nil) | ||
done | done | ||
− | (* | + | (* La demostración declarativa es *) |
− | lemma " | + | lemma "inversa [x] = [x]" |
− | by ( | + | proof - |
+ | have "inversa [x] = inversa (x#[])" by simp | ||
+ | also have "... = (inversa []) @ [x]" by (simp only: inversa.simps(2)) | ||
+ | also have "... = [] @ [x]" by (simp only: inversa.simps(1)) | ||
+ | also have "... = [x]" by (simp only: append_Nil) | ||
+ | finally show "inversa [x] = [x]" by simp | ||
+ | qed | ||
− | (* | + | (* La demostración declarativa simplificada es *) |
− | lemma " | + | lemma "inversa [x] = [x]" |
− | by ( | + | proof - |
+ | have "inversa [x] = inversa (x#[])" by simp | ||
+ | also have "... = (inversa []) @ [x]" by simp | ||
+ | also have "... = [] @ [x]" by simp | ||
+ | also have "... = [x]" by simp | ||
+ | finally show "inversa [x] = [x]" by simp | ||
+ | qed | ||
+ | (* La demostración automática es *) | ||
+ | lemma "inversa [x] = [x]" | ||
+ | by simp | ||
+ | |||
+ | section {* Razonamiento por inducción sobre los naturales *} | ||
+ | |||
+ | text {* | ||
+ | [Principio de inducción sobre los naturales] 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 sobre los naturales está | ||
+ | formalizado en el teorema nat.induct y puede verse con | ||
+ | thm nat.induct | ||
+ | *} | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 7. Definir la función | |
− | + | repite :: nat ⇒ 'a ⇒ 'a list | |
− | tal que | + | tal que (repite n x) es la lista formada por n copias del elemento |
− | + | x. Por ejemplo, | |
− | Por ejemplo, | + | repite 3 a = [a,a,a] |
− | |||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | + | fun repite :: "nat ⇒ 'a ⇒ 'a list" where | |
− | fun | + | "repite 0 x = []" |
− | " | + | | "repite (Suc n) x = x # (repite n x)" |
− | |||
− | |||
− | |||
− | |||
− | |||
− | |||
− | + | value "repite 3 a = [a,a,a]" | |
− | |||
− | |||
− | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 8. (p. 18) Demostrar que | |
− | + | longitud (repite n x) = n | |
------------------------------------------------------------------- *} | ------------------------------------------------------------------- *} | ||
− | (* | + | (* La demostración aplicativa es *) |
− | lemma " | + | lemma "longitud (repite n x) = n" |
− | apply( | + | apply (induct n) |
− | apply | + | apply simp_all |
done | done | ||
− | (* | + | (* La demostración estructurada es *) |
− | lemma " | + | lemma "longitud (repite n x) = n" |
− | + | proof (induct n) | |
+ | show "longitud (repite 0 x) = 0" by simp | ||
+ | next | ||
+ | fix n | ||
+ | assume HI: "longitud (repite n x) = n" | ||
+ | have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" | ||
+ | by simp | ||
+ | also have "... = 1 + longitud (repite n x)" by simp | ||
+ | also have "... = 1 + n" using HI by simp | ||
+ | finally show "longitud (repite (Suc n) x) = Suc n" by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Comentarios sobre la demostración anterior: | ||
+ | · A la derecha de proof se indica el método de la demostración. | ||
+ | · (induct n) indica que la demostración se hará por inducción en n. | ||
+ | · Se generan dos subobjetivos correspondientes a la base y el paso de | ||
+ | inducción: | ||
+ | 1. longitud (repite 0 x) = 0 | ||
+ | 2. ⋀n. longitud (repite n x) = n ⟹ longitud (repite (Suc n) x) = Suc n | ||
+ | donde ⋀n se lee "para todo n". | ||
+ | · "next" indica el siguiente subobjetivo. | ||
+ | · "fix n" indica "sea n un número natural cualquiera" | ||
+ | · assume HI: "longitud (repite n x) = n" indica «supongamos que | ||
+ | "longitud (repite n x) = n" y sea HI la etiqueta de este supuesto». | ||
+ | · "using HI" usando la propiedad etiquetada con HI. | ||
+ | *} | ||
− | (* | + | (* La demostración automática es *) |
− | lemma " | + | lemma "longitud (repite n x) = n" |
by (induct n) auto | by (induct n) auto | ||
+ | |||
+ | section {* Razonamiento por inducción sobre listas *} | ||
+ | |||
+ | text {* | ||
+ | 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 otra lista que también | ||
+ | tiene la propiedad. | ||
+ | |||
+ | En Isabelle el principio de inducción sobre listas está formalizado | ||
+ | mediante el teorema list.induct | ||
+ | ⟦P []; | ||
+ | ⋀x xs. P xs ⟹ P (x#xs)⟧ | ||
+ | ⟹ P xs | ||
+ | *} | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 9. Definir la función | |
− | + | conc :: 'a list ⇒ 'a list ⇒ 'a list | |
− | tal que ( | + | tal que (conc xs ys) es la concatención de las listas xs e ys. Por |
− | + | ejemplo, | |
− | + | conc [a,d] [b,d,a,c] = [a,d,b,d,a,c] | |
+ | ------------------------------------------------------------------ *} | ||
+ | |||
+ | fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where | ||
+ | "conc [] ys = ys" | ||
+ | | "conc (x#xs) ys = x # (conc xs ys)" | ||
+ | |||
+ | value "conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]" | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 10. (p. 24) Demostrar que | ||
+ | conc xs (conc ys zs) = (conc xs ys) zs | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "conc xs (conc ys zs) = conc (conc xs ys) zs" | ||
+ | proof (induct xs) | ||
+ | show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp | ||
+ | next | ||
+ | fix x xs | ||
+ | assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" | ||
+ | have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp | ||
+ | also have "... = x # (conc (conc xs ys) zs)" using HI by simp | ||
+ | also have "... = conc (conc (x # xs) ys) zs" by simp | ||
+ | finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" | ||
+ | by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Comentario sobre la demostración anterior | ||
+ | · (induct xs) genera dos subobjetivos: | ||
+ | 1. conc [] (conc ys zs) = conc (conc [] ys) zs | ||
+ | 2. ⋀a xs. conc xs (conc ys zs) = conc (conc xs ys) zs ⟹ | ||
+ | conc (a#xs) (conc ys zs) = conc (conc (a#xs) ys) zs | ||
+ | *} | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "conc xs (conc ys zs) = conc (conc xs ys) zs" | ||
+ | by (induct xs) auto | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 11. Refutar que | ||
+ | conc xs ys = conc ys xs | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | lemma "conc xs ys = conc ys xs" | ||
+ | quickcheck | ||
+ | oops | ||
+ | |||
+ | text {* Encuentra el contraejemplo, | ||
+ | xs = [a2] | ||
+ | ys = [a1] *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 12. (p. 28) Demostrar que | ||
+ | conc xs [] = xs | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "conc xs [] = xs" | ||
+ | proof (induct xs) | ||
+ | show "conc [] [] = []" by simp | ||
+ | next | ||
+ | fix x xs | ||
+ | assume HI: "conc xs [] = xs" | ||
+ | have "conc (x # xs) [] = x # (conc xs [])" by simp | ||
+ | also have "... = x # xs" using HI by simp | ||
+ | finally show "conc (x # xs) [] = x # xs" by simp | ||
+ | qed | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "conc xs [] = xs" | ||
+ | by (induct xs) simp_all | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 13. (p. 30) Demostrar que | ||
+ | longitud (conc xs ys) = longitud xs + longitud ys | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "longitud (conc xs ys) = longitud xs + longitud ys" | ||
+ | proof (induct xs) | ||
+ | show "longitud (conc [] ys) = longitud [] + longitud ys" by simp | ||
+ | next | ||
+ | fix x xs | ||
+ | assume HI: "longitud (conc xs ys) = longitud xs + longitud ys" | ||
+ | have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))" | ||
+ | by simp | ||
+ | also have "... = 1 + longitud (conc xs ys)" by simp | ||
+ | also have "... = 1 + longitud xs + longitud ys" using HI by simp | ||
+ | also have "... = longitud (x # xs) + longitud ys" by simp | ||
+ | finally show "longitud (conc (x # xs) ys) = | ||
+ | longitud (x # xs) + longitud ys" by simp | ||
+ | qed | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "longitud (conc xs ys) = longitud xs + longitud ys" | ||
+ | by (induct xs) auto | ||
+ | |||
+ | section {* Inducción correspondiente a la definición recursiva *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 14. 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 {* --------------------------------------------------------------- | ||
+ | Ejemplo 15. Definir la función | ||
+ | elimina :: nat ⇒ 'a list ⇒ 'a list | ||
+ | tal que (elimina n xs) es la lista obtenida eliminando los n primeros | ||
+ | elementos de xs. Por ejemplo, | ||
+ | elimina 2 [a,c,d,b,e] = [d,b,e] | ||
+ | ------------------------------------------------------------------ *} | ||
+ | |||
+ | fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where | ||
+ | "elimina n [] = []" | ||
+ | | "elimina 0 xs = xs" | ||
+ | | "elimina (Suc n) (x#xs) = elimina n xs" | ||
+ | |||
+ | value "elimina 2 [a,c,d,b,e] = [d,b,e]" | ||
+ | |||
+ | text {* | ||
+ | La definición coge genera el esquema de inducción coge.induct: | ||
+ | ⟦⋀n. P n []; | ||
+ | ⋀x xs. P 0 (x#xs); | ||
+ | ⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧ | ||
+ | ⟹ P n x | ||
+ | |||
+ | Puede verse usando "thm coge.induct". *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 16. (p. 35) Demostrar que | ||
+ | conc (coge n xs) (elimina n xs) = xs | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "conc (coge n xs) (elimina n xs) = xs" | ||
+ | proof (induct rule: coge.induct) | ||
+ | fix n | ||
+ | show "conc (coge n []) (elimina n []) = []" by simp | ||
+ | next | ||
+ | fix x xs | ||
+ | show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" by simp | ||
+ | next | ||
+ | fix n x xs | ||
+ | assume HI: "conc (coge n xs) (elimina n xs) = xs" | ||
+ | have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = | ||
+ | conc (x#(coge n xs)) (elimina n xs)" by simp | ||
+ | also have "... = x#(conc (coge n xs) (elimina n xs))" by simp | ||
+ | also have "... = x#xs" using HI by simp | ||
+ | finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = | ||
+ | x#xs" | ||
+ | by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Comentario sobre la demostración anterior: | ||
+ | · (induct rule: coge.induct) indica que el método de demostración es | ||
+ | por el esquema de inducción correspondiente a la definición de la | ||
+ | función coge. | ||
+ | · Se generan 3 subobjetivos: | ||
+ | · 1. ⋀n. conc (coge n []) (elimina n []) = [] | ||
+ | · 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs | ||
+ | · 3. ⋀n x xs. | ||
+ | conc (coge n xs) (elimina n xs) = xs ⟹ | ||
+ | conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs | ||
+ | *} | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "conc (coge n xs) (elimina n xs) = xs" | ||
+ | by (induct rule: coge.induct) auto | ||
+ | |||
+ | section {* Razonamiento por casos *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 17. Definir la función | ||
+ | esVacia :: 'a list ⇒ bool | ||
+ | tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo, | ||
+ | esVacia [] = True | ||
+ | esVacia [1] = False | ||
+ | ------------------------------------------------------------------ *} | ||
+ | |||
+ | fun esVacia :: "'a list ⇒ bool" where | ||
+ | "esVacia [] = True" | ||
+ | | "esVacia (x#xs) = False" | ||
+ | |||
+ | value "esVacia [] = True" | ||
+ | value "esVacia [a] = False" | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 18 (p. 39) . Demostrar que | ||
+ | esVacia xs = esVacia (conc xs xs) | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "esVacia xs = esVacia (conc xs xs)" | ||
+ | proof (cases xs) | ||
+ | assume "xs = []" | ||
+ | then show "esVacia xs = esVacia (conc xs xs)" by simp | ||
+ | next | ||
+ | fix y ys | ||
+ | assume "xs = y#ys" | ||
+ | then show "esVacia xs = esVacia (conc xs xs)" by simp | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Comentarios sobre la demostración anterior: | ||
+ | · "(cases xs)" es el método de demostración por casos según xs. | ||
+ | · Se generan dos subobjetivos correspondientes a los dos | ||
+ | constructores de listas: | ||
+ | · 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs) | ||
+ | · 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs) | ||
+ | · "then" indica "usando la propiedad anterior" | ||
+ | *} | ||
+ | |||
+ | (* La demostración estructurada simplificada es *) | ||
+ | lemma "esVacia xs = esVacia (conc xs xs)" | ||
+ | proof (cases xs) | ||
+ | case Nil | ||
+ | then show "esVacia xs = esVacia (conc xs xs)" by simp | ||
+ | next | ||
+ | case Cons | ||
+ | then show "esVacia xs = esVacia (conc xs xs)" 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" | ||
+ | · "thus" es una abreviatura de "then show". | ||
+ | *} | ||
+ | |||
+ | (* La demostración con el patrón sugerido es *) | ||
+ | lemma "esVacia xs = esVacia (conc xs xs)" | ||
+ | proof (cases xs) | ||
+ | case Nil | ||
+ | then show ?thesis by simp | ||
+ | next | ||
+ | case (Cons x xs) | ||
+ | then show ?thesis by simp | ||
+ | qed | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "esVacia xs = esVacia (conc xs xs)" | ||
+ | by (cases xs) auto | ||
+ | |||
+ | section {* Heurística de generalización *} | ||
+ | |||
+ | text {* | ||
+ | Heurística de generalización: Cuando se use demostración estructural, | ||
+ | cuantificar universalmente las variables libres (o, equivalentemente, | ||
+ | considerar las variables libres como variables arbitrarias). *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 19. Definir la función | ||
+ | inversaAc :: 'a list ⇒ 'a list | ||
+ | tal que (inversaAc xs) es a inversa de xs calculada usando | ||
+ | acumuladores. Por ejemplo, | ||
+ | inversaAc [a,c,b,e] = [e,b,c,a] | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | + | fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where | |
− | fun | + | "inversaAcAux [] ys = ys" |
− | " | + | | "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)" |
− | |||
− | + | fun inversaAc :: "'a list ⇒ 'a list" where | |
− | fun | + | "inversaAc xs = inversaAcAux xs []" |
− | " | ||
− | |||
− | + | value "inversaAc [a,c,b,e] = [e,b,c,a]" | |
− | |||
− | |||
− | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 20. (p. 44) Demostrar que | |
− | + | inversaAcAux xs ys = (inversa xs) @ ys | |
− | + | ------------------------------------------------------------------- *} | |
− | |||
− | |||
− | |||
− | |||
− | ----------------------------------------------------------------- *} | ||
− | (* | + | (* La demostración estructurada es *) |
− | + | lemma inversaAcAux_es_inversa: | |
− | " | + | "inversaAcAux xs ys = (inversa xs) @ ys" |
− | " | + | proof (induct xs arbitrary: ys) |
+ | show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp | ||
+ | next | ||
+ | fix a xs | ||
+ | assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys" | ||
+ | show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys" | ||
+ | proof - | ||
+ | fix ys | ||
+ | have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp | ||
+ | also have "… = inversa xs@(a#ys)" using HI by simp | ||
+ | also have "… = inversa (a#xs)@ys" by simp | ||
+ | finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp | ||
+ | qed | ||
+ | qed | ||
+ | |||
+ | text {* | ||
+ | Comentarios sobre la demostración anterior: | ||
+ | · "(induct xs arbitrary: ys)" es el método de demostración por | ||
+ | inducción sobre xs usando ys como variable arbitraria. | ||
+ | · Se generan dos subobjetivos: | ||
+ | · 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys | ||
+ | · 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹ | ||
+ | inversaAcAux (a # xs) ys = inversa (a # xs) @ ys | ||
+ | · Dentro de una demostración se pueden incluir otras demostraciones. | ||
+ | · Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una | ||
+ | lista arbitraria (con "fix ys") y se demuestra "P(ys)". | ||
+ | *} | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "inversaAcAux xs ys = (inversa xs)@ys" | ||
+ | by (induct xs arbitrary: ys) auto | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 21. (p. 43) Demostrar que | |
− | + | inversaAc xs = inversa xs | |
------------------------------------------------------------------- *} | ------------------------------------------------------------------- *} | ||
− | (* | + | (* La demostración automática es *) |
− | + | corollary "inversaAc xs = inversa xs" | |
− | + | by (simp add: inversaAcAux_es_inversa) | |
− | + | ||
− | + | text {* | |
+ | Comentario de la demostración anterior: | ||
+ | · "(simp add: inversaAcAux_es_inversa)" es el método de demostración | ||
+ | por simplificación usando como regla de simplificación la propiedad | ||
+ | inversaAcAux_es_inversa. | ||
+ | *} | ||
+ | |||
+ | section {* Demostración por inducción para funciones de orden superior *} | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 22. Definir la función | ||
+ | sum :: nat list ⇒ nat | ||
+ | tal que (sum xs) es la suma de los elementos de xs. Por ejemplo, | ||
+ | sum [3,2,5] = 10 | ||
+ | ------------------------------------------------------------------ *} | ||
+ | |||
+ | fun sum :: "nat list ⇒ nat" where | ||
+ | "sum [] = 0" | ||
+ | | "sum (x#xs) = x + sum xs" | ||
− | + | value "sum [3,2,5] = 10" | |
− | |||
− | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 23. Definir la función | |
− | + | map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list | |
− | tal que ( | + | tal que (map f xs) es la lista obtenida aplicando la función f a los |
− | + | elementos de xs. Por ejemplo, | |
− | + | map (λx. 2*x) [3,2,5] = [6,4,10] | |
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | + | fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where | |
− | fun | + | "map f [] = []" |
− | " | + | | "map f (x#xs) = (f x) # map f xs" |
− | + | ||
+ | value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]" | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
− | + | Ejemplo 24. (p. 45) Demostrar que | |
− | + | sum (map (λx. 2*x) xs) = 2 * (sum xs) | |
------------------------------------------------------------------- *} | ------------------------------------------------------------------- *} | ||
− | (* | + | (* La demostración estructurada es *) |
− | lemma " | + | lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)" |
− | + | proof (induct xs) | |
− | + | show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp | |
− | + | next | |
+ | fix a xs | ||
+ | assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)" | ||
+ | have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))" | ||
+ | by simp | ||
+ | also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp | ||
+ | also have "... = 2*a + 2*(sum xs)" using HI by simp | ||
+ | also have "... = 2*(a + sum xs)" by simp | ||
+ | also have "... = 2*(sum (a#xs))" by simp | ||
+ | finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp | ||
+ | qed | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)" | ||
+ | by (induct xs) auto | ||
+ | |||
+ | text {* --------------------------------------------------------------- | ||
+ | Ejemplo 25. (p. 48) Demostrar que | ||
+ | longitud (map f xs) = longitud xs | ||
+ | ------------------------------------------------------------------- *} | ||
+ | |||
+ | (* La demostración estructurada es *) | ||
+ | lemma "longitud (map f xs) = longitud xs" | ||
+ | proof (induct xs) | ||
+ | show "longitud (map f []) = longitud []" by simp | ||
+ | next | ||
+ | fix a xs | ||
+ | assume HI: "longitud (map f xs) = longitud xs" | ||
+ | have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp | ||
+ | also have "... = 1 + longitud (map f xs)" by simp | ||
+ | also have "... = 1 + longitud xs" using HI by simp | ||
+ | also have "... = longitud (a#xs)" by simp | ||
+ | finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp | ||
+ | qed | ||
+ | |||
+ | (* La demostración automática es *) | ||
+ | lemma "longitud (map f xs) = longitud xs" | ||
+ | by (induct xs) auto | ||
− | + | section {* Referencias *} | |
− | |||
− | |||
− | + | text {* | |
− | + | · J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3 | |
− | + | · G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about | |
+ | programms". | ||
+ | · S. Thompson. "Haskell: the Craft of Functional Programming, 3rd | ||
+ | Edition. Cap. 8 "Reasoning about programms". | ||
+ | · L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6. | ||
+ | "Reasoning about functional programs". | ||
+ | *} | ||
end | end | ||
</source> | </source> |
Revisión actual del 14:27 23 nov 2018
chapter {* Tema 3: Razonamiento estructurado sobre programas *}
theory T3_Razonamiento_sobre_programas
imports Main
begin
text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 2a y se demostraron
automáticamente en el tema 2b. A diferencia del tema 2b, ahora
nos fijamos no sólo en el método de demostración sino en la estructura
de la prueba resaltando su semejanza con las del tema 2a. *}
declare [[names_short]]
section {* Razonamiento ecuacional *}
text {* ----------------------------------------------------------------
Ejemplo 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [a,c,d] = 3
------------------------------------------------------------------- *}
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"
value "longitud [a,c,d] = 3"
text {* ---------------------------------------------------------------
Ejemplo 2. Demostrar que
longitud [a,c,d] = 3
------------------------------------------------------------------- *}
lemma "longitud [a,c,d] = 3"
by simp
text {* ---------------------------------------------------------------
Ejemplo 3. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"
value "intercambia (u,v) = (v,u)"
text {*
La definición de la función intercambia genera una regla de
simplificación
· intercambia.simps: intercambia (x,y) = (y,x)
Se puede ver con
· thm intercambia.simps
*}
text {* ---------------------------------------------------------------
Ejemplo 4. (p.6) Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}
(* Demostración aplicativa *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
apply (simp only: intercambia.simps)
done
(* Demostración declarativa *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)"
by (simp only: intercambia.simps)
also have "... = (x,y)"
by (simp only: intercambia.simps)
finally show "intercambia (intercambia (x,y)) = (x,y)"
by simp
qed
text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "proof" para iniciar la prueba,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "by (simp only: intercambia.simps)" para indicar que sólo se usa
como regla de escritura la correspondiente a la definición de
intercambia,
· "also" para encadenar pasos ecuacionales,
· "..." para representar la derecha de la igualdad anterior en un
razonamiento ecuacional,
· "finally" para indicar el último pasa de un razonamiento ecuacional,
· "show" para establecer la conclusión.
· "by simp" para indicar el método de demostración por simplificación y
· "qed" para terminar la pruebas,
*}
(* Demostración declarativa simplificada *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)" by simp
also have "... = (x,y)" by simp
finally show "intercambia (intercambia (x,y)) = (x,y)" by simp
qed
text {*
Nota: La diferencia entre las dos demostraciones es que en los dos
primeros pasos no se explicita la regla de simplificación.
*}
(* Demostración automática *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp
text {* ---------------------------------------------------------------
Ejemplo 5. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}
fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"
value "inversa [a,d,c] = [c,d,a]"
text {* ---------------------------------------------------------------
Ejemplo 6. (p. 9) Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}
(* La demostración aplicativa es *)
lemma "inversa [x] = [x]"
apply simp
done
text {*
En la demostración anterior se usaron las siguientes reglas:
· inversa.simps(1): inversa [] = []
· inversa.simps(2): inversa (x#xs) = inversa xs @ [x]
· append_Nil: [] @ ys = ys
Vamos a explicitar su aplicación.
*}
(* La demostración aplicativa detallada es *)
lemma "inversa [x] = [x]"
apply (simp only: inversa.simps(2))
apply (simp only: inversa.simps(1))
apply (simp only: append_Nil)
done
(* La demostración declarativa es *)
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by (simp only: inversa.simps(2))
also have "... = [] @ [x]" by (simp only: inversa.simps(1))
also have "... = [x]" by (simp only: append_Nil)
finally show "inversa [x] = [x]" by simp
qed
(* La demostración declarativa simplificada es *)
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by simp
also have "... = [] @ [x]" by simp
also have "... = [x]" by simp
finally show "inversa [x] = [x]" by simp
qed
(* La demostración automática es *)
lemma "inversa [x] = [x]"
by simp
section {* Razonamiento por inducción sobre los naturales *}
text {*
[Principio de inducción sobre los naturales] 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 sobre los naturales está
formalizado en el teorema nat.induct y puede verse con
thm nat.induct
*}
text {* ---------------------------------------------------------------
Ejemplo 7. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"
value "repite 3 a = [a,a,a]"
text {* ---------------------------------------------------------------
Ejemplo 8. (p. 18) Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}
(* La demostración aplicativa es *)
lemma "longitud (repite n x) = n"
apply (induct n)
apply simp_all
done
(* La demostración estructurada es *)
lemma "longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume HI: "longitud (repite n x) = n"
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))"
by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using HI by simp
finally show "longitud (repite (Suc n) x) = Suc n" by simp
qed
text {*
Comentarios sobre la demostración anterior:
· A la derecha de proof se indica el método de la demostración.
· (induct n) indica que la demostración se hará por inducción en n.
· Se generan dos subobjetivos correspondientes a la base y el paso de
inducción:
1. longitud (repite 0 x) = 0
2. ⋀n. longitud (repite n x) = n ⟹ longitud (repite (Suc n) x) = Suc n
donde ⋀n se lee "para todo n".
· "next" indica el siguiente subobjetivo.
· "fix n" indica "sea n un número natural cualquiera"
· assume HI: "longitud (repite n x) = n" indica «supongamos que
"longitud (repite n x) = n" y sea HI la etiqueta de este supuesto».
· "using HI" usando la propiedad etiquetada con HI.
*}
(* La demostración automática es *)
lemma "longitud (repite n x) = n"
by (induct n) auto
section {* Razonamiento por inducción sobre listas *}
text {*
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 otra lista que también
tiene la propiedad.
En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct
⟦P [];
⋀x xs. P xs ⟹ P (x#xs)⟧
⟹ P xs
*}
text {* ---------------------------------------------------------------
Ejemplo 9. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"
value "conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
text {* ---------------------------------------------------------------
Ejemplo 10. (p. 24) Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs"
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using HI by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs"
by simp
qed
text {*
Comentario sobre la demostración anterior
· (induct xs) genera dos subobjetivos:
1. conc [] (conc ys zs) = conc (conc [] ys) zs
2. ⋀a xs. conc xs (conc ys zs) = conc (conc xs ys) zs ⟹
conc (a#xs) (conc ys zs) = conc (conc (a#xs) ys) zs
*}
(* La demostración automática es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto
text {* ---------------------------------------------------------------
Ejemplo 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}
lemma "conc xs ys = conc ys xs"
quickcheck
oops
text {* Encuentra el contraejemplo,
xs = [a2]
ys = [a1] *}
text {* ---------------------------------------------------------------
Ejemplo 12. (p. 28) Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "conc xs [] = xs"
proof (induct xs)
show "conc [] [] = []" by simp
next
fix x xs
assume HI: "conc xs [] = xs"
have "conc (x # xs) [] = x # (conc xs [])" by simp
also have "... = x # xs" using HI by simp
finally show "conc (x # xs) [] = x # xs" by simp
qed
(* La demostración automática es *)
lemma "conc xs [] = xs"
by (induct xs) simp_all
text {* ---------------------------------------------------------------
Ejemplo 13. (p. 30) Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume HI: "longitud (conc xs ys) = longitud xs + longitud ys"
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))"
by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + longitud xs + longitud ys" using HI by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show "longitud (conc (x # xs) ys) =
longitud (x # xs) + longitud ys" by simp
qed
(* La demostración automática es *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto
section {* Inducción correspondiente a la definición recursiva *}
text {* ---------------------------------------------------------------
Ejemplo 14. 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 {* ---------------------------------------------------------------
Ejemplo 15. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"
value "elimina 2 [a,c,d,b,e] = [d,b,e]"
text {*
La definición coge genera el esquema de inducción coge.induct:
⟦⋀n. P n [];
⋀x xs. P 0 (x#xs);
⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
⟹ P n x
Puede verse usando "thm coge.induct". *}
text {* ---------------------------------------------------------------
Ejemplo 16. (p. 35) Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
fix n
show "conc (coge n []) (elimina n []) = []" by simp
next
fix x xs
show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" by simp
next
fix n x xs
assume HI: "conc (coge n xs) (elimina n xs) = xs"
have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) =
conc (x#(coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = x#xs" using HI by simp
finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) =
x#xs"
by simp
qed
text {*
Comentario sobre la demostración anterior:
· (induct rule: coge.induct) indica que el método de demostración es
por el esquema de inducción correspondiente a la definición de la
función coge.
· Se generan 3 subobjetivos:
· 1. ⋀n. conc (coge n []) (elimina n []) = []
· 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs
· 3. ⋀n x xs.
conc (coge n xs) (elimina n xs) = xs ⟹
conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs
*}
(* La demostración automática es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto
section {* Razonamiento por casos *}
text {* ---------------------------------------------------------------
Ejemplo 17. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"
value "esVacia [] = True"
value "esVacia [a] = False"
text {* ---------------------------------------------------------------
Ejemplo 18 (p. 39) . Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
assume "xs = []"
then show "esVacia xs = esVacia (conc xs xs)" by simp
next
fix y ys
assume "xs = y#ys"
then show "esVacia xs = esVacia (conc xs xs)" by simp
qed
text {*
Comentarios sobre la demostración anterior:
· "(cases xs)" es el método de demostración por casos según xs.
· Se generan dos subobjetivos correspondientes a los dos
constructores de listas:
· 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
· 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
· "then" indica "usando la propiedad anterior"
*}
(* La demostración estructurada simplificada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil
then show "esVacia xs = esVacia (conc xs xs)" by simp
next
case Cons
then show "esVacia xs = esVacia (conc xs xs)" 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"
· "thus" es una abreviatura de "then show".
*}
(* La demostración con el patrón sugerido es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil
then show ?thesis by simp
next
case (Cons x xs)
then show ?thesis by simp
qed
(* La demostración automática es *)
lemma "esVacia xs = esVacia (conc xs xs)"
by (cases xs) auto
section {* Heurística de generalización *}
text {*
Heurística de generalización: Cuando se use demostración estructural,
cuantificar universalmente las variables libres (o, equivalentemente,
considerar las variables libres como variables arbitrarias). *}
text {* ---------------------------------------------------------------
Ejemplo 19. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"
fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"
value "inversaAc [a,c,b,e] = [e,b,c,a]"
text {* ---------------------------------------------------------------
Ejemplo 20. (p. 44) Demostrar que
inversaAcAux xs ys = (inversa xs) @ ys
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix a xs
assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
proof -
fix ys
have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
also have "… = inversa xs@(a#ys)" using HI by simp
also have "… = inversa (a#xs)@ys" by simp
finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
qed
qed
text {*
Comentarios sobre la demostración anterior:
· "(induct xs arbitrary: ys)" es el método de demostración por
inducción sobre xs usando ys como variable arbitraria.
· Se generan dos subobjetivos:
· 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
· 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
· Dentro de una demostración se pueden incluir otras demostraciones.
· Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
lista arbitraria (con "fix ys") y se demuestra "P(ys)".
*}
(* La demostración automática es *)
lemma "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto
text {* ---------------------------------------------------------------
Ejemplo 21. (p. 43) Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}
(* La demostración automática es *)
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)
text {*
Comentario de la demostración anterior:
· "(simp add: inversaAcAux_es_inversa)" es el método de demostración
por simplificación usando como regla de simplificación la propiedad
inversaAcAux_es_inversa.
*}
section {* Demostración por inducción para funciones de orden superior *}
text {* ---------------------------------------------------------------
Ejemplo 22. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}
fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"
value "sum [3,2,5] = 10"
text {* ---------------------------------------------------------------
Ejemplo 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"
value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]"
text {* ---------------------------------------------------------------
Ejemplo 24. (p. 45) Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))"
by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2*(sum xs)" using HI by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2*(sum (a#xs))" by simp
finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp
qed
(* La demostración automática es *)
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto
text {* ---------------------------------------------------------------
Ejemplo 25. (p. 48) Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}
(* La demostración estructurada es *)
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix a xs
assume HI: "longitud (map f xs) = longitud xs"
have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using HI by simp
also have "... = longitud (a#xs)" by simp
finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp
qed
(* La demostración automática es *)
lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto
section {* Referencias *}
text {*
· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
programms".
· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
Edition. Cap. 8 "Reasoning about programms".
· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.
"Reasoning about functional programs".
*}
end