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

PorJosé A. Alonso 23 abril 202029 abril 2020
En la clase de hoy del curso de Lógica matemática y fundamentos se ha concluido el estudio, iniciado en la clase anterior, de 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.
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 los vídeos correspondientes son:
Primera parte:
Segunda parte:
Tercera parte:
Las transparencia utilizadas son las del tema a partir de la página 29.
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
chapter ‹Tema 6: Razonamiento sobre programas›

theory T6_Razonamiento_sobre_programas
imports Main 
begin

text ‹--------------------------------------------------------------- 
  Ejemplo 13. (p. 30) Demostrar que 
     longitud (conc xs ys) = longitud xs + longitud ys
  ------------------------------------------------------------------- ›

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

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

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

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

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 xs

  Puede verse usando "thm coge.induct". ›

thm elimina.induct
thm coge.induct

text ‹--------------------------------------------------------------- 
  Ejemplo 16. (p. 35) Demostrar que 
     conc (coge n xs) (elimina n xs) = xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  apply (induct rule: coge.induct) 
      (*  1. ⋀n. conc (coge n []) (elimina n []) = []
          2. ⋀v va. conc (coge 0 (v # va)) (elimina 0 (v # va)) =
                     v # va
          3. ⋀n x xs. conc (coge n xs) (elimina n xs) = xs ⟹
                       conc (coge (Suc n) (x # xs)) 
                            (elimina (Suc n) (x # xs)) =
                       x # xs *)
    apply simp_all
      (* No subgoals! *)
  done

(* La demostración automática es *)
lemma "conc (coge n xs) (elimina n xs) = xs"
  by (induct rule: coge.induct) simp_all

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

text ‹Comentario sobre la demostración anterior:
  · (induct rule: coge.induct) indica que el método de demostración es
    por el esquema de inducción correspondiente a la definición de la
    función coge.
  · Se generan 3 subobjetivos:
    · 1. ⋀n. conc (coge n []) (elimina n []) = []
    · 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs
    · 3. ⋀n x xs. 
            conc (coge n xs) (elimina n xs) = xs ⟹
            conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs
›

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

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

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

(* La demostración automática es *)
lemma "esVacia xs = esVacia (conc xs xs)"
  by (cases xs) simp_all

(* La demostración declarativa es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  assume "xs = []"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
next
  fix y ys
  assume "xs = y#ys"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
qed

text ‹Comentarios sobre la demostración anterior:
  · "(cases xs)" es el método de demostración por casos según xs.
  · Se generan dos subobjetivos  correspondientes a los dos
    constructores de listas:
    · 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
    · 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
  · "then" indica "usando la propiedad anterior"
›

(* La demostración declarativa detallada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  assume "xs = []"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by (simp only: conc.simps(1))
next
  fix y ys
  assume "xs = y#ys"
  then show "esVacia xs = esVacia (conc xs xs)" 
    by (simp only: esVacia.simps(2)
                   conc.simps(2))
qed

(* La demostración declarativa simplificada es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
next
  case Cons
  then show "esVacia xs = esVacia (conc xs xs)" 
    by simp
qed

text ‹Comentarios sobre la demostración anterior:
  · "case Nil" es una abreviatura de "assume xs = []"
  · "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"›

lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show ?thesis 
    by simp
next
  case (Cons a list)
  then show ?thesis 
    by simp
qed


(* La demostración con el patrón sugerido es *)
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
  case Nil
  then show ?thesis by simp
next
  case (Cons x xs)
  then show ?thesis by simp
qed

section ‹Heurística de generalización›

text ‹--------------------------------------------------------------- 
  Ejemplo 19. Definir la función
     inversaAc :: 'a list ⇒ 'a list
  tal que (inversaAc xs) es a inversa de xs calculada usando
  acumuladores. Por ejemplo, 
     inversaAc [a,c,b,e] = [e,b,c,a]
  ------------------------------------------------------------------ ›

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
  "inversaAcAux [] ys     = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

definition inversaAc :: "'a list ⇒ 'a list" where
  "inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e] = [e,b,c,a]"

text ‹Lema. [Ejemplo de equivalencia entre las definiciones]
  La inversa de [a,b,c] es lo mismo calculada con la primera definición
  que con la segunda.›

lemma "inversaAc [a,b,c] = inversa [a,b,c]"
  by (simp add: inversaAc_def)

text ‹Nota. [Ejemplo fallido de demostración por inducción]
  El siguiente intento de demostrar que para cualquier lista xs, se
  tiene que  "inversaAc xs = inversa xs" falla.›

lemma "inversaAc xs = inversa xs"
proof (induct xs)
  show "inversaAc [] = inversa []" 
    by (simp add: inversaAc_def)
next
  fix a :: "'b" and xs :: "'b list" 
  assume HI: "inversaAc xs = inversa xs"
  have "inversaAc (a#xs) = inversaAcAux (a#xs) []" 
    by (simp add: inversaAc_def)
  also have "… = inversaAcAux xs [a]" 
    by simp
  also have "… = inversa (a#xs)"
  (* Problema: la hipótesis de inducción no es aplicable. *)
oops

text ‹Nota. [Heurística de generalización]
  Cuando se use demostración estructural, cuantificar universalmente las 
  variables libres (o, equivalentemente, considerar las variables libres
  como variables arbitrarias).

  Lema. [Lema con generalización]
  Para toda lista ys se tiene 
     inversaAcAux xs ys = (inversa xs) @ ys
›

text ‹--------------------------------------------------------------- 
  Ejemplo 20. (p. 44) Demostrar que 
     inversaAcAux xs ys = (inversa xs) @ ys
  ------------------------------------------------------------------- ›

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

(* La demostración automática es *)
lemma "inversaAcAux xs ys = (inversa xs) @ ys"
  by (induct xs arbitrary: ys) simp_all

(* La demostración declarativa es *)
lemma
  "inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversaAcAux [] ys = (inversa []) @ ys" 
    by simp
next
  fix a :: "'b" and xs :: "'b list" 
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs @ ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs) @ ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" 
      by simp
    also have "… = inversa xs @ (a#ys)" 
      using HI by simp
    also have "… = inversa (a#xs) @ ys" 
      (* using [[simp_trace]] *)
      by simp 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs) @ ys" 
      by simp
  qed
qed

text ‹Comentarios sobre la demostración anterior:
  · "(induct xs arbitrary: ys)" es el método de demostración por
    inducción sobre xs usando ys como variable arbitraria.
  · Se generan dos subobjetivos:
    · 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
    · 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
                    inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
  · Dentro de una demostración se pueden incluir otras demostraciones.
  · Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
    lista arbitraria (con "fix ys") y se demuestra "P(ys)". ›

text ‹Nota. En el paso "inversa xs@(a#ys) = inversa (a#xs)@ys" se usan
  lemas de la teoría List. Se puede observar, insertano 
     using [[simp_trace]]
  entre la igualdad y by simp, que los lemas usados son 
  · append_simps_1: []@ys = ys
  · append_simps_2: (x#xs)@ys = x#(xs@ys)
  · append_assoc:   (xs @ ys) @ zs = xs @ (ys @ zs)
  Las dos primeras son las ecuaciones de la definición de append.

  En la siguiente demostración se detallan los lemas utilizados.›

― ‹Demostración aplicativa detallada›
lemma "(inversa xs) @ (a#ys) = (inversa (a#xs)) @ ys"
  apply (simp only: inversa.simps(2))
    (* inversa xs @ (a # ys) = (inversa xs @ [a]) @ ys*)
  apply (simp only: append_assoc)
    (* inversa xs @ (a # ys) = inversa xs @ ([a] @ ys) *)
  apply (simp only: append.simps(2))
    (* inversa xs @ (a # ys) = inversa xs @ (a # ([] @ ys)) *)
  apply (simp only: append.simps(1))
    (* *)
  done

― ‹Demostración declarativa detallada del lema auxiliar›
lemma auxiliar: "(inversa xs) @ (a#ys) = (inversa (a#xs)) @ ys"
proof -
  have "(inversa xs) @ (a#ys) = (inversa xs) @ (a # ([] @ ys))" 
    by (simp only: append.simps(1))
  also have "… = (inversa xs) @ ([a] @ ys)" 
    by (simp only: append.simps(2))
  also have "… = ((inversa xs) @ [a]) @ ys" 
    by (simp only: append_assoc)
  also have "… = (inversa (a#xs)) @ ys" 
    by (simp only: inversa.simps(2))
  finally show ?thesis 
    by this
qed

(* La demostración declarativa detallada es *)
lemma inversaAcAux_es_inversa:
  "inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'b list"
  show "inversaAcAux [] ys = (inversa []) @ ys" 
    by (simp only: inversaAcAux.simps(1)
                   inversa.simps(1)
                   append.simps(1))
next
  fix a :: "'b" and xs :: "'b list"
  assume HI: "⋀ys. inversaAcAux xs ys = inversa xs @ ys"
  show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs) @ ys"
  proof -
    fix ys
    have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" 
      by (simp only: inversaAcAux.simps(2))
    also have "… = inversa xs @ (a#ys)" 
      using HI by (simp only:)
    also have "… = inversa (a#xs) @ ys" 
      by (rule auxiliar) 
    finally show "inversaAcAux (a#xs) ys = inversa (a#xs) @ ys" 
      by this
  qed
qed

text ‹--------------------------------------------------------------- 
  Ejemplo 21. (p. 43) Demostrar que 
     inversaAc xs = inversa xs
  ------------------------------------------------------------------- ›

(* La demostración aplicativa es *)
corollary "inversaAc xs = inversa xs"
  apply (simp add: inversaAcAux_es_inversa inversaAc_def)
  done 

(* La demostración automática es *)
corollary "inversaAc xs = inversa xs"
  by (simp add: inversaAcAux_es_inversa inversaAc_def)

text ‹Comentario de la demostración anterior:
  · "(simp add: inversaAcAux_es_inversa inversaAc_def)" es el método de 
    demostración por simplificación usando como regla de simplificación 
    las propiedades inversaAcAux_es_inversa e inversaAc_def. ›
 
section ‹Demostración por inducción para funciones de orden superior ›

text ‹ --------------------------------------------------------------- 
  Ejemplo 22. Definir la función
     sum :: nat list ⇒ nat
  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
     sum [3,2,5] = 10
  ------------------------------------------------------------------ ›

fun sum :: "nat list ⇒ nat" where
  "sum []     = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5] = 10"

text ‹--------------------------------------------------------------- 
  Ejemplo 23. Definir la función
     map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
  tal que (map f xs) es la lista obtenida aplicando la función f a los
  elementos de xs. Por ejemplo,
     map (λx. 2*x) [3::nat,2,5] = [6,4,10]
     map ((*) 2)   [3::nat,2,5] = [6,4,10]
     map ((+) 2)   [3::nat,2,5] = [5,4,7]
  ------------------------------------------------------------------ ›

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
  "map f []     = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5] = [6,4,10]"
value "map ((*) 2)   [3::nat,2,5] = [6,4,10]"
value "map ((+) 2)   [3::nat,2,5] = [5,4,7]"

text ‹--------------------------------------------------------------- 
  Ejemplo 24. (p. 45) Demostrar que 
     sum (map ((*) 2) xs) = 2 * (sum xs)
  ------------------------------------------------------------------- ›

declare [[names_short]]

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

(* La demostración automática es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
  by (induct xs) simp_all

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

(* La demostración declarativa detallada es *)
lemma "sum (map ((*) 2) xs) = 2 * (sum xs)"
proof (induct xs)
  show "sum (map ((*) 2) []) = 2 * (sum [])" 
    by (simp only: map.simps(1)
                   sum.simps(1))
next
  fix a xs
  assume HI: "sum (map ((*) 2) xs) = 2 * (sum xs)"
  have "sum (map ((*) 2) (a#xs)) = sum ((2*a)#(map ((*) 2) xs))" 
    by (simp only: map.simps(2))
  also have "… = 2*a + sum (map ((*) 2) xs)" 
    by (simp only: sum.simps(2))
  also have "… = 2*a + 2*(sum xs)" 
    using HI by (simp only:)
  also have "… = 2*(a + sum xs)" 
    (* find_theorems "_ * (_ + _)" *)
    by (simp only: add_mult_distrib2)
  also have "… = 2*(sum (a#xs))" 
    by (simp only: sum.simps(2))
  finally show "sum (map ((*) 2) (a#xs)) = 2*(sum (a#xs))" 
    by this
qed

text ‹ --------------------------------------------------------------- 
  Ejemplo 25. (p. 48) Demostrar que 
     longitud (map f xs) = longitud xs
  ------------------------------------------------------------------- ›

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

(* La demostración automática es *)
lemma "longitud (map f xs) = longitud xs"
  by (induct xs) simp_all

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

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

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
1
2
3
4
5
6
7
Se puede imprimir o compartir con
