RA2017: Ejercicios de razonamiento detallado sobre programas en Isabelle/HOL

En la primera parte de la clase de hoy del curso de
Razonamiento automático se han comentado las soluciones de la 3ª relación de ejercicios sobre razonamiento detallado sobre programas en Isabelle/HOL

La teoría con las soluciones de los ejercicios es la siguiente

chapter {* R3: Razonamiento sobre programas *}

theory R3
imports Main 
begin

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)"

text {* --------------------------------------------------------------- 
  Ejercicio 1.2. Escribir la demostración detallada de 
     sumaImpares n = n*n
  ------------------------------------------------------------------- *}

-- "La demostración detallada 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 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)"

text {* --------------------------------------------------------------- 
  Ejercicio 2.2. Escribir la demostración detallada de 
     sumaPotenciasDeDosMasUno n = 2^(n+1)
  ------------------------------------------------------------------- *}

-- "La demostración detallada 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 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"

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.2. Demostrar detalladamente que todos los elementos de
  (copia n x) son iguales a x. 
  ------------------------------------------------------------------- *}

-- "La demostración detallada 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 4.1. 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"

text {* --------------------------------------------------------------- 
  Ejercicio 4.2. 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"

-- "La demostración detallada 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 4.3. Escribir la demostración detallada de
     factI n = factR n
  ------------------------------------------------------------------- *}

corollary "factI n = factR n"
by (simp add: fact)

text {* --------------------------------------------------------------- 
  Ejercicio 5.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"

text {* --------------------------------------------------------------- 
  Ejercicio 5.2. Escribir la demostración detallada de
     amplia xs y = xs @ [y]
  ------------------------------------------------------------------- *}

-- "La demostración detallada 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

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

chapter {* R3: Razonamiento sobre programas *}

theory R3

imports Main

begin

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)"

text {* ---------------------------------------------------------------

Ejercicio 1.2. Escribir la demostración detallada de

sumaImpares n = n*n

------------------------------------------------------------------- *}

-- "La demostración detallada es"

lemma "sumaImpares n = n*n"

proof (induct n)

show "sumaImpares 0 = 0 * 0" by simp

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 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)"

text {* ---------------------------------------------------------------

Ejercicio 2.2. Escribir la demostración detallada de

sumaPotenciasDeDosMasUno n = 2^(n+1)

------------------------------------------------------------------- *}

-- "La demostración detallada es"

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"

proof (induct n)

show "sumaPotenciasDeDosMasUno 0 = 2^(0+1)" by simp

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 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"

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.2. Demostrar detalladamente que todos los elementos de

(copia n x) son iguales a x.

------------------------------------------------------------------- *}

-- "La demostración detallada es"

lemma "todos (λy. y=x) (copia n x)"

proof (induct n)

show "todos (λy. y = x) (copia 0 x)" by simp

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 4.1. 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"

text {* ---------------------------------------------------------------

Ejercicio 4.2. 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"

-- "La demostración detallada es"

lemma fact: "factI' n x = x * factR n"

proof (induct n arbitrary: x)

show "⋀x. factI' 0 x = x * factR 0" by simp

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

-- "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 4.3. Escribir la demostración detallada de

factI n = factR n

------------------------------------------------------------------- *}

corollary "factI n = factR n"

by (simp add: fact)

text {* ---------------------------------------------------------------

Ejercicio 5.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"

text {* ---------------------------------------------------------------

Ejercicio 5.2. Escribir la demostración detallada de

amplia xs y = xs @ [y]

------------------------------------------------------------------- *}

-- "La demostración detallada es"

lemma "amplia xs y = xs @ [y]"

proof (induct xs)

show "amplia [] y = [] @ [y]" by simp

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

Se puede imprimir o compartir con