RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL
En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 2ª relación de ejercicios de razonamiento sobre programas. Para cada propiedad se dan dos demostraciones en Isabelle/HOL: la primera automática y la segunda aplicativa detallando los pasos.
La teoría con las soluciones de los ejercicios 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 |
chapter ‹R2: Razonamiento sobre programas› theory R2_Razonamiento_sobre_programas_sol imports Main begin declare [[names_short]] text ‹--------------------------------------------------------------- Ejercicio 1.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 1.2. Demostrar detallamente que sumaImpares n = n*n -------------------------------------------------------------------› lemma "sumaImpares n = n*n" apply (induct n) apply (simp only: sumaImpares.simps(1)) apply (simp only: sumaImpares.simps(2)) apply simp done text ‹--------------------------------------------------------------- Ejercicio 1.3. Demostrar automáticamente que sumaImpares n = n*n -------------------------------------------------------------------› lemma "sumaImpares n = n*n" by (induct n) simp_all text ‹--------------------------------------------------------------- Ejercicio 2.1. 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 2.2. Demostrar detalladamente que sumaPotenciasDeDosMasUno n = 2^(n+1) -------------------------------------------------------------------› lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" apply (induct n) apply (simp only: sumaPotenciasDeDosMasUno.simps(1)) apply simp apply (simp only: sumaPotenciasDeDosMasUno.simps(2)) apply simp done text ‹--------------------------------------------------------------- Ejercicio 2.3. Demostrar automáticamente que sumaPotenciasDeDosMasUno n = 2^(n+1) -------------------------------------------------------------------› lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)" by (induct n) simp_all text ‹--------------------------------------------------------------- Ejercicio 3.1. 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 3.2. 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 3.3. Demostrar detalladamente que todos los elementos de (copia n x) son iguales a x. -------------------------------------------------------------------› lemma "todos (λy. y=x) (copia n x)" apply (induct n) apply (simp only: copia.simps(1)) apply (simp only:todos.simps(1)) apply (simp only: copia.simps(2)) apply (simp only:todos.simps(2)) done text ‹--------------------------------------------------------------- Ejercicio 3.4. Demostrar automáticamente que todos los elementos de (copia n x) son iguales a x. -------------------------------------------------------------------› lemma "todos (λy. y=x) (copia n x)" by (induct n) simp_all text ‹--------------------------------------------------------------- Ejercicio 4.1. 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 4.2. Demostrar detalladamente que amplia xs y = xs @ [y] -------------------------------------------------------------------› lemma "amplia xs y = xs @ [y]" apply (induct xs) apply (simp only: amplia.simps(1)) apply (simp only: append.simps(1)) apply (simp only: amplia.simps(2)) apply (simp only: append.simps(2)) done text ‹--------------------------------------------------------------- Ejercicio 4.3. Demostrar automáticamente que amplia xs y = xs @ [y] -------------------------------------------------------------------› lemma "amplia xs y = xs @ [y]" by (induct xs) simp_all end |