RA2013: Razonamiento estructurado sobre programas con Isabelle/HOL (2)

En la clase de hoy del curso de Razonamiento automático hemos continuado la presentación de cómo se puede demostrar detalladamente propiedades de programas funcionales con Isabelle/HOL.

Para ello, se visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 2a (que se corresponden con el capítulo 13 del libro de G. Hutton Programming in Haskell).

Las demostraciones estudiadas son las correspondientes a las páginas 38 a 50 del tema 2a. Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.

La teoría con los ejemplos presentados en la clase es la siguiente:

header {* Tema 3: Razonamiento estructurado sobre programas *}

theory T3
imports Main 
begin

section {* Razonamiento por casos *}

text {* --------------------------------------------------------------- 
  Ejemplo 17. Definir la función
     esVacia :: 'a list ⇒ bool
  tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
     esVacia []  = True
     esVacia [1] = False
  ------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
  "esVacia []     = True"
| "esVacia (x#xs) = False"

value "esVacia []"  -- "= True"
value "esVacia [1]" -- "= False"

text {* --------------------------------------------------------------- 
  Ejemplo 18 (p. 39) . Demostrar que 
     esVacia xs = esVacia (conc xs xs)
  ------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  assume "xs = []"
  then show "esVacia xs = esVacia (conc xs xs)" by simp
next
  fix y ys
  assume "xs = y#ys"
  then show "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · "(cases xs)" es el método de demostración por casos según xs.
  · Se generan dos subobjetivos  correspondientes a los dos
    constructores de listas:
    · 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
    · 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
  · "then" indica "usando la propiedad anterior"
*}

-- "La demostración estructurada simplificada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show "esVacia xs = esVacia (conc xs xs)" by simp
next
  case Cons
  then show "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
  Comentarios sobre la demostración anterior:
  · "case Nil" es una abreviatura de "assume xs = []"
  · "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"
  · "thus" es una abreviatura de "then show".
*}

-- "La demostración automática es"
lemma "esVacia xs = esVacia (conc xs xs)"
by (cases xs) auto

section {* Heurística de generalización *}

text {* 
  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). *}

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

fun inversaAc :: "'a list ⇒ 'a list" where
  "inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* --------------------------------------------------------------- 
  Ejemplo 20. (p. 44) Demostrar que 
     inversaAcAux xs ys = (inversa xs) @ ys
  ------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
  fix a xs 
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
    also have "… = inversa xs@(a#ys)" using HI by simp
    also have "… = inversa (a#xs)@ys" by simp 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
  qed
qed

text {*
  Comentarios sobre la demostración anterior:
  · "(induct xs arbitrary: ys)" es el método de demostración por
    inducción sobre xs usando ys como variable arbitraria.
  · Se generan dos subobjetivos:
    · 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
    · 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
                    inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
  · Dentro de una demostración se pueden incluir otras demostraciones.
  · Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
    lista arbitraria (con "fix ys") y se demuestra "P(ys)". 
*}

-- "La demostración automática es"
lemma "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* --------------------------------------------------------------- 
  Ejemplo 21. (p. 43) Demostrar que 
     inversaAc xs = inversa xs
  ------------------------------------------------------------------- *}

-- "La demostración automática es"
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {*
  Comentario de la demostración anterior:
  · "(simp add: inversaAcAux_es_inversa)" es el método de demostración
    por simplificación usando como regla de simplificación la propiedad
    inversaAcAux_es_inversa. 
*}

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,2,5] = [6,4,10]
  ------------------------------------------------------------------ *}

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

text {* --------------------------------------------------------------- 
  Ejemplo 24. (p. 45) Demostrar que 
     sum (map (λx. 2*x) xs) = 2 * (sum xs)
  ------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
  show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
  fix a xs
  assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
  have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))" 
    by simp
  also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
  also have "... = 2*a + 2*(sum xs)" using HI by simp
  also have "... = 2*(a + sum xs)" by simp
  also have "... = 2*(sum (a#xs))" by simp
  finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp
qed

-- "La demostración automática es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

text {* --------------------------------------------------------------- 
  Ejemplo 25. (p. 48) Demostrar que 
     longitud (map f xs) = longitud xs
  ------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
  show "longitud (map f []) = longitud []" by simp
next
  fix a xs
  assume HI: "longitud (map f xs) = longitud xs"
  have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp
  also have "... = 1 + longitud (map f xs)" by simp
  also have "... = 1 + longitud xs" using HI by simp
  also have "... = longitud (a#xs)" by simp
  finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp
qed

-- "La demostración automática es"
lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

section {* Referencias *}

text {*
  · J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
  · G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
    programms". 
  · S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
    Edition. Cap. 8 "Reasoning about programms". 
  · L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6. 
    "Reasoning about functional programs". 
*}

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

232

233

234

235

236

237

238

239

240

header {* Tema 3: Razonamiento estructurado sobre programas *}

theory T3

imports Main

begin

section {* Razonamiento por casos *}

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

Ejemplo 17. Definir la función

esVacia :: 'a list ⇒ bool

tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,

esVacia [] = True

esVacia [1] = False

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

fun esVacia :: "'a list ⇒ bool" where

"esVacia [] = True"

| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"

value "esVacia [1]" -- "= False"

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

Ejemplo 18 (p. 39) . Demostrar que

esVacia xs = esVacia (conc xs xs)

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

-- "La demostración estructurada es"

lemma "esVacia xs = esVacia (conc xs xs)"

proof (cases xs)

assume "xs = []"

then show "esVacia xs = esVacia (conc xs xs)" by simp

fix y ys

assume "xs = y#ys"

then show "esVacia xs = esVacia (conc xs xs)" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· "(cases xs)" es el método de demostración por casos según xs.

· Se generan dos subobjetivos correspondientes a los dos

constructores de listas:

· 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)

· 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)

· "then" indica "usando la propiedad anterior"

-- "La demostración estructurada simplificada es"

lemma "esVacia xs = esVacia (conc xs xs)"

proof (cases xs)

case Nil

then show "esVacia xs = esVacia (conc xs xs)" by simp

case Cons

then show "esVacia xs = esVacia (conc xs xs)" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· "case Nil" es una abreviatura de "assume xs = []"

· "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"

· "thus" es una abreviatura de "then show".

-- "La demostración automática es"

lemma "esVacia xs = esVacia (conc xs xs)"

by (cases xs) auto

section {* Heurística de generalización *}

text {*

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). *}

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

fun inversaAc :: "'a list ⇒ 'a list" where

"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

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

Ejemplo 20. (p. 44) Demostrar que

inversaAcAux xs ys = (inversa xs) @ ys

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

-- "La demostración estructurada es"

lemma inversaAcAux_es_inversa:

"inversaAcAux xs ys = (inversa xs) @ ys"

proof (induct xs arbitrary: ys)

show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp

fix a xs

assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"

show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"

proof -

fix ys

have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp

also have "… = inversa xs@(a#ys)" using HI by simp

also have "… = inversa (a#xs)@ys" by simp

finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp

qed

text {*

Comentarios sobre la demostración anterior:

· "(induct xs arbitrary: ys)" es el método de demostración por

inducción sobre xs usando ys como variable arbitraria.

· Se generan dos subobjetivos:

· 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys

· 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹

inversaAcAux (a # xs) ys = inversa (a # xs) @ ys

· Dentro de una demostración se pueden incluir otras demostraciones.

· Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una

lista arbitraria (con "fix ys") y se demuestra "P(ys)".

-- "La demostración automática es"

lemma "inversaAcAux xs ys = (inversa xs)@ys"

by (induct xs arbitrary: ys) auto

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

Ejemplo 21. (p. 43) Demostrar que

inversaAc xs = inversa xs

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

-- "La demostración automática es"

corollary "inversaAc xs = inversa xs"

by (simp add: inversaAcAux_es_inversa)

text {*

Comentario de la demostración anterior:

· "(simp add: inversaAcAux_es_inversa)" es el método de demostración

por simplificación usando como regla de simplificación la propiedad

inversaAcAux_es_inversa.

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,2,5] = [6,4,10]

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

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

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

Ejemplo 24. (p. 45) Demostrar que

sum (map (λx. 2*x) xs) = 2 * (sum xs)

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

-- "La demostración estructurada es"

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"

proof (induct xs)

show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp

fix a xs

assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"

have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))"

by simp

also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp

also have "... = 2*a + 2*(sum xs)" using HI by simp

also have "... = 2*(a + sum xs)" by simp

also have "... = 2*(sum (a#xs))" by simp

finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp

qed

-- "La demostración automática es"

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"

by (induct xs) auto

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

Ejemplo 25. (p. 48) Demostrar que

longitud (map f xs) = longitud xs

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

-- "La demostración estructurada es"

lemma "longitud (map f xs) = longitud xs"

proof (induct xs)

show "longitud (map f []) = longitud []" by simp

fix a xs

assume HI: "longitud (map f xs) = longitud xs"

have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp

also have "... = 1 + longitud (map f xs)" by simp

also have "... = 1 + longitud xs" using HI by simp

also have "... = longitud (a#xs)" by simp

finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp

qed

-- "La demostración automática es"

lemma "longitud (map f xs) = longitud xs"

by (induct xs) auto

section {* Referencias *}

text {*

· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3

· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about

programms".

· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd

Edition. Cap. 8 "Reasoning about programms".

· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.

"Reasoning about functional programs".

end

Como tarea para la próxima clase se propuso la resolución de los ejercicios de la relación 4.

Se puede imprimir o compartir con