0 Daumen
82 Aufrufe

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.

Avatar von

Ein anderes Problem?

Stell deine Frage

Willkommen bei der Stacklounge! Stell deine Frage einfach und kostenlos

x
Made by a lovely community