En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.
Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.
La teoría con los ejemplos presentados en la clase es la siguiente:
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. *} 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 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. *} -- "La demostración automática es" 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 auto 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) auto text {* --------------------------------------------------------------- Ejemplo 13. (p. 30) Demostrar que longitud (conc xs ys) = longitud xs + longitud ys ------------------------------------------------------------------- *} -- "La demostración automática 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 {* 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 |
Como tarea para la próxima clase se propuso la resolución de los ejercicios de la 3ª relación