Dokažte, že funkce fact x počítá faktoriál celého nezáporného čísla x!
fact 0 = 1
fact x = x * fact (x-1)
Důkaz povedeme indukcí vzhledem k hodnotě x.
I: Báze indukce
Ukážeme, že tvrzení platí pro nejmenší možný argument x = 0:
fact 0 = 0!
L: fact 0 ~> 1 -- levá strana rovnice
P: 0! = 1, což platí. -- pravá strana rovnice
II: Indukční krok
Nejprve musíme formulovat indukční předpoklad. Budeme předpokládat, že funkce fact x počítá
faktoriál čísla x pro libovolné číslo x = k:
Indukční předpoklad: fact k = k!
Za pomoci indukčního předpokladu ukážeme, že funkce je korektní pro číslo o jedna větší, než
které je použito v indukčním předpokladu x = k + 1:
fact (k+1) = (k+1)!
Zbývá zjistit, zda je na obou stranách opravdu stejná hodnota:
L: fact (k+1) ~> (k+1) * fact k IP
(k+1) * k! = (k+1)!
P: (k+1)! za použití indukčního předpokladu
Levá strana je rovna pravé => rovnost platí => dokázali jsme, že funkce je korektní.
Pozn.: Intuitivně můžeme indukci chápat tak, že platnost indukčního předpokladu lze vždy dokázat
pomocí indukčního kroku: korektnost fact k dokážeme s využitím předpokladu fact (k-1) =
(k - 1)!. Tento předpoklad můžeme opět dokázat pomocí předpokladu fact (k-2) = (k - 2)!.
Takto můžeme pokračovat, až po konečném počtu kroků dokážeme korektnost fact 1 = 1! za
předpokladu, že fact 0 = 0!, což máme přímo řečeno v bázi.
Dokažte, že funkce length m vrací délku seznamu m.
length [] = 0
length (_:s) = 1 + length s
Důkaz povedeme indukcí vzhledem k délce seznamu m.
I: Báze indukce
Ukážeme, že tvrzení platí pro nejkratší možný seznam m = []:
length [] = 0,
L: length [] ~> 0
P: 0, což platí.
II: Indukční krok
Nejprve musíme formulovat indukční předpoklad. Budeme předpokládat, že funkce length m
počítá délku seznamu m, m = s:
Indukční předpoklad: length s = n , kde n je délka seznamu s.
Za pomoci indukčního předpokladu ukážeme, že funkce je korektní pro seznam o jeden prvek delší,
než který je v indukčním předpokladu m = (x:s), délka m = n + 1:
length (x:s) = 1 + n
Zbývá zjistit, zda je na obou stranách opravdu stejná hodnota:
L: length (x:s) ~> 1 + length s IP
1 + n
P: 1 + n za použití indukčního předpokladu
Levá strana je rovna pravé => rovnost platí => dokázali jsme, že funkce je korektní.