PDF de programación - Introducción a la demostración asistida por ordenador (con Isabelle/Isar)

Introducción a la demostración asistida

por ordenador (con Isabelle/Isar)

José A. Alonso Jiménez

Grupo de Lógica Computacional
Dpto. de Ciencias de la Computación e Inteligencia Artificial
Universidad de Sevilla
Sevilla, 5 de abril de 2008 (versión de 26 de mayo de 2009)

2

Índice

1

.

.

.

.

.

.

Introducción .

7
Isabelle como un lenguaje funcional
7
1.1
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 N úmeros naturales, enteros y booleanos . . . . . . . . . . . . . . . . . . . .
7
1.3 Definiciones no recursivas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
1.4 Definiciones locales . .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
. .
1.5 Pares .
. .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.6 Listas .
. .
. .
1.7 Registros .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
. .
1.8 Funciones anónimas
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
.
1.9 Condicionales .
. .
. .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.10 Tipos de datos y recursión primitiva . . . . . . . . . . . . . . . . . . . . . . 14

. .
. .
. .

. .
. .
. .

2 El lenguaje de demostración Isar

15
2.1 Panorama de la sintaxis (simplificada) de Isar . . . . . . . . . . . . . . . . . 15
2.2 Razonamiento proposicional . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.3 Atajos de Isar
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.4 Cuantificadores universal y existencial . . . . . . . . . . . . . . . . . . . . . 21
2.5 Razonamiento ecuacional
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

.

.

.

.

.

3 Distinción de casos e inducción

27
3.1 Razonamiento por distinción de casos . . . . . . . . . . . . . . . . . . . . . 27
3.1.1 Distinción de casos booleanos . . . . . . . . . . . . . . . . . . . . . . 27
3.1.2 Distinción de casos sobre otros tipos de datos
. . . . . . . . . . . . 28
Inducción matemática . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
Inducción estructural .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31

3.2
3.3

4 Patrones de demostración

35
4.1 Demostraciones por casos . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
4.2 Negación .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
4.3 Contradicciones . .
4.4 Equivalencias .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

.
.
. .
. .

.

.

.

.

.

3

4

Índice

5 Heurísticas para la inducción y recursion general

41
5.1 Heurísticas para la inducción . . . . . . . . . . . . . . . . . . . . . . . . . . 41
5.2 Recursión general. La función de Ackermann . . . . . . . . . . . . . . . . . 43
5.3 Recursión mutua e inducción . . . . . . . . . . . . . . . . . . . . . . . . . . 45

6 Caso de estudio: Compilación de expresiones

49
6.1 Las expresiones y el intérprete . . . . . . . . . . . . . . . . . . . . . . . . . . 49
6.2 La máquina de pila .
.
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
6.3 El compilador .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
. .
6.4 Corrección del compilador . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

.

Índice

5

6

Índice

Capítulo 1

Isabelle como un lenguaje funcional

1.1

Introducción

Nota 1.1.1. Esta notas son una introducción a la demostración asistida utilizando el sis-
tema Isabelle/HOL/Isar. La versión de Isabelle utilizada es la de 2009.

Nota 1.1.2. Un lema introduce una proposición seguida de una demostración. Isabelle
dispone de varios procedimientos automáticos para generar demostraciones, uno de los
cuales es el de simplificación (llamado simp). El procedimiento simp aplica un conjunto
de reglas de reescritura que inicialmente contiene un gran n úmero de reglas relativas a
los objetos definidos. El ejemplo del lema más trivial es el siguiente

lemma elMasTrivial: True
by simp

En este capítulos se presenta el lenguaje funcional que está incluido en Isabelle. El
lenguaje funcional es muy parecido al ML estándard.

1.2 N úmeros naturales, enteros y booleanos

Nota 1.2.1 (N úmeros naturales).

• En Isabelle están definidos los n úmero naturales con la sintaxis de Peano usando

dos constructores: 0 (cero) y Suc n (el sucesor de n).

• Los n úmeros como el 1 son abreviaturas de los correspondientes en la notación de

Peano, en este caso Suc 0.

• El tipo de los n úmeros naturales es nat.

7

8

Capítulo 1. Isabelle como un lenguaje funcional

Lema 1.2.2 (Ejemplo de simplificación de n úmeros naturales). El siguiente del 0 es el 1.

lemma Suc 0 = 1
by simp

Nota 1.2.3 (Suma y producto de n úmeros naturales). En Isabelle están definida la suma
y el producto de n úmeros naturales:

• x+y es la suma de x e y
• x∗y es el producto de x e y

Lema 1.2.4 (Ejemplo de suma). La suma de los números naturales 1 y 2 es el número natural
3.

lemma 1 + 2 = (3::nat)
by simp

Nota 1.2.5 (Epecificación de tipo). La notación del par de dos puntos se usa para asignar
un tipo a un término (por ejemplo, 3::nat significa que se considera que 3 es un n úmero
natural).

Lema 1.2.6 (Ejemplo de producto). El producto de los números naturales 2 y 3 es el número
natural 6.
lemma 2 ∗ 3 = (6::nat)
by simp

Nota 1.2.7 (División de n úmeros naturales). En Isabelle está definida la división de
n úmeros naturales: n div m es el mayor n úmero natural que multiplicado por m es
menor o igual que n.

Lema 1.2.8 (Ejemplo de división). La división natural de 7 entre 3 es 2.

lemma 7 div 3 = (2::nat)
by simp

Nota 1.2.9 (Resto de división de n úmeros naturales). En Isabelle está definida el resto
de n úmeros naturales: n mod m es el resto de dividir n entre m.

Lema 1.2.10 (Ejemplo de resto). El resto de dividir 7 entre 3 es 1.

lemma 7 mod 3 = (1::nat)
by simp

1.2. N úmeros naturales, enteros y booleanos

9

Nota 1.2.11 (N úmeros enteros). En Isabelle también están definidos los n úmeros enteros.
El tipo de los enteros se representa por int.

Lema 1.2.12 (Ejemplo de operación con enteros). La suma de 1 y -2 es el número entero -1.
lemma 1 + −2 = (−1::int)
by simp

Nota 1.2.13 (Sobrecarga). Los numerales están sobrecargados. Por ejemplo, el ’1’ puede
ser un natural o un entero, dependiendo del contexto. Isabelle resuelve ambig ¨uedades
mediante inferencia de tipos. A veces, es necesario usar declaraciones de tipo para
resolver la ambig ¨uedad.

Nota 1.2.14 (Booleanos, conectivas y cuantificadores). En Isabelle están definidos los
valores booleanos (True y False), las conectivas (¬, ∧, ∨, →, ↔) y los cuantificadores (∀,
∃). El tipo de los booleanos es bool.
Lema 1.2.15 (Ejemplos de evaluaciones booleanas).

1. La conjunción de dos fórmulas verdaderas es verdadera.

2. La conjunción de un fórmula verdadera y una falsa es falsa.

3. La disyunción de una fórmula verdadera y una falsa es verdadera.

4. La disyunción de dos fórmulas falsas es falsa.

5. La negación de una fórmula verdadera es falsa.

6. Una fórmula falsa implica una fórmula verdadera.

7. Todo elemento es igual a sí mismo.

8. Existe un elemento igual a 1.

lemma True ∧ True = True
by simp
lemma True ∧ False = False
by simp
lemma True ∨ False = True
by simp
lemma False ∨ False = False

10

Capítulo 1. Isabelle como un lenguaje funcional

by simp
lemma ¬ True = (False::bool)
by simp
lemma False −→ True
by simp
lemma ∀ x. x = x
by simp
lemma ∃ x. x = 1
by simp

1.3 Definiciones no recursivas

Definición 1.3.1 (Ejemplo de definición no recursiva). La disyunción exclusiva de A y B se
verifica si una es verdadera y la otra no lo es.
definition xor :: bool ⇒ bool ⇒ bool where
xor A B ≡ (A ∧ ¬ B) ∨ (¬ A ∧ B)

Lema 1.3.2 (Ejemplo de demostración con definiciones no recursivas). La disyunción ex-
clusiva de dos fórmulas verdaderas es falsa.

Demostración: Por simplificación, usando la definición de la disyunción exclusiva.



lemma xor True True = False
by (simp add: xor-def )

Nota 1.3.3 (Ejemplo de ampliación de las reglas de simplificación). Se a ñade la definición
de la disyunción exlusiva al conjunto de reglas de simplificación automáticas.

declare xor-def [simp]

1.4 Definiciones locales

Nota 1.4.1 (Variables locales). Se puede asignar valores a variables locales mediante ’let’
y usarlo en las expresiones dentro de ’in’.

1.5. Pares

11

Lema 1.4.2 (Ejemplo de entorno local). Sea x el número natural 3. Entonces x × x = 9.
lemma (let x = 3::nat in x ∗ x = 9)
by simp

1.5 Pares

Nota 1.5.1 (Pares).

• Un par se representa escribiendo los elementos entre paréntesis y separados por

coma.

• El tipo de los pares es el producto de los tipos.
• La función fst devuelve el primer elemento de un par y la snd el segundo.

Lema 1.5.2 (Ejemplo de uso de pares). Sea p el par de números naturales (2, 3). La suma del
primer elemento de p y 1 es igual al segundo elemento de p.
lemma let p = (2,3)::nat × nat in fst p + 1 = snd p
by simp

1.6 Listas

Nota 1.6.1 (Construcción de listas).

• Una lista se representa escribiendo los elementos entre corchetes y separados por

coma.

• La lista vacía se representa por [].
• Todos los elementos de una lista tienen que ser del mismo tipo.
• El tipo de las listas de elementos del tipo a es a list.
• El término a#l representa la lista obtenida a ñadiendo el elemento a al principio de

la lista l.

Lema 1.6.2 (Ejemplo de construcción de listas). La lista obtenida añadiendo sucesivamente a
la lista vacía los elementos 3, 2 y 1 es [1,2,3].

lemma 1#(2#(3#[])) = [1,2,3]
by simp

12

Capítulo 1. Isabelle como un lenguaje funcional

Nota 1.6.3 (Primero y resto).

• hd l es el primer elemento de la lista l.
• tl l es el resto de la lista l.

Lema 1.6.4 (Ejemplo de cálculo con listas). Sea l la lista de números naturales [1,2,3].
Entonces, el primero de l e