Wir haben folgende Funktionen:
prod :: [Int] -> Int
prod [] = 1 -- prod.1
prod (x:xs) = x * prod xs -- prod.2
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f acc [] = acc -- foldl.1
foldl f acc (x:xs) = foldl f (f acc x) xs -- foldl.2
Aufgabe:
Man soll mit struktureller Induktion beweisen, dass folgende Aussage gilt:
foldl (*) 1 xs = prod xs
Ich habe momentan:
foldl (*) 1 xs = prod xs
I.A. (xs = []):
foldl (*) 1 [] = prod []
foldl f acc [] = acc prod [] = 1 -- foldl.1 & plod.1
foldl f 1 [] = 1
1 = 1
I.V.: Wir nehmen an, dass die Aussage gilt für ein beliebiges xs
I.S. (xs -> x:xs):
foldl (*) 1 (x:xs) = prod (x:xs) -- foldl.2 & prod.2
foldl (*) ((*) 1 x) xs = x * prod xs
Problem: Ich weiß nun nicht wie ich mit dem Induktionsschritt fortfahren soll.
