RA2019: Razonamiento sobre programas con Isabelle/HOL (2/2)
En la clase de hoy del curso de Razonamiento automático se ha completado el estudio (comenzado en la clase anterior) sobre demostración de propiedades de programas con Isabelle/HOL.
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 |
chapter ‹Tema 2: Razonamiento sobre programas› theory T2_Razonamiento_sobre_programas imports Main begin section ‹Heurística de generalización› 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)" definition inversaAc :: "'a list ⇒ 'a list" where "inversaAc xs = inversaAcAux xs []" value "inversaAc [a,c,b,e] = [e,b,c,a]" text ‹Lema. [Ejemplo de equivalencia entre las definiciones] La inversa de [a,b,c] es lo mismo calculada con la primera definición que con la segunda.› lemma "inversaAc [a,b,c] = inversa [a,b,c]" apply (simp only: inversaAc_def) apply (simp only: inversaAcAux.simps(2)) apply (simp only: inversaAcAux.simps(1)) apply (simp only: inversa.simps(2)) apply (simp only: inversa.simps(1)) apply (simp only: append.simps(1)) apply (simp only: append.simps(2)) apply (simp only: append.simps(1)) apply (simp only: append.simps(2)) apply (simp only: append.simps(1)) done (* Se puede simplificar la demostración *) lemma "inversaAc [a,b,c] = inversa [a,b,c]" by (simp add: inversaAc_def) text ‹Nota. [Ejemplo fallido de demostración por inducción] El siguiente intento de demostrar que para cualquier lista xs, se tiene que "inversaAc xs = inversa xs" falla.› lemma "inversaAc xs = inversa xs" apply (induct xs) apply (simp only: inversaAc_def) apply (simp only: inversaAcAux.simps(1)) apply (simp only: inversa.simps(1)) apply (simp only: inversaAc_def) apply (simp only: inversaAcAux.simps(2)) apply (simp only: inversa.simps(2)) oops text ‹Nota. [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). Lema. [Lema con generalización] Para toda lista ys se tiene inversaAcAux xs ys = (inversa xs) @ ys› text ‹ --------------------------------------------------------------- Ejemplo 20. (p. 44) Demostrar que inversaAcAux xs ys = (inversa xs) @ ys ------------------------------------------------------------------- › (* Demostración aplicativa detallada *) lemma "inversaAcAux xs ys = (inversa xs)@ys" apply (induct xs arbitrary: ys) apply (simp only: inversaAcAux.simps(1)) apply (simp only: inversa.simps(1)) apply (simp only: append.simps(1)) apply (simp only: inversaAcAux.simps(2)) apply (simp only: inversa.simps(2)) apply (simp only: append_assoc) apply (simp only: append.simps(2)) apply (simp only: append.simps(1)) done (* Demostración aplicativa no detallada *) lemma "inversaAcAux xs ys = (inversa xs)@ys" apply (induct xs arbitrary: ys) apply simp_all done (* Demostración automática *) lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" by (induct xs arbitrary: ys) simp_all text ‹ --------------------------------------------------------------- Ejemplo 21. (p. 43) Demostrar que inversaAc xs = inversa xs ------------------------------------------------------------------- › (* Demostración aplicativa detallada *) corollary "inversaAc xs = inversa xs" apply (simp only: inversaAc_def) apply (simp only: inversaAcAux_es_inversa) apply (simp only: append_Nil2) done (* Nota: El último simplificador se busca con *) find_theorems "_ @ [] = _" (* Demostración aplicativa no detallada *) corollary "inversaAc xs = inversa xs" apply (simp add: inversaAcAux_es_inversa inversaAc_def) done (* Demostración automática *) corollary "inversaAc xs = inversa xs" by (simp add: inversaAcAux_es_inversa inversaAc_def) 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::nat,2,5] = [6,4,10] map ((*) 2) [3::nat,2,5] = [6,4,10] map ((+) 2) [3::nat,2,5] = [5,4,7] ------------------------------------------------------------------ › 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]" value "map ((*) 2) [3::nat,2,5] = [6,4,10]" value "map ((+) 2) [3::nat,2,5] = [5,4,7]" text ‹ --------------------------------------------------------------- Ejemplo 24. (p. 45) Demostrar que sum (map ((*) 2) xs) = 2 * (sum xs) ------------------------------------------------------------------- › (* Demostración aplicativa detallada *) lemma "sum (map ((*) 2) xs) = 2 * (sum xs)" apply (induct xs) apply (simp only: map.simps(1)) apply (simp only: sum.simps(1)) apply (simp only: map.simps(2)) apply (simp only: sum.simps(2)) apply (simp only: add_mult_distrib2) done (* Nota: El último simplificador se busca con *) find_theorems "_ * (_ + _) = _" (* Demostración aplicativa no detallada *) lemma "sum (map ((*) 2) xs) = 2 * (sum xs)" apply (induct xs) apply simp_all done (* Demostración automática *) lemma "sum (map ((*) 2) xs) = 2 * (sum xs)" by (induct xs) simp_all text ‹ --------------------------------------------------------------- Ejemplo 25. (p. 48) Demostrar que longitud (map f xs) = longitud xs ------------------------------------------------------------------- › (* Demostración aplicativa no detallada *) lemma "longitud (map f xs) = longitud xs" apply (induct xs) apply (simp only: map.simps(1)) apply (simp only: longitud.simps(1)) apply (simp only: map.simps(2)) apply (simp only: longitud.simps(2)) done (* Demostración aplicativa no detallada *) lemma "longitud (map f xs) = longitud xs" apply (induct xs) apply simp_all done (* Demostración automática *) lemma "longitud (map f xs) = longitud xs" by (induct xs) simp_all end |