Wir haben folgende Funktionen:
prod1 :: (Num a) => [a] -> a
prod1 [] = 1
prod1 (x:xs) = x * prod1 xs
prod2 :: (Num a) => [a] -> a
prod2 xs = help 1 xs
where
help acc [] = acc
help acc (x:xs) = help (x*acc) xs
Aufgabe:
Man soll mit struktureller Induktion und unter Verwendung einer geeigneten Hilfseigenschaft beweisen, dass folgende Aussage gilt:
prod1 xs = prod2 xs
Ich habe momentan:
prod1 xs = prod2 xs
I.A. (xs = []):
prod1 [] = prod2 []
prod1 [] = 1 prod2 [] = help 1 [] -- help
help 1 [] = 1
1 = 1
I.V.: Wir nehmen an, dass die Aussage gilt für ein beliebiges xs
I.S. (xs -> x:xs):
prod1 (x:xs) = prod2 (x:xs)
x * prod1 xs = help (x * 1) xs
Problem: Ich weiß nun nicht wie ich mit dem Induktionsschritt fortfahren soll.