Menu Close

RA2019: Razonamiento sobre programas con Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la 1ª relación.

En la segunda parte, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 8 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:

chapter ‹Tema 2: Razonamiento sobre programas›
 
theory T2_Razonamiento_sobre_programas
imports Main 
begin
 
text ‹En este tema se demuestra con Isabelle las propiedades de los
  programas funcionales como se expone en el tema 8 del curso
  "Informática" que puede leerse en
  https://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8.pdf › 
 
declare [[names_short]]
 
section ‹Razonamiento ecuacional›
 
text-----------------------------------------------------------------
  Ejemplo 1. Definir, por recursión, la función
     longitud :: 'a list ⇒ nat
  tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
     longitud [a,c,d] = 3
  --------------------------------------------------------------------›
 
fun longitud :: "'a list ⇒ nat" where
  "longitud []     = 0"
| "longitud (x#xs) = 1 + longitud xs"
 
value "longitud [a,c,d] = 3"
 
text ‹La definición de la función longitud genera dos regla de
  simplificación
  · longitud.simps(1): longitud [] = 0
  · longitud.simps(2): longitud (?x # ?xs) = 1 + longitud ?xs
 
  Se pueden ver con 
  · thm longitud.simps(1)
  · thm longitud.simps(2)
›
 
thm longitud.simps(1)
(* da longitud [] = 0 *)
 
thm longitud.simps(2)
(* da longitud (?x # ?xs) = 1 + longitud ?xs *)
 
text---------------------------------------------------------------
  Ejemplo 2. Demostrar que 
     longitud [a,c,d] = 3
  ------------------------------------------------------------------- ›
 
(* Demostración detallada *)
lemma "longitud [a,c,d] = 3"
  apply (simp only: longitud.simps(2))
  apply (simp only: longitud.simps(1))
  done
 
(* Demostración aplicativa no detallada  *)
lemma "longitud [a,c,d] = 3"
  apply simp
  done
 
(* Demostración automática *)
lemma "longitud [a,c,d] = 3"
  by simp
 
text--------------------------------------------------------------- 
  Ejemplo 3. Definir la función
     fun intercambia :: 'a × 'b ⇒ 'b × 'a
  tal que (intercambia p) es el par obtenido intercambiando las
  componentes del par p. Por ejemplo,
     intercambia (u,v) = (v,u)
  ------------------------------------------------------------------ ›
 
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
  "intercambia (x,y) = (y,x)"
 
value "intercambia (u,v) = (v,u)"
 
text ‹La definición de la función intercambia genera una regla de
  simplificación
  · intercambia.simps: intercambia (x,y) = (y,x)
 
  Se puede ver con 
  · thm intercambia.simps 
›
 
thm intercambia.simps
(* da intercambia (?x, ?y) = (?y, ?x) *)
 
text--------------------------------------------------------------- 
  Ejemplo 4. (p.6) Demostrar que 
     intercambia (intercambia (x,y)) = (x,y)
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  apply (simp only: intercambia.simps)
  done
 
(* Demostración aplicativa no detallada *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  apply simp
  done
 
(* Demostración automática *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by simp 
 
text--------------------------------------------------------------- 
  Ejemplo 5. Definir, por recursión, la función
     inversa :: 'a list ⇒ 'a list
  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
  elementos de xs. Por ejemplo,
     inversa [a,d,c] = [c,d,a]
  ------------------------------------------------------------------ ›
 
fun inversa :: "'a list ⇒ 'a list" where
  "inversa []     = []"
| "inversa (x#xs) = inversa xs @ [x]"
 
value "inversa [a,d,c] = [c,d,a]"
 
text--------------------------------------------------------------- 
  Ejemplo 6. (p. 9) Demostrar que 
     inversa [x] = [x]
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "inversa [x] = [x]"
  apply (simp only: inversa.simps(2)) 
  apply (simp only: inversa.simps(1)) 
  apply (simp only: append_Nil)       
  done
 
(* Nota: El nombre del último simplificador se busca con *)
find_theorems "[] @ _ = _"
 
(* También se puede buscar con la pestaña Query *)
 
(* Demostración aplicativa no detallada *)
lemma "inversa [x] = [x]"
  apply simp
  done
 
(* Demostración automática *)
lemma "inversa [x] = [x]"
  by simp
 
section ‹Razonamiento por inducción sobre los naturales›
 
text[Principio de inducción sobre los naturales] Para demostrar una
  propiedad P para todos los números naturales basta probar que el 0
  tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
  también la tiene.  
     ⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m
 
  En Isabelle el principio de inducción sobre los naturales está
  formalizado en el teorema nat.induct y puede verse con
     thm nat.induct
›
 
thm nat.induct
 
text--------------------------------------------------------------- 
  Ejemplo 7. Definir la función
     repite :: nat ⇒ 'a ⇒ 'a list
  tal que (repite n x) es la lista formada por n copias del elemento
  x. Por ejemplo, 
     repite 3 a = [a,a,a]
  ------------------------------------------------------------------ ›
 
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
  "repite 0 x       = []"
| "repite (Suc n) x = x # (repite n x)"
 
value "repite 3 a = [a,a,a]"
 
text--------------------------------------------------------------- 
  Ejemplo 8. (p. 18) Demostrar que 
     longitud (repite n x) = n
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa *)
lemma "longitud (repite n x) = n"
  apply (induct n) 
   apply (simp only: repite.simps(1))
   apply (simp only: longitud.simps(1))
  apply (simp only: repite.simps(2))
  apply (simp only: longitud.simps(2))
  done
 
(* Demostración aplicativa no detallada *)
lemma "longitud (repite n x) = n"
  apply (induct n) 
   apply simp      
  apply simp       
  done
 
(* Demostración aplicativa con simp_all *)
lemma "longitud (repite n x) = n"
  apply (induct n) 
   apply simp_all  
  done
 
(* Demostración automática *)
lemma "longitud (repite n x) = n"
  by (induct n) simp_all
 
section ‹Razonamiento por inducción sobre listas›
 
text ‹Para demostrar una propiedad para todas las listas basta demostrar
  que la lista vacía tiene la propiedad y que al añadir un elemento a
  una lista que tiene la propiedad se obtiene otra lista que también
  tiene la propiedad. 
 
  En Isabelle el principio de inducción sobre listas está formalizado
  mediante el teorema list.induct 
     ⟦P []; 
      ⋀x xs. P xs ⟹ P (x#xs)⟧ 
     ⟹ P xs
›
 
thm list.induct
 
text--------------------------------------------------------------- 
  Ejemplo 9. Definir la función
     conc :: 'a list ⇒ 'a list ⇒ 'a list
  tal que (conc xs ys) es la concatención de las listas xs e ys. Por
  ejemplo, 
     conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
  ------------------------------------------------------------------ ›
 
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
  "conc []     ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"
 
value "conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]"
 
text--------------------------------------------------------------- 
  Ejemplo 10. (p. 24) Demostrar que 
     conc xs (conc ys zs) = (conc xs ys) zs
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  apply (induct xs) 
   apply (simp only: conc.simps(1))  
  apply (simp only: conc.simps(2))   
  done  
 
(* Demostración aplicativa no detallada *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  apply (induct xs) 
   apply simp_all   
  done  
 
(* Demostración automática *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  by (induct xs) simp_all
 
text--------------------------------------------------------------- 
  Ejemplo 11. Refutar que 
     conc xs ys = conc ys xs
  ------------------------------------------------------------------- ›
 
lemma "conc xs ys = conc ys xs"
  quickcheck
  oops
 
text ‹Encuentra el contraejemplo, 
  xs = [a2]
  ys = [a1]›
 
text--------------------------------------------------------------- 
  Ejemplo 12. (p. 28) Demostrar que 
     conc xs [] = xs
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "conc xs [] = xs"
  apply (induct xs) 
   apply (simp only: conc.simps(1))
  apply (simp only: conc.simps(2))
  done  
 
(* Demostración aplicativa no detallada *)
lemma "conc xs [] = xs"
  apply (induct xs) 
   apply simp_all   
  done  
 
(* Demostración automática *)
lemma "conc xs [] = xs"
  by (induct xs) simp_all
 
text--------------------------------------------------------------- 
  Ejemplo 13. (p. 30) Demostrar que 
     longitud (conc xs ys) = longitud xs + longitud ys
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
  apply (induct xs)  
   apply (simp only: conc.simps(1))
   apply (simp only: longitud.simps(1))
  apply (simp only: conc.simps(2)) 
  apply (simp only: longitud.simps(2))
  done  
 
(* Demostración aplicativa *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
  apply (induct xs)  
   apply simp_all   
  done  
 
(* Demostración automática *)
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
  by (induct xs) simp_all
 
section ‹Inducción correspondiente a la definición recursiva›
 
text--------------------------------------------------------------- 
  Ejemplo 14. Definir la función
     coge :: nat ⇒ 'a list ⇒ 'a list
  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por 
  ejemplo, 
     coge 2 [a,c,d,b,e] = [a,c]
  ------------------------------------------------------------------ ›
 
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
  "coge n []           = []"
| "coge 0 xs           = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"
 
value "coge 2 [a,c,d,b,e] = [a,c]"
 
text--------------------------------------------------------------- 
  Ejemplo 15. Definir la función
     elimina :: nat ⇒ 'a list ⇒ 'a list
  tal que (elimina n xs) es la lista obtenida eliminando los n primeros
  elementos de xs. Por ejemplo, 
     elimina 2 [a,c,d,b,e] = [d,b,e]
  ------------------------------------------------------------------ ›
 
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
  "elimina n []           = []"
| "elimina 0 xs           = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"
 
value "elimina 2 [a,c,d,b,e] = [d,b,e]"
 
text ‹ 
  La definición coge genera el esquema de inducción coge.induct:
     ⟦⋀n. P n []; 
      ⋀x xs. P 0 (x#xs); 
      ⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
     ⟹ P n x
 
  Puede verse usando "thm coge.induct". ›
 
thm coge.induct
 
text--------------------------------------------------------------- 
  Ejemplo 16. (p. 35) Demostrar que 
     conc (coge n xs) (elimina n xs) = xs
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  apply (induct rule: coge.induct) 
    apply (simp only: coge.simps(1))
    apply (simp only: elimina.simps(1))
    apply (simp only: conc.simps(1))
   apply (simp only: coge.simps(2))
   apply (simp only: elimina.simps(2))
   apply (simp only: conc.simps(1))
   apply (simp only: coge.simps(3))
   apply (simp only: elimina.simps(3))
  apply (simp only: conc.simps(2))
  done
 
(* Demostración aplicativa no detallada *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  apply (induct rule: coge.induct) 
    apply simp_all
  done
 
(* Demostración automática *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  by (induct rule: coge.induct) simp_all
 
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 [a] = False"
 
text--------------------------------------------------------------- 
  Ejemplo 18 (p. 39) . Demostrar que 
     esVacia xs = esVacia (conc xs xs)
  ------------------------------------------------------------------- ›
 
(* Demostración aplicativa detallada *)
lemma "esVacia xs = esVacia (conc xs xs)"
  apply (cases xs) 
   apply (simp only: esVacia.simps(1))
   apply (simp only: conc.simps(1))
   apply (simp only: esVacia.simps(1))
  apply (simp only: esVacia.simps(2))
  apply (simp only: conc.simps(2))
  apply (simp only: esVacia.simps(2))
  done
 
(* Demostración aplicativa *)
lemma "esVacia xs = esVacia (conc xs xs)"
  apply (cases xs) 
   apply simp_all
  done
 
(* Demostración automática *)
lemma "esVacia xs = esVacia (conc xs xs)"
  by (cases xs) simp_all
 
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 se propuso la resolución de los ejercicios de la 2ª relación.

RA2019