RA2017: Razonamiento automático sobre programas en Isabelle/HOL
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,
|
1 |
lemma "longitud (repite n x) = n" |
También se puede poner un nombre al lema, por ejemplo,
|
1 2 |
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.