Para demostrar que sum.(xs ++ ys) = sum.xs + sum.ys, necesitamos tener las definiciones escritas:
(++)
: [A] → [A] → [A] |
sum
: [Num] → Num |
Prueba 1: por inducción en xs
Caso Base: reemplazo la variable elegida por [ ]:
sum.([ ] ++ ys) = sum.[ ] + sum.ys
y pruebo lo que obtengo:
sum.([
] ++ ys)
={ Definición de ++}
sum.ys
={
Aritmética }
0
+ sum.ys
={ Definición de sum }
sum.[
] + sum.ys
Caso inductivo: Copio el teorema tal como venía, y le llamo Hipótesis Inductiva (HI):
(HI) sum.(xs ++ ys) = sum.xs + sum.ys
reemplazo ahora (x ▷ xs) en lugar de xs en todos lados:
sum.((x ▷ xs) ++ ys) = sum. (x ▷ xs) + sum.ys
y demuestro lo que obtuve usando las definiciones y la HI.
sum.((x ▷ xs)++
ys)
={
Definición de ++}
sum.( x ▷
(xs ++ ys))
={ Definición de sum }
x
+ sum.(xs
++ ys)
={
HI }
x
+ sum.xs
+ sum.ys
={ Definición de sum }
sum.(x
▷ xs) + sum.ys
Prueba 2: Puede ocurrir que no se nos ocurran algunos pasos de la demostración de arriba, así que hay otra forma de escribir esta prueba, un poco más repetitiva pero que hace más fácil imaginarse qué hacer. Por lo demás, la prueba es la misma (también por inducción).
Caso Base: sum.([ ] ++ ys) = sum.[ ] + sum.ys
En vez de salir de un lado y llegar al otro, tomo todo.
sum.([
] ++ ys)
= sum.[ ] + sum.ys
≡{ Definición de ++}
sum.ys
= sum.[
]
+ sum.ys
≡{ Definición de sum }
sum.ys=
0 + sum.ys
≡{ Aritmética }
True
Caso inductivo: Usando
(HI) sum.(xs ++ ys) = sum.xs + sum.ys
pruebo:
sum.((x ▷ xs) ++ ys) = sum. (x ▷ xs) + sum.ys.
Tomo todo y opero:
sum.((x ▷ xs)++
ys)
= sum. (x ▷ xs) + sum.ys
≡{ Definición de
++}
sum.( x ▷ (xs ++ ys)) =
sum. (x ▷ xs) + sum.ys
≡{ Definición de sum
}
x + sum.(xs
++ ys)
= sum. (x ▷ xs) + sum.ys
≡{ HI }
x
+ sum.xs + sum.ys = sum.
(x ▷ xs)
+ sum.ys
≡{ Definición de sum }
x
+ sum.xs + sum.ys = x + sum.xs + sum.ys
≡{ Reflexividad de =
}
True