LMF2019: Razonamiento sobre programas con Isabelle/HOL (1º parte)

PorJosé A. Alonso 16 abril 202029 abril 2020

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell y cómo traducir dichas demostraciones a Isabelle/HOL.

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.

La traducción de los 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"

1	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"

1 2	lemma inversaAcAux_es_inversa: "inversaAcAux xs ys = (inversa xs)@ys"

De cada propiedad se han presentados distintas demostracciones:

automática,
aplicativa estructurada (usando simp)
aplicativa detallada (usando simp only)
declarativa estructurada (usando simp)
declarativa detallada (usando simp only)

La clase se ha dado mediante videoconferencia y el vídeo correspondiente a la primera parte es

y el de la segunda parte es

Las transparencia utilizadas son las 28 primeras páginas del tema

La teoría con los ejemplos presentados en la clase es la siguiente:

chapter ‹Tema 6: Razonamiento sobre programas›

theory T6_Razonamiento_sobre_programas
imports Main 
begin

text ‹En este tema se demuestra con Isabelle las propiedades de los
  programas funcionales de tema 6 http://bit.ly/2Za6YWY

  Para cada propiedades se presentan distintos tipos de demostraciones:
  automáticas, aplicativas y declarativas.› 

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 (_#xs) = 1 + longitud xs"
   
value "longitud [a,c,d]"

text ‹ --------------------------------------------------------------- 
  Ejemplo 2. Demostrar que 
     longitud [a,c,d] = 3
  ------------------------------------------------------------------- ›

lemma "longitud [a,c,d] = 3"
  apply simp
  done

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)"

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(1)
(* da intercambia (?x, ?y) = (?y, ?x) *)

text ‹ --------------------------------------------------------------- 
  Ejemplo 4. (p.6) Demostrar que 
     intercambia (intercambia (x,y)) = (x,y)
  ------------------------------------------------------------------- ›

(* Demostración automática *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by auto

(* Demostración automática 1 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by simp 

(* Demostración automática 2 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  by (simp only: intercambia.simps)

(* Demostración aplicativa *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
  apply (simp only: intercambia.simps)
  done

(* Demostración declarativa 1 *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
  have "intercambia (intercambia (x,y)) = intercambia (y,x)"  
    by simp
  also have "… = (x,y)" 
    by simp 
  finally show "intercambia (intercambia (x,y)) = (x,y)" 
    by simp
qed

(* Demostración detallada *)
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
  have "intercambia (intercambia (x,y)) = intercambia (y,x)"  
    by (simp only: intercambia.simps)
  also have "… = (x,y)" 
    by (simp only: intercambia.simps)
  finally show "intercambia (intercambia (x,y)) = (x,y)" 
    by this
qed

text ‹Notas sobre el lenguaje: En la demostración anterior se ha usado
  · "proof" para iniciar la prueba,
  · "-" (después de "proof") para no usar el método por defecto,
  · "have" para establecer un paso,
  · "by (simp only: intercambia.simps)" para indicar que sólo se usa
    como regla de escritura la correspondiente a la definición de
    intercambia,
  · "also" para encadenar pasos ecuacionales,
  · "…" para representar la derecha de la igualdad anterior en un
    razonamiento ecuacional,
  · "finally" para indicar el último pasa de un razonamiento ecuacional,
  · "show" para establecer la conclusión.
  · "by simp" para indicar el método de demostración por simplificación y 
  · "qed" para terminar la pruebas.›

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]
  ------------------------------------------------------------------- ›

(* La demostración automática es *)
lemma "inversa [x] = [x]"
  by simp

(* La demostración aplicativa es *)
lemma "inversa [x] = [x]"
  apply simp
  done

text ‹En la demostración anterior se usaron las siguientes reglas:
  · inversa.simps(1): inversa [] = []
  · inversa.simps(2): inversa (x#xs) = inversa xs @ [x]
  · append_Nil:       [] @ ys = ys
  Vamos a explicitar su aplicación.
›

thm inversa.simps(2)
thm append_Nil
thm append.simps
thm append.simps(1)

find_theorems
find_theorems "_ @ _ = _"
find_theorems "[] @ _ = _"

(* La demostración aplicativa detallada es *)
lemma "inversa [x] = [x]"
  apply (simp only: inversa.simps(2)) (* inversa [] @ [x] = [x] *)
  apply (simp only: inversa.simps(1)) (* [] @ [x] = [x] *)
  apply (simp only: append_Nil)       (* No subgoals! *)
  done

(* La demostración declarativa simplificada es *)
lemma "inversa [x] = [x]"
proof -
  have "inversa [x] = inversa (x#[])" 
    by simp
  also have "… = (inversa []) @ [x]" 
    by simp
  also have "… = [] @ [x]" 
    by simp
  also have "… = [x]" 
    by simp 
  finally show "inversa [x] = [x]" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "inversa [x] = [x]"
proof -
  have "inversa [x] = (inversa []) @ [x]" 
    by (simp only: inversa.simps(2))
  also have "… = [] @ [x]" 
    by (simp only: inversa.simps(1))
  also have "… = [x]" 
    by (simp only: append_Nil) 
  finally show "inversa [x] = [x]" 
    by this
qed

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
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "longitud (repite n x) = n"
  apply (induct n) (* 1. longitud (repite 0 x) = 0
                      2. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
   apply simp      (* 1. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
  apply simp       (* No subgoals *)
  done

(* La demostración aplicativa con simp_all es *)
lemma "longitud (repite n x) = n"
  apply (induct n) (* 1. longitud (repite 0 x) = 0
                      2. ⋀n. longitud (repite n x) = n ⟹
                         longitud (repite (Suc n) x) = Suc n *)
   apply simp_all  (* No subgoals *)
  done

(* La demostración automática es *)
lemma "longitud (repite n x) = n"
  by (induct n) simp_all

(* La demostración declarativa es *)
lemma "longitud (repite n x) = n"
proof (induct n)
  show "longitud (repite 0 x) = 0" 
    by simp
next 
  fix n
  assume HI: "longitud (repite n x) = n"
  have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" 
    by simp
  also have "… = 1 + longitud (repite n x)" 
    by simp
  also have "… = 1 + n" 
    using HI by simp
  finally show "longitud (repite (Suc n) x) = Suc n" 
    by simp
qed

text ‹Comentarios sobre la demostración anterior:
  · A la derecha de proof se indica el método de la demostración.
  · (induct n) indica que la demostración se hará por inducción en n.
  · Se generan dos subobjetivos correspondientes a la base y el paso de
    inducción:
    1. longitud (repite 0 x) = 0
    2. ⋀n. longitud (repite n x) = n ⟹ 
            longitud (repite (Suc n) x) = Suc n
    donde ⋀n se lee "para todo n".  
  · "next" indica el siguiente subobjetivo.
  · "fix n" indica "sea n un número natural cualquiera"
  · assume HI: "longitud (repite n x) = n" indica «supongamos que 
    "longitud (repite n x) = n" y sea HI la etiqueta de este supuesto».
  · "using HI" usando la propiedad etiquetada con HI. ›

(* La demostración declarativa detallada es *)
lemma "longitud (repite n x) = n"
proof (induct n)
  show "longitud (repite 0 x) = 0"
    by (simp only: repite.simps(1)
                   longitud.simps(1))
next 
  fix n
  assume HI: "longitud (repite n x) = n"
  have "longitud (repite (Suc n) x) = longitud (x # (repite n x))" 
    by (simp only: repite.simps(2))
  also have "… = 1 + longitud (repite n x)" 
    by (simp only: longitud.simps(2))
  also have "… = 1 + n" 
    using HI by (simp only:)
  also have "… = Suc n"
    (* find_theorems "Suc _ = _ + _" *)
    by (simp only: Suc_eq_plus1_left)
  finally show "longitud (repite (Suc n) x) = Suc n" 
    by this
qed

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
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  apply (induct xs) (*  1. conc [] (conc ys zs) = conc (conc [] ys) zs
                        2. ⋀a xs.
                              conc xs (conc ys zs) =
                              conc (conc xs ys) zs ⟹
                              conc (a # xs) (conc ys zs) =
                              conc (conc (a # xs) ys) zs *)
   apply simp_all   (* No subgoals! *)
  done  

(* La demostración automática es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
  by (induct xs) simp_all

(* La demostración declarativa es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
  show "conc [] (conc ys zs) = conc (conc [] ys) zs" 
    by simp
next
  fix x xs
  assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" 
  have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" 
    by simp
  also have "… = x # (conc (conc xs ys) zs)" 
    using HI by simp
  also have "… = conc (conc (x # xs) ys) zs" 
    by simp
  finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
  show "conc [] (conc ys zs) = conc (conc [] ys) zs" 
    by (simp only: conc.simps(1))
next
  fix x xs
  assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs" 
  have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" 
    by (simp only: conc.simps(2))
  also have "… = x # (conc (conc xs ys) zs)" 
    using HI by (simp only:)
  also have "… = conc (conc (x # xs) ys) zs" 
    by (simp only: conc.simps(2))
  finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" 
    by this
qed

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
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc xs [] = xs"
  apply (induct xs) (* 1. conc [] [] = []
                       2. ⋀a xs.
                             conc xs [] = xs ⟹
                             conc (a # xs) [] = a # xs *)
   apply simp_all   (* No subgoals! *)
  done  

(* La demostración automática es *)
lemma "conc xs [] = xs"
  by (induct xs) simp_all

(* declare [[show_types]] *)

(* La demostración declarativa es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" 
    by simp
next 
  fix x xs
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by simp
  also have "… = x # xs" 
    using HI by simp
  finally show "conc (x # xs) [] = x # xs" 
    by simp
qed


(* La demostración declarativa es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" by simp
next 
  fix x :: "'a" and xs :: "'a list"
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by simp
  also have "… = x # xs" 
    using HI by simp
  finally show "conc (x # xs) [] = x # xs" 
    by simp
qed

(* La demostración declarativa detallada es *)
lemma "conc xs [] = xs"
proof (induct xs)
  show "conc [] [] = []" 
    by (simp only: conc.simps(1))
next 
  fix x :: "'a" and xs :: "'a list"
  assume HI: "conc xs [] = xs" 
  have "conc (x # xs) [] = x # (conc xs [])" 
    by (simp only: conc.simps(2))
  also have "… = x # xs" 
    using HI by (simp only:)
  finally show "conc (x # xs) [] = x # xs" 
    by this
qed

end

1

2

3

Se puede imprimir o compartir con