RA2012: Razonamiento sobre programas con Isabelle/HOL (1)
En la segunda parte de 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.
En la presentación se han usado los ejemplos del tema 8 del curso de Informática (de 1º del Grado en Matemáticas).
La teoría con los ejemplos presentados en la clase es la siguiente:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 |
header {* Tema 5: Razonamiento sobre programas *} theory T5 imports Main begin text {* En este tema se demuestra con Isabelle las propiedades de los programas funcionales como se expone en el tema 8 del curso "Informática" que puede leerse en http://goo.gl/Imvyt *} 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 [4,2,5] = 3 ------------------------------------------------------------------- *} fun longitud :: "'a list ⇒ nat" where "longitud [] = 0" | "longitud (x#xs) = 1 + longitud xs" value "longitud [4,2,5]" -- "= 3" text {* --------------------------------------------------------------- Ejemplo 2. Demostrar que longitud [4,2,5] = 3 ------------------------------------------------------------------- *} lemma "longitud [4,2,5] = 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 {* --------------------------------------------------------------- Ejemplo 4. (p.6) Demostrar que intercambia (intercambia (x,y)) = (x,y) ------------------------------------------------------------------- *} -- "La demostración detallada es" 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 {* El razonamiento ecuacional se realiza usando la combinación de "also" (además) y "finally" (finalmente). *} -- "La demostración estructurada es" 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 -- "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 detallada 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 estructurada 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 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 -- "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 que puede verse con thm list.induct *} 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 -- "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 = [a\<^isub>2] ys = [a\<^isub>1] *} 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". *} end |
Como tarea se propuso la resolución de los ejercicios de la relación 8.