Ejercicio de Inducción (mal)
La siguiente es una demostración errónea de que sum.(duplica.xs) = 2 * sum.xs. Escribimos las definiciones:
|
duplica : [Num]
→ [Num] |
sum
: [Num] → Num |
Caso Base: reemplazo la variable elegida por [ ]:
sum.(duplica.[ ]) = 2*sum.[ ]
y pruebo lo que obtengo:
sum.(duplica.[
] )
={ Definición de duplica }
sum.[
]
={ Definición de sum }
0
={
Aritmética }
2*0
={
Definición de sum }
2*sum.[ ]
Caso inductivo: La Hipótesis Inductiva es:
(HI) sum.(duplica.xs) = 2 * sum.xs
y debemos probar
sum.(duplica.(x ▷ xs)) = 2* sum. (x ▷ xs):
Comparemos el lado izquierdo con la hipótesis inductiva. Como venimos haciendo, ponemos uno arriba del otro,
|
sum.(duplica. |
xs |
)= 2*sum. |
xs |
|
sum.(duplica. |
(x ▷ xs) |
)= 2*sum. |
... |
Luego, en lugar de los puntos suspensivos debe ir (x ▷ xs):
|
sum.(duplica. |
xs |
)= 2*sum. |
xs |
|
sum.(duplica. |
(x ▷ xs) |
)= 2*sum. |
(x ▷ xs) |
Entonces podemos justificar así:
sum.(duplica.(x ▷ xs))
=
2*sum. (x ▷ xs)
≡{ HI para (x ▷ xs)
}
2*sum.
(x ▷ xs) = 2*sum. (x ▷ xs)
≡{
Reflexividad de = }
True
Y así concluye la prueba (?!?)
Ejercicio: Encontrar el error!