Razonamiento automático (2016-17) Razonamiento automático (2016-17)

Pregunta de Wilmorort

chapter {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
imports Main 
begin

declare [[names_short]]

text {* --------------------------------------------------------------- 
  Ejercicio 1.1. Definir la función
     sumaImpares :: nat ⇒ nat
  tal que (sumaImpares n) es la suma de los n primeros números
  impares. Por ejemplo,
  sumaImpares 5  =  25
  ------------------------------------------------------------------ *}
   
(*Notar: Por la propiedad de Gauss se puede deducir que:
         la suma de los n numeros impares es igual a la suma de los 
         n y n-1 numeros consecutivos*)   
fun suma :: "nat ⇒ nat" where
    "suma 0 = 0"|
    "suma n = n + suma(n-1)"
    

fun sumaImpares1 :: "nat ⇒ nat" where
   "sumaImpares1 0 = 0" |
   "sumaImpares1 n = suma(n) + suma(n-1)"
  
value "sumaImpares1 3  = 9 "

lemma aux1 : "suma(Suc n) + suma(n) = (n+1) + suma(n) + n + suma(n-1)"
apply (induct n)
apply auto
done

lemma aux2: "(n+1) + suma(n) + n + suma(n-1) = (n+1) + n + sumaImpares1 n "
apply (induct n)
apply auto
done


text {* --------------------------------------------------------------- 
  Ejercicio 1.2. Demostrar que 
     sumaImpares n = n*n
  ------------------------------------------------------------------- *}
text {* --------------------------------------------------------------- 
  Por que no funciona demostrar con el siguiente algoritmo by(induct n) auto
  y se tiene que hacer una demostración detallada ??? 
  ------------------------------------------------------------------- *}

text {* --------------------------------------------------------------- 
  Creo que no funcionaba porque al usar una funcion auxiliar en tu definicion
  de sumaImpares te queda por demostrar la propiedad de esa funcion. Es decir, si aplicas
  induccion en "n+1" te quedaría por demostrar:
  (n+1)+(suma n)+(suma n) = (n+1)(n+1)
  (suma n) + (suma n) = n*n + n
  Asi que lo he demostrado anteriormente y he usado ese teorema en la demostracion

~~~~
  ------------------------------------------------------------------- *}

(* ~~~~ *)
lemma sumAux: "(suma n) + (suma n) = n + n * n"
apply (induct n)
apply auto
done

(*----------------------ERROR ----------------------------------------*) 
lemma "sumaImpares1 n = n*n"
apply (induct n)
apply auto
apply (simp add: sumAux) (* ~~~~ *)
done
(*--------------------------------------------------------------------*)
  
lemma "sumaImpares1 n = n*n"
proof (induct n)
show "sumaImpares1 0 = 0*0" by simp
next 
 fix n
 assume HI:"sumaImpares1 n = n*n"
 have "sumaImpares1 (Suc n) = suma(Suc n) + suma(n)" by simp
 have "suma(Suc n) + suma(n) = (n+1) + suma(n) + n + suma(n-1)"  using
 "aux1" by simp
 also have "... = (n+1) + n + sumaImpares1 n " using "aux2" by simp
 also have "... = 2*n +1 + n*n" using HI by simp
 also have "... = (n+1)*(n+1)" by simp
 finally show "sumaImpares1 (Suc n) = Suc n * Suc n" by simp
 qed

end