En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comenzado el estudio de la demostración automática de propiedades de programas funcionales en Isabelle/HOL.
En primer lugar, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las [transparencias del tema 8][http://www.cs.us.es/~jalonso/cursos/i1m-16/temas/tema-8.pdf) del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.
A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.
El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,
|
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
|
lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys" |
La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son
- by simp: que es el método de simplificación por reescritura,
- by (induct x) auto: que es por inducción en x (donde x es un número natural o una lista) y simplificación automática de ambos casos,
- by (induct rule: fn.induct) auto: que es por inducción según la definición de la función fn y simplificación automática de todos los casos,
- by (simp add: lema_auxiliar): que es el método de simplificación por reescritura añadiéndole a las reglas de reescritura la correspondiente al lema_auxiliar,
La teoría con los ejemplos presentados en la clase es la siguiente:
Como tarea se propuso la resolución de los ejercicios de la 2ª relación.