Ver el código de «Rel 11 (sol)»

<source lang="isabelle">
chapter ‹ R11: Razonamiento sobre programas en Isabelle/HOL (II)›
 
theory R11_sol
imports Main 
begin


text ‹ --------------------------------------------------------------- 
   En toda la relación de ejercicios las demostraciones han de realizarse
   de las formas siguientes:
    + automática
    + en el ejercicio 1.2, la prueba detallada usando "simp only:..."
      (bien de forma declarativa o aplicativa) 
    + en los ejercicios 5, 6 y 7 sólo es necesario hacer la demostración 
      detallada usando "simp", sin llegar al detalle de usar "simp only:..."
  ------------------------------------------------------------------ ›
    
text ‹ --------------------------------------------------------------- 
  Ejercicio 1.1. Definir la función
    factR :: nat ⇒ nat
  tal que (factR n) es el factorial de n. Por ejemplo,
    factR 4 = 24
  ------------------------------------------------------------------ ›
 
fun factR :: "nat ⇒ nat" where
  "factR 0       = 1"
| "factR (Suc n) = Suc n * factR n"
 
value "factR 4" ― ‹= 24›
 
text ‹ --------------------------------------------------------------- 
  Ejercicio 1.2. Se considera la siguiente definición iterativa de la
  función factorial 
     factI :: "nat ⇒ nat" where
     factI n = factI' n 1
 
     factI' :: nat ⇒ nat ⇒ nat" where
     factI' 0       x = x
     factI' (Suc n) x = factI' n (Suc n)*x
  Demostrar que, para todo n y todo x, se tiene 
     factI' n x = x * factR n
  ------------------------------------------------------------------- ›
 
fun factI' :: "nat ⇒ nat ⇒ nat" where
  "factI' 0       x = x"
| "factI' (Suc n) x = factI' n (x* (Suc n))"
 
fun factI :: "nat ⇒ nat" where
  "factI n = factI' n 1"
 
 ― ‹Demostración automática:›
lemma "factI' n x = x * factR n"  
  by (induct n arbitrary: x) 
    (auto simp del: mult_Suc)

 ― ‹Demostración en lenguaje natural:
Por inducción en n con x arbitrario, hay que probar 
     ∀n. (∀x. factI' n x = x * factR n)

+ Caso base:  hay que probar ∀x. factI' 0 x = x * factR 0
  En efecto, para cualquier x, se tiene factI' 0 x = x * factR 0,
  aplicando directamenta las definiciones de ambas funciones.

+ Paso inductivo:
  + HI: ∀x. factI' n x = x * factR n
  + Hay que probar  ∀x. factI' (n+1) x = x * factR (n+1)
  En efecto, sea a cualquiera
     factI' (n+1) a       = (por def. de factI')
     factI' n (a*(n+1))   = (por HI, para x = a*(n+1))
     (a*(n+1))*(factR n)  = (asociativa de *)
     a*((n+1)*(factR n))  = (def. de factR)
     a*(factR (n+1))
›

― ‹Demostración estructurada:›
lemma "factI' n x = x * factR n"
proof (induct n arbitrary: x)
  show "⋀x. factI' 0 x = x * factR 0" by simp
next
  fix n
  assume HI: "⋀x. factI' n x = x * factR n"
  show "⋀x. factI' (Suc n) x = x * factR (Suc n)"
  proof -
    fix x
    have "factI' (Suc n) x = factI' n (x * Suc n)" by simp
    also have "... = (x * Suc n) * factR n" using HI by simp
    also have "... = x * (Suc n * factR n)" by (simp del: mult_Suc)
    also have "... = x * factR (Suc n)" by simp
    finally show "factI' (Suc n) x = x * factR (Suc n)" by simp
  qed
qed

― ‹Demostración detallada declarativa:›     
lemma fact: "factI' n x = x * factR n"
proof (induct n arbitrary: x)
fix x
  have "factI' 0 x = x"
    by (simp only: factI'.simps(1))
  also have "... = x * 1"
    by (simp only: mult_1_right)
  also have "... = x * factR 0"
    by (simp only: factR.simps(1))
  finally show "factI' 0 x= x* factR 0"
    by this
next
  fix n 
  assume HI: " ⋀x. factI' n x = x *factR n"
  show "⋀x. factI' (Suc n) x = x*factR (Suc n)"
  proof -
    fix x
    have "factI' (Suc n) x = factI' n (x*Suc n)"
      by (simp only: factI'.simps(2))
    also have "... = (x*Suc n)*factR n"
      by (simp only: HI)
    also have "... = x*(Suc n*factR n)"
      by (simp only: mult.assoc)
    also have "... = x*factR (Suc n)"
      by (simp only: factR.simps(2))
    finally show "factI' (Suc n) x= x*factR (Suc n)"
      by this
  qed
qed

― ‹Demostración detallada aplicativa:›     
lemma  "factI' n x = x * factR n"
  apply (induct n arbitrary: x)
   apply (simp only: factI'.simps(1))
   apply (simp only: factR.simps(1)) 
  apply  (simp only: factI'.simps(2))
  apply  (simp only: factR.simps(2))
  done

text ‹ --------------------------------------------------------------- 
  Ejercicio 1.3. Demostrar que
     factI n = factR n
  ------------------------------------------------------------------- ›


― ‹Demostración automática:›
corollary "factI n = factR n"
  by (simp add: fact)

― ‹Demostración en lenguaje natural:

   factI n        = (def. de factI)
   factI' n 1     = (lema fact)
   1 * (factR n)  = (1 es elemento neutro de *)
   factR n
›


― ‹Demostración estructurada:›
corollary "factI n = factR n"
proof -
  have "factI n = factI' n 1"
    by simp
  also have "… = 1 * factR n"
    by (simp add: fact)
  also have "… = factR n"
    by simp 
  finally show "factI n = factR n"
    by this
qed

― ‹Demostración detallada declarativa:›
corollary "factI n = factR n"
proof -
  have "factI n = factI' n 1"
    by (simp only: factI.simps)
  also have "… = 1 * factR n"
    by (simp only: fact)
  also have "… = factR n"
    by (simp only: nat_mult_1)
  finally show "factI n = factR n"
    by this
qed


 text ‹
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función
     estaEn :: 'a ⇒ 'a list ⇒ bool
  tal que (estaEn x xs) se verifica si el elemento x está en la lista
  xs. Por ejemplo, 
     estaEn (2::nat) [3,2,4] = True
     estaEn (1::nat) [3,2,4] = False
  --------------------------------------------------------------------- 
›

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x []     = False"
| "estaEn x (a#xs) = (x=a ∨ estaEn x xs)"


text ‹ 
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función
     sinDuplicados :: 'a list ⇒ bool
  tal que (sinDuplicados xs) se verifica si la lista xs no contiene
  duplicados. Por ejemplo,  
     sinDuplicados [1::nat,4,2]   = True
     sinDuplicados [1::nat,4,2,4] = False
  --------------------------------------------------------------------- 
›

fun sinDuplicados :: "'a list ⇒ bool" where
  "sinDuplicados []     = True"
| "sinDuplicados (a#xs) = ((¬ estaEn a xs) ∧ sinDuplicados xs)"


text ‹ 
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función
     borraDuplicados :: 'a list ⇒ bool
  tal que (borraDuplicados xs) es la lista obtenida eliminando los
  elementos duplicados de la lista xs. Por ejemplo, 
     borraDuplicados [1::nat,2,4,2,3] = [1,4,2,3]

  Nota: La función borraDuplicados es equivalente a la predefinida 
  remdups. 
  --------------------------------------------------------------------- 
›


fun borraDuplicados :: "'a list ⇒ 'a list" where
  "borraDuplicados []     = []"
| "borraDuplicados (a#xs) = (if estaEn a xs
                             then borraDuplicados xs
                             else (a#borraDuplicados xs))"

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     length (borraDuplicados xs) ≤ length xs
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "length (borraDuplicados xs) ≤ length xs"
  by (induct xs) simp_all

 ― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: 
    length (borraDuplicados [])  ≤ length [], directamente por las definciones.

+ Paso inductivo: 
  + HI: length (borraDuplicados xs) ≤ length xs
  + Hay que probar: length (borraDuplicados (a#xs)) ≤ length (a#xs)
    La demostración se realiza por casos:

    + Caso 1: estaEn a xs
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
      length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
      length (borraDuplicados xs)     ≤ (por HI)
      length xs                       ≤ (aritmética)
      1 + length xs                   = (por def. de length)
      length (a#xs)    
              
    + Caso 2: ¬ (estaEn a xs)
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (a#xs) = a#(borraDuplicados xs). Por tanto,
      length (borraDuplicados (a#xs)) = (def. de borraDuplicados)
      length (a#(borraDuplicados xs)) = (def. de length)
      1 + length (borraDuplicados xs) ≤ (por HI)
      1 + length xs                   = (por def. de length)
      length (a#xs)                  

›


 ― ‹Demostración estructurada:›

lemma 
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados [])  ≤ length []" by simp
next
  fix a xs
  assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
  thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
  proof (cases)
    assume "estaEn a xs"
    thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
      using HI by simp
  next
    assume "(¬ estaEn a xs)"
    thus "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
      using HI by simp
  qed
qed


 ― ‹Auxiliares para la demostración detallada:›
lemma estaEnBD1:
  assumes "estaEn b xs"
  shows "borraDuplicados (b#xs) = borraDuplicados xs" 
  using assms by (simp only:borraDuplicados.simps(2) if_P)

lemma estaEnBD2:
  assumes "¬ (estaEn b xs)"
  shows "borraDuplicados (b#xs) = b#(borraDuplicados xs)" 
proof-
 have  "borraDuplicados (b#xs) =  (if estaEn b xs 
                             then borraDuplicados xs
                             else (b#borraDuplicados xs))" 
   by (simp only: borraDuplicados.simps(2))
  also have "…= (b#borraDuplicados xs)" using assms by (rule if_not_P)
  finally show "borraDuplicados (b # xs) = b # borraDuplicados xs" by this
qed 


 ― ‹Demostración detallada declarativa:›
lemma length_borraDuplicados_d:
"length (borraDuplicados xs) ≤ length xs"
proof (induct xs)
  show "length (borraDuplicados []) ≤ length []" 
    by (simp only: borraDuplicados.simps(1) list.size)
next
  fix a xs
  assume HI: "length (borraDuplicados (xs :: 'a list)) ≤ length xs"
  show "length (borraDuplicados (a#xs)) ≤ length (a#xs)"
  proof (cases)
    assume "estaEn a xs"
    then have "borraDuplicados (a#xs) = borraDuplicados xs" by (rule estaEnBD1)
    then have "length (borraDuplicados (a#xs)) = length (borraDuplicados xs)"
      by (rule arg_cong)
    also have "... ≤ length xs" using HI by this
    also have "... ≤ length (a#xs)" by (simp only: list.size)
    finally show ?thesis by this
  next
    assume "(¬ estaEn a xs)"
    then have "borraDuplicados (a#xs) = a#(borraDuplicados xs)"
      by (rule estaEnBD2)
    then have "length (borraDuplicados (a#xs)) = length (a#(borraDuplicados xs))"
      by (rule arg_cong)
    also have "... = 1 + length (borraDuplicados xs)" by (simp only: list.size)
    also have "... ≤ 1 + length xs" using HI by (simp only: add_left_mono)
    also have "... = length (a#xs)" by (simp only: list.size)
    finally show ?thesis  by this
  qed
qed

 ― ‹Demostración aplicativa detallada:›
lemma length_borraDuplicados_a:
"length (borraDuplicados xs) ≤ length xs"
  apply (induct xs)
   apply (simp only: borraDuplicados.simps(1) list.size)
  apply (simp only: borraDuplicados.simps(2))
  apply(split if_split)
  apply (rule conjI)
  apply (rule impI)
   apply (drule estaEnBD1)
   apply (simp only:list.size)
   apply (rule impI)
   apply (drule estaEnBD2)
   apply (simp only:list.size)
  done

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     estaEn a (borraDuplicados xs) = estaEn a xs
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
  by (induct xs) auto

 ― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: 
     estaEn a (borraDuplicados []) = estaEn a [], directamente por las definiciones.

+ Paso inductivo:
  + HI: estaEn a (borraDuplicados xs) = estaEn a xs
  + Hay que probar: estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs).
    La demostración se realiza por casos.
    
    + Caso 1: estaEn b xs
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (b#xs) = borraDuplicados xs. Por tanto,
      estaEn a (borraDuplicados (b#xs))    = (def. de borraDuplicados)
      estaEn a (borraDuplicados xs)        = (por HI)
      estaEn a xs                          = (por (estaEn b xs))
      estaEn a (b#xs)
           
    + Caso 2: ¬ (estaEn b xs)
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (b#xs) = b # (borraDuplicados xs). Por tanto,
      estaEn a (borraDuplicados (b#xs))        = (def. de borraDuplicados)
      estaEn a ( b # (borraDuplicados xs))     = (def. de estaEn)
      (a = b) ∨ (estaEn a (borraDuplicados xs) = (por HI)
      (a = b) ∨ (estaEn a xs                  = (def. de estaEn)
      estaEn a (b#xs)
›    


 ― ‹Demostración estructurada:›
lemma 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
  show "estaEn a (borraDuplicados []) = estaEn a []" by simp
next
  fix b xs
  assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
  show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)" 
  proof  (cases)
    assume "estaEn b xs"
    then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
    then have "estaEn a (borraDuplicados (b#xs)) = 
               estaEn a (borraDuplicados xs)" by (rule arg_cong)
    also have "… = estaEn a xs" using HI by this
    also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by auto
    finally show ?thesis by this
  next
    assume " ¬ estaEn b xs"
    then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
    then have "estaEn a (borraDuplicados (b#xs)) = 
               estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
    also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
      by (simp only: estaEn.simps(2))
    also have "… =  ((a = b) ∨ (estaEn a  xs))" using HI by simp
    also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
    finally show ?thesis by this
  qed
  qed

 ― ‹Auxiliar:›

lemma estaEnCons:
  assumes "estaEn b xs"
  shows "estaEn a xs = estaEn a (b#xs)" 
proof (rule iffI)
  assume " estaEn a xs " 
  then have "((a = b) ∨ (estaEn a xs))" by (rule disjI2)
  then show "estaEn a (b # xs)" by (simp only:estaEn.simps(2))
next
  assume "estaEn a (b # xs)" 
   then have "((a = b) ∨ (estaEn a xs))" by (simp only:estaEn.simps(2))
   then show  "estaEn a xs" 
   proof
     assume "a = b" then show "estaEn a xs" using assms by (rule ssubst)
   next 
     assume "estaEn a xs" then show  "estaEn a xs" by this
   qed
qed

 ― ‹Demostración detallada declarativa:›
lemma estaEn_borraDuplicados_d:
  "estaEn a (borraDuplicados xs) = estaEn a xs"
proof (induct xs)
  show "estaEn a (borraDuplicados []) = estaEn a []" 
    by (simp only:borraDuplicados.simps(1))
next
  fix b xs
  assume HI: "estaEn a (borraDuplicados xs) = estaEn a xs"
  show "estaEn a (borraDuplicados (b#xs)) = estaEn a (b#xs)" 
  proof  (cases)
    assume "estaEn b xs"
    then have "borraDuplicados (b#xs) = borraDuplicados xs" by (rule estaEnBD1)
    then have "estaEn a (borraDuplicados (b#xs)) = 
               estaEn a (borraDuplicados xs)" by (rule arg_cong)
    also have "… = estaEn a xs" using HI by this
    also have "… = estaEn a (b#xs)" using ‹estaEn b xs› by (rule  estaEnCons)
    finally show ?thesis by this
  next
    assume " ¬ estaEn b xs"
    then have "borraDuplicados (b#xs) = b#(borraDuplicados xs)" by (rule estaEnBD2)
    then have "estaEn a (borraDuplicados (b#xs)) = 
               estaEn a (b#(borraDuplicados xs))" by (rule arg_cong)
    also have "… = ((a = b) ∨ (estaEn a (borraDuplicados xs)))"
      by (simp only: estaEn.simps(2))
    also have "… =  ((a = b) ∨ (estaEn a  xs))" using HI by simp
    also have "… = estaEn a (b#xs)" by (simp only: estaEn.simps(2))
    finally show ?thesis by this
  qed
  qed

 ― ‹Demostración detallada aplicativa:›
lemma 
  "estaEn a (borraDuplicados xs) = estaEn a xs"
  apply (induct xs)
   apply (simp only: borraDuplicados.simps(1))
    apply (simp only: borraDuplicados.simps(2))
  apply(split if_split)
  apply (rule conjI)
   apply (rule impI) 
   apply (simp only: estaEnCons)
  apply (rule impI) 
  apply (simp only: estaEn.simps(2))
  done
                    

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar o refutar
     sinDuplicados (borraDuplicados xs)
  --------------------------------------------------------------------- 
›

 ― ‹Demostración automática:›
lemma "sinDuplicados (borraDuplicados xs)"
  by (induct xs) 
    (auto simp add: estaEn_borraDuplicados_d)

 ― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: 
   sinDuplicados (borraDuplicados []), directamente por las definiciones.

+ Paso inductivo:
  + HI: sinDuplicados (borraDuplicados xs)
  + Hay que probar: sinDuplicados (borraDuplicados (a#xs))
       La demostración se realiza por casos.
    
    + Caso 1: estaEn a xs
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (a#xs) = borraDuplicados xs. Por tanto,
      sinDuplicados (borraDuplicados (a#xs)) = (def.de borraDuplicados)
      sinDuplicados  (borraDuplicados xs)     (cierto, por HI)
    
    + Caso 2: ¬ (estaEn a xs)
      En este caso, por la definición de borraDuplicados, 
      borraDuplicados (a#xs) = a # (borraDuplicados xs). Por tanto,
      sinDuplicados (borraDuplicados (a#xs))     = (def. de borraDuplicados)  
      sinDuplicados (a#(borraDuplicados xs))     = (def. de sinDuplicados)
      ((¬ estaEn a (borraDuplicados xs)) ∧ 
       sinDuplicados (borraDuplicados xs))       = (por hI)
      ¬ estaEn a (borraDuplicados xs)            (cierto por la hipótesis del 
                                                  caso 2 y el ejercicio 6)   
›

 ― ‹Demostración estructurada:›
lemma 
  "sinDuplicados (borraDuplicados xs)"
proof (induct xs)
  show "sinDuplicados (borraDuplicados [])" by simp
next
  fix a xs
  assume HI: "sinDuplicados (borraDuplicados (xs :: 'a list))"
  show "sinDuplicados (borraDuplicados (a#xs))"
  proof (cases)
    assume "estaEn a xs"
    thus "sinDuplicados (borraDuplicados (a#xs))" using HI by simp
  next
    assume "¬ estaEn a xs"
    thus "sinDuplicados (borraDuplicados (a#xs))"
      using `¬ estaEn a xs` HI by (auto simp add: estaEn_borraDuplicados_d)
  qed
qed


 ― ‹Demostración detallada declarativa:›
lemma sinDuplicados_borraDuplicados_d:
  "sinDuplicados (borraDuplicados xs)"
proof (induct xs)
  show "sinDuplicados (borraDuplicados [])" 
    by (simp only: borraDuplicados.simps(1) 
                   sinDuplicados.simps(1))
next
  fix a xs
  assume HI: "sinDuplicados (borraDuplicados (xs:: 'a list))"
  show "sinDuplicados (borraDuplicados (a#xs))"
  proof (cases)
    assume "estaEn a xs"
    then have "borraDuplicados (a#xs) = borraDuplicados xs" 
      by (rule estaEnBD1)
    then show "sinDuplicados (borraDuplicados (a#xs))" using HI 
      by (rule ssubst)
  next
    assume 1: "¬ estaEn a xs"
     then have 2: "borraDuplicados (a#xs) = a#(borraDuplicados xs)" 
       by (rule estaEnBD2)
     have "¬ estaEn a (borraDuplicados xs)" using 1
       by  (simp add: estaEn_borraDuplicados_d)
     then have "¬ (estaEn a (borraDuplicados xs)) 
                   ∧ sinDuplicados (borraDuplicados xs)"
       using HI by (rule conjI)
     then have "sinDuplicados (a#(borraDuplicados xs))" 
       by (simp only: sinDuplicados.simps(2)[THEN sym])  
     with 2 show  "sinDuplicados (borraDuplicados (a#xs))" 
       by (rule ssubst)
  qed
qed

text ‹
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar o refutar:
    borraDuplicados (rev xs) = rev (borraDuplicados xs)
  --------------------------------------------------------------------- 
›

lemma "borraDuplicados (rev xs) = rev (borraDuplicados xs)"
  oops
(*
Auto Quickcheck found a counterexample:
  xs = [a⇩1, a⇩2, a⇩1]
Evaluated terms:
  borraDuplicados (rev xs) = [a⇩2, a⇩1]
  rev (borraDuplicados xs) = [a⇩1, a⇩2]
*)

end
</source>