RA2018: Definiciones inductivas en IsabelleHOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.

La clase se ha basado en la siguiente teoría Isabelle

chapter {* Tema 11: Definiciones inductivas *}

theory T11_Definiciones_inductivas
imports Main
begin

section {* El conjunto de los números pares *}

text {* 
  · El conjunto de los números pares se define inductivamente como el
    menor conjunto que contiene al 0 y es cerrado por la operación (+2).

  · El conjunto de los números pares también puede definirse como los 
    naturales divisible por 2.

  · Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
    se demuestra su equivalencia.
*}

subsection {* Definición inductiva del conjunto de los pares *}

inductive_set par :: "nat set" where
  cero [intro!]: "0 ∈ par" 
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"

text {*
  · Una definición inductiva está formada con reglas de introducción.

  · La definición inductiva genera varios teoremas:
    · par.cero:   0 ∈ par
    · par.paso:   n ∈ par ⟹ Suc (Suc n) ∈ par
    · par.simps:  (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))
*}

subsection {* Uso de las reglas de introducción *}

text {*
  Lema: Los números de la forma 2*k son pares.
*}

― ‹La demostración automática es›
lemma dobles_son_pares [intro!]: 
  "2*k ∈ par"
by (induct k) auto

― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
  "2*k ∈ par"
proof (induct k)
  show "2 * 0 ∈ par" by auto
next
  show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
qed

text {*
  · Nota: Nuestro objetivo es demostrar la equivalencia de la definición
    anterior y la definición mediante divisibilidad (even).
  
  · Lema: Si n es divisible por 2, entonces es par.
*}

lemma even_imp_par: "even n ⟹ n ∈ par"
by auto

subsection {* Regla de inducción *} 

text {*
  Entre las reglas generadas por la definión de par está la de
  inducción:
  · par.induct: ⟦ x ∈ par; 
                 P 0; 
                 ⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧ 
                ⟹ P x
*}

text {*
  Lema: Los números pares son divisibles por 2.
*} 

― ‹1ª demostración (detallada)›
lemma par_imp_even: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed

― ‹2ª demostración (con arith)›
lemma par_imp_even_2: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed

― ‹3ª demostración (automática)›
lemma par_imp_even_3: 
  "n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)

text {*
  Lema: Un número n es par syss es divisible por 2. 
*}

theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)

subsection{* Generalización y regla de inducción *}

text {*
  · Antes de aplicar inducción se debe de generalizar la fórmula a
    probar.
 
  · Vamos a ilustrar el principio anterior en el caso de los conjuntos
    inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
    entonces n también lo es.

  · El siguiente intento falla:
*}

lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
  apply (erule par.induct) 
oops

text {*
  En el intento anterior, los subobjetivos generados son
     1. n ∈ par
     2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
  que no se pueden demostrar.

  Se ha perdido la información sobre Suc (Suc n).
*}

text {*
  Reformulación del lema: Si n es par, entonces n-2 también lo es.
*}

― ‹La demostración automática es›
lemma par_imp_par_menos_2: 
  "n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto

― ‹La demostración estructurada es›
lemma "n ∈  par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
  show "0 - 2 ∈ par" by auto
next
  show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed

text {* 
  Con el lema anterior se puede demostrar el original.
*}

― ‹La demostración estructurada es›
lemma
  assumes "Suc (Suc n) ∈ par" 
  shows   "n ∈ par"
proof -
  have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)
  then show "n ∈ par" by simp 
qed

― ‹La demostración aplicativa es›
lemma 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2) 
apply simp
done

(* Comentar el uso de drule *)

― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par: 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
by (drule par_imp_par_menos_2, simp)

text {*
  Lemma. Un número natural n es par syss n+2 es par.
*}

lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)

text {*
  Se usa el atributo "iff" porque sirve como regla de simplificación.
*}

subsection {* Definiciones mutuamente inductivas *}

text {*
  Definición cruzada de los conjuntos inductivos de los pares y de los 
  impares:
*}

inductive_set
  Pares    :: "nat set" and
  Impares  :: "nat set"
where
  ceroP:    "0 ∈ Pares"
| ParesI:   "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares   ⟹ Suc n ∈ Impares"

text {*
  El esquema de inducción generado por la definición anterior es
  · Pares_Impares.induct:
    ⟦P1 0; 
     ⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
     ⋀n. ⟦n ∈ Pares;   P1 n⟧ ⟹ P2 (Suc n)⟧
    ⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)
*}

text {*
  Ejemplo de demostración usando el esquema anterior.
*}

lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
  show "even (0::nat)" by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Impares" and
         H2: "even (Suc n)"
  show "even (Suc n)" using H2 by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Pares" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed

subsection {* Definición inductiva de predicados *}

text {*
  Definición inductiva del predicado es_par tal que (es_par n) se
  verifica si n es par.
*}

inductive es_par :: "nat ⇒ bool" where
  "es_par 0" 
| "es_par n ⟹ es_par (Suc(Suc n))"

text {*
  Heurística para elegir entre definir conjuntos o predicados:
  · si se va a combinar con operaciones conjuntistas, definir conjunto;
  · en caso contrario, definir predicado.
*}

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

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

chapter {* Tema 11: Definiciones inductivas *}

theory T11_Definiciones_inductivas

imports Main

begin

section {* El conjunto de los números pares *}

text {*

· El conjunto de los números pares se define inductivamente como el

menor conjunto que contiene al 0 y es cerrado por la operación (+2).

· El conjunto de los números pares también puede definirse como los

naturales divisible por 2.

· Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo

se demuestra su equivalencia.

subsection {* Definición inductiva del conjunto de los pares *}

inductive_set par :: "nat set" where

cero [intro!]: "0 ∈ par"

| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"

text {*

· Una definición inductiva está formada con reglas de introducción.

· La definición inductiva genera varios teoremas:

· par.cero: 0 ∈ par

· par.paso: n ∈ par ⟹ Suc (Suc n) ∈ par

· par.simps: (a ∈ par) = (a = 0 ∨ (∃n. a = Suc (Suc n) ∧ n ∈ par))

subsection {* Uso de las reglas de introducción *}

text {*

Lema: Los números de la forma 2*k son pares.

― ‹La demostración automática es›

lemma dobles_son_pares [intro!]:

"2*k ∈ par"

by (induct k) auto

― ‹La demostración estructurada es›

lemma dobles_son_pares_2:

"2*k ∈ par"

proof (induct k)

show "2 * 0 ∈ par" by auto

show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto

qed

text {*

· Nota: Nuestro objetivo es demostrar la equivalencia de la definición

anterior y la definición mediante divisibilidad (even).

· Lema: Si n es divisible por 2, entonces es par.

lemma even_imp_par: "even n ⟹ n ∈ par"

by auto

subsection {* Regla de inducción *}

text {*

Entre las reglas generadas por la definión de par está la de

inducción:

· par.induct: ⟦ x ∈ par;

P 0;

⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧

⟹ P x

text {*

Lema: Los números pares son divisibles por 2.

― ‹1ª demostración (detallada)›

lemma par_imp_even:

"n ∈ par ⟹ even n"

proof (induction rule: par.induct)

show "2 dvd (0::nat)" by (simp_all add: dvd_def)

fix n::nat

assume H1: "n ∈ par" and

H2: "even n"

have "∃k. n = 2*k" using H2 by (simp add: dvd_def)

then obtain k where "n = 2*k" ..

then have "Suc (Suc n) = 2*(k+1)" by auto

then have "∃k. Suc (Suc n) = 2*k" ..

then show "even (Suc (Suc n))" by (simp add: dvd_def)

qed

― ‹2ª demostración (con arith)›

lemma par_imp_even_2:

"n ∈ par ⟹ even n"

proof (induction rule: par.induct)

show "even (0::nat)" by (simp_all add: dvd_def)

fix n::nat

assume H1: "n ∈ par" and

H2: "even n"

then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)

qed

― ‹3ª demostración (automática)›

lemma par_imp_even_3:

"n ∈ par ⟹ even n"

by (induction rule:par.induct) (auto simp add: dvd_def, arith)

text {*

Lema: Un número n es par syss es divisible por 2.

theorem par_iff_even: "(n ∈ par) = (even n)"

by (blast intro: even_imp_par par_imp_even)

subsection{* Generalización y regla de inducción *}

text {*

· Antes de aplicar inducción se debe de generalizar la fórmula a

probar.

· Vamos a ilustrar el principio anterior en el caso de los conjuntos

inductivamente definidos, con el siguiente ejemplo: si n+2 es par,

entonces n también lo es.

· El siguiente intento falla:

lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"

apply (erule par.induct)

oops

text {*

En el intento anterior, los subobjetivos generados son

1. n ∈ par

2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par

que no se pueden demostrar.

Se ha perdido la información sobre Suc (Suc n).

text {*

Reformulación del lema: Si n es par, entonces n-2 también lo es.

― ‹La demostración automática es›

lemma par_imp_par_menos_2:

"n ∈ par ⟹ n - 2 ∈ par"

by (induction rule:par.induct) auto

― ‹La demostración estructurada es›

lemma "n ∈ par ⟹ n - 2 ∈ par"

proof (induction rule:par.induct)

show "0 - 2 ∈ par" by auto

show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto

qed

text {*

Con el lema anterior se puede demostrar el original.

― ‹La demostración estructurada es›

lemma

assumes "Suc (Suc n) ∈ par"

shows "n ∈ par"

proof -

have "Suc (Suc n) - 2 ∈ par" using assms by (rule par_imp_par_menos_2)

then show "n ∈ par" by simp

qed

― ‹La demostración aplicativa es›

lemma

"Suc (Suc n) ∈ par ⟹ n ∈ par"

apply (drule par_imp_par_menos_2)

apply simp

done

(* Comentar el uso de drule *)

― ‹La demostración automática es›

lemma Suc_Suc_par_imp_par:

"Suc (Suc n) ∈ par ⟹ n ∈ par"

by (drule par_imp_par_menos_2, simp)

text {*

Lemma. Un número natural n es par syss n+2 es par.

lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"

by (blast dest: Suc_Suc_par_imp_par)

text {*

Se usa el atributo "iff" porque sirve como regla de simplificación.

subsection {* Definiciones mutuamente inductivas *}

text {*

Definición cruzada de los conjuntos inductivos de los pares y de los

impares:

inductive_set

Pares :: "nat set" and

Impares :: "nat set"

where

ceroP: "0 ∈ Pares"

| ParesI: "n ∈ Impares ⟹ Suc n ∈ Pares"

| ImparesI: "n ∈ Pares ⟹ Suc n ∈ Impares"

text {*

El esquema de inducción generado por la definición anterior es

· Pares_Impares.induct:

⟦P1 0;

⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);

⋀n. ⟦n ∈ Pares; P1 n⟧ ⟹ P2 (Suc n)⟧

⟹ (x1 ∈ Pares ⟶ P1 x1) ∧ (x2 ∈ Impares ⟶ P2 x2)

text {*

Ejemplo de demostración usando el esquema anterior.

lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"

proof (induction rule:Pares_Impares.induct)

show "even (0::nat)" by simp

fix n :: "nat"

assume H1: "n ∈ Impares" and

H2: "even (Suc n)"

show "even (Suc n)" using H2 by simp

fix n :: "nat"

assume H1: "n ∈ Pares" and

H2: "even n"

have "∃k. n = 2*k" using H2 by (simp add: dvd_def)

then obtain k where "n = 2*k" ..

then have "Suc (Suc n) = 2*(k+1)" by auto

then have "∃k. Suc (Suc n) = 2*k" ..

then show "even (Suc (Suc n))" by (simp add: dvd_def)

qed

subsection {* Definición inductiva de predicados *}

text {*

Definición inductiva del predicado es_par tal que (es_par n) se

verifica si n es par.

inductive es_par :: "nat ⇒ bool" where

"es_par 0"

| "es_par n ⟹ es_par (Suc(Suc n))"

text {*

Heurística para elegir entre definir conjuntos o predicados:

· si se va a combinar con operaciones conjuntistas, definir conjunto;

· en caso contrario, definir predicado.

end

Como ejercicio se propuso la relación 8 sobre gramáticas libres de contexto.

Se puede imprimir o compartir con