RA2014: Ejercicios de razonamiento automático sobre programas con Isabelle/HOL
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 3ª relación de ejercicios cuyo objetivo es demostrar con Isabelle/HOL propiedades de programas.
Los ejercicios y sus soluciones se muestran a continuación
|
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 |
header {* R3: Razonamiento sobre programas *} theory R3 imports Main begin text {* --------------------------------------------------------------- Ejercicio 1. Definir la función sumaImpares :: nat ⇒ nat tal que (sumaImpares n) es la suma de los n primeros números impares. Por ejemplo, sumaImpares 5 = 25 ------------------------------------------------------------------ *} fun sumaImpares :: "nat ⇒ nat" where "sumaImpares 0 = 0" | "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" value "sumaImpares 5" -- "= 25" text {* --------------------------------------------------------------- Ejercicio 2. Demostrar que sumaImpares n = n*n ------------------------------------------------------------------- *} -- "La demostración estructurada es" lemma "sumaImpares n = n*n" proof (induct n) show "sumaImpares 0 = 0 * 0" by simp next fix n assume HI: "sumaImpares n = n * n" have "sumaImpares (Suc n) = sumaImpares n + (2*n+1)" by simp also have "... = n*n + (2*n+1)" using HI by simp also have "... = Suc n * Suc n" by simp finally show "sumaImpares (Suc n) = Suc n * Suc n" by simp qed -- "La demostración automática es" lemma "sumaImpares n = n*n" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 3. Definir la función sumaPotenciasDeDosMasUno :: nat ⇒ nat tal que (sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n. Por ejemplo, sumaPotenciasDeDosMasUno 3 = 16 ------------------------------------------------------------------ *} fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where "sumaPotenciasDeDosMasUno 0 = 2" | "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" value "sumaPotenciasDeDosMasUno 3" -- "= 16" text {* --------------------------------------------------------------- Ejercicio 4. Demostrar que sumaPotenciasDeDosMasUno n = 2^(n+1) ------------------------------------------------------------------- *} -- "La demostración estructurada es" lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" proof (induct n) show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp next fix n assume HI: "sumaPotenciasDeDosMasUno n = 2^(n+1)" have "sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(n+1)" by simp also have "... = 2^(n+1) + 2^(n+1)" using HI by simp also have "... = 2 ^ (Suc n + 1)" by simp finally show "sumaPotenciasDeDosMasUno (Suc n) = 2 ^ (Suc n + 1)" by simp qed -- "La demostración automática es" lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 5. Definir la función copia :: nat ⇒ 'a ⇒ 'a list tal que (copia n x) es la lista formado por n copias del elemento x. Por ejemplo, copia 3 x = [x,x,x] ------------------------------------------------------------------ *} fun copia :: "nat ⇒ 'a ⇒ 'a list" where "copia 0 x = []" | "copia (Suc n) x = x # copia n x" value "copia 3 x" -- "= [x,x,x]" text {* --------------------------------------------------------------- Ejercicio 6. Definir la función todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool tal que (todos p xs) se verifica si todos los elementos de xs cumplen la propiedad p. Por ejemplo, todos (λx. x>(1::nat)) [2,6,4] = True todos (λx. x>(2::nat)) [2,6,4] = False ------------------------------------------------------------------ *} fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where "todos p [] = True" | "todos p (x#xs) = (p x ∧ todos p xs)" value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True" value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False" text {* --------------------------------------------------------------- Ejercicio 7. Demostrar que todos los elementos de (copia n x) son iguales a x. ------------------------------------------------------------------- *} -- "La demostración estructurada es" lemma "todos (λy. y=x) (copia n x)" proof (induct n) show "todos (λy. y = x) (copia 0 x)" by simp next fix n assume HI: "todos (λy. y = x) (copia n x)" have "todos (λy. y = x) (copia (Suc n) x) = todos (λy. y = x) (x # copia n x)" by simp also have "... = (x = x ∧ todos (λy. y = x) (copia n x))" by simp also have "... = True" using HI by simp finally show "todos (λy. y = x) (copia (Suc n) x)" by simp qed -- "La demostración automática es" lemma "todos (λy. y=x) (copia n x)" by (induct n) auto text {* --------------------------------------------------------------- Ejercicio 8. Definir la función factR :: nat ⇒ nat tal que (factR n) es el factorial de n. Por ejemplo, factR 4 = 24 ------------------------------------------------------------------ *} fun factR :: "nat ⇒ nat" where "factR 0 = 1" | "factR (Suc n) = Suc n * factR n" value "factR 4" -- "= 24" text {* --------------------------------------------------------------- Ejercicio 9. Se considera la siguiente definición iterativa de la función factorial factI :: "nat ⇒ nat" where factI n = factI' n 1 factI' :: nat ⇒ nat ⇒ nat" where factI' 0 x = x factI' (Suc n) x = factI' n (Suc n)*x Demostrar que, para todo n y todo x, se tiene factI' n x = x * factR n Indicación: La propiedad mult_Suc es (Suc m) * n = n + m * n Puede que se necesite desactivarla en un paso con (simp del: mult_Suc) ------------------------------------------------------------------- *} fun factI' :: "nat ⇒ nat ⇒ nat" where "factI' 0 x = x" | "factI' (Suc n) x = factI' n (x * Suc n)" fun factI :: "nat ⇒ nat" where "factI n = factI' n 1" value "factI 4" -- "= 24" -- "La demostración estructurada es" lemma fact: "factI' n x = x * factR n" proof (induct n arbitrary: x) show "⋀x. factI' 0 x = x * factR 0" by simp next fix n assume HI: "⋀x. factI' n x = x * factR n" show "⋀x. factI' (Suc n) x = x * factR (Suc n)" proof - fix x have "factI' (Suc n) x = factI' n (x * Suc n)" by simp also have "... = (x * Suc n) * factR n" using HI by simp also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc) also have "... = x * factR (Suc n)" by simp finally show "factI' (Suc n) x = x * factR (Suc n)" by simp qed qed -- "La demostración automática es" lemma "factI' n x = x * factR n" by (induct n arbitrary: x) (auto simp del: mult_Suc) text {* --------------------------------------------------------------- Ejercicio 10. Demostrar que factI n = factR n ------------------------------------------------------------------- *} corollary "factI n = factR n" by (simp add: fact) text {* --------------------------------------------------------------- Ejercicio 11. Definir, recursivamente y sin usar (@), la función amplia :: 'a list ⇒ 'a ⇒ 'a list tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al final de la lista xs. Por ejemplo, amplia [d,a] t = [d,a,t] ------------------------------------------------------------------ *} fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where "amplia [] y = [y]" | "amplia (x#xs) y = x # amplia xs y" value "amplia [d,a] t" -- "= [d,a,t]" text {* --------------------------------------------------------------- Ejercicio 12. Demostrar que amplia xs y = xs @ [y] ------------------------------------------------------------------- *} -- "La demostración estructurada es" lemma "amplia xs y = xs @ [y]" proof (induct xs) show "amplia [] y = [] @ [y]" by simp next fix x xs assume HI: "amplia xs y = xs @ [y]" have "amplia (x # xs) y = x # amplia xs y" by simp also have "... = x # (xs @ [y])" using HI by simp also have "... = (x # xs) @ [y]" by simp finally show "amplia (x # xs) y = (x # xs) @ [y]" by simp qed -- "La demostración automática es" lemma "amplia xs y = xs @ [y]" by (induct xs) auto end |