====== AP5, IN5 Důkazy programů ======

===== Zadání =====
(dokazování vlastností programů, induktivní metody, invarianty cyklů)

===== Vypracování =====

==== Označení ====
(Tato část je napsána podle slajdů k předmětu Návrh algoritmů 1.)
<box 95% round blue | Označení>
    * //In//  Množina vstupních dat.
    * //Out//  Množina výstupních dat.
    * //A : In -> Out//  Algoritmus.
    * <math>\varphi: In \mapsto Bool</math> vstupní podmínka
    * <math>\psi: In \times Out \mapsto Bool</math> výstupní podmínka
</box>

Intuitivně řečeno, vstupní podmínka je unární predikát na množině vstupních dat a vymezuje ty, se kterými je algoritmus "ochoten pracovat". Výstupní podmínka říká, zda daný výstup je, nebo není výstupem algoritmu pro daný vstup. Pomocí těchto podmínek vyjadřujeme formálně svoje tvrzení o chování programu. Podmínky nemusí popisovat úplně celé chování programu, popisují jen to, co chceme dokazovat.

<box 95% round green | Příklad>Algoritmus A přečte tři čísla a vypíše je v neklesajícím pořadí. Funguje korektně jen pro nezáporná čísla.
    * In = Out = <math>\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}</math>
    * <math>\varphi_A((x,y,z))</math> je true právě když <math>x \geq 0 \wedge y \geq 0 \wedge z \geq 0</math>
    * <math>\psi_A(((x,y,z), (u,v,w)))</math> je true právě když (u,v,w) je permutací (x,y,z) a <math>u\leq v\leq w</math>

Tedy vstupní podmínka říká, že algoritmus funguje jen pro nezáporná čísla, přestože do něj můžeme
vložit i záporné číslo. Výstupní podmínka říká, jak bude vypadat výstup, pokud vstup splňuje vstupní podmínku.
</box>

==== Tvrzení, která budeme dokazovat ====
<box 95% round blue | Definice 1>Říkáme, že algoritmus //A// je **konvergentní vzhledem k **<math>\varphi</math>, pokud je množina <math>\left\{x\in In | \varphi(x)\right\}</math> podmnožinou definičního oboru funkce A.
</box>Intuitivně toto znamená, že algoritmus je konvergentní, pokud zastaví pro každou hodnotu povolenou vstupní podmínkou. 
(definiční obor algoritmu A jsou právě ty vstupy, pro které zastaví, to víme z vyčíslitelnosti).

<box 95% round green | Příklad 1>Pokud tedy tvrdíme, že algoritmus zastaví pro libovolné přirozené číslo na vstupu (tedy tvrdíme, že <math>\varphi(x) = true \Longleftrightarrow x \in \mathbb{N}</math>) a přitom se program zacyklí pro vstup 14, potom náš program není konvergentní vzhledem k <math>\varphi</math>. 

Stačí z <math>\varphi</math> vyřadit 14 a jsme v suchu ;)
</box><box 95% round blue | Definice 2>Řekneme, že A je **parciálně korektní vzhledem k **<math>\varphi, \psi</math>, pokud pro každou vstupní
hodnotu //x// z definičního oboru funkce A, pro kterou <math>\varphi(x) = true</math>, platí
<math>\psi((x, A(x)))</math>
</box>Intuitivně tedy musí algoritmus dávat ty hodnoty, které předepisuje výstupní podmínka <math>\psi</math>. Ale stačí, když je bude dávat jen pro vstupy povolené vstupní podmínkou <math>\varphi</math>. Navíc tato podmínka nepředepisuje, že algoritmus musí zastavit. Pokud tedy bude cyklit pro jakýkoliv vstup, stejně bude parciálně korektní. 


A nakonec definice, která říká to, co opravdu od programu očekáváme:
<box 95% round blue | Definice 3>Řekneme, že A je **totálně korektní vzhledem k ** <math>\varphi, \psi</math>, když je konvergentní vzhledem k <math>\varphi</math> a parciálně korektní vzhledem k <math>\varphi, \psi</math>.
</box>Jinak řečeno algoritmus musí skončit pro každou hodnotu povolenou vstupní podmínkou <math>\varphi</math> a navíc musí dát hodnotu splňující výstupní podmínku <math>\psi</math>.

==== Důkazové techniky ====
Nyní se dostaneme k tomu, jak vlastně dokázat, že program je totálně korektní vzhledem ke vstupní a výstupní podmínce. Důkazové techniky jsou trochu jiné pro funkcionální a pro imperativní paradigma.

=== Funkcionální paradigma ===
Dokazování vlastností čistě funkcionálních programů je jednodušší, protože každá funkce má nějakou hodnotu, o které můžeme něco tvrdit. Nejčastější důkazová technika je indukce, která často dobře odpovídá definicím funkcí v Haskellu.
<box 95% round green | Příklad funkcionálního programu 1>Mějme v Haskellu funkci/program ''fact''
   fact 0 = 1
   fact n = n * fact (n - 1)

Vyslovíme o ní následující dvě tvrzení:
   * Program ''fact'' je konvergentní vzhledem ke vstupní podmínce <math>\varphi</math>, která je definována <math>\varphi(x) = True \Leftrightarrow x\in \mathbb{N}_0</math>.
   * Program ''fact'' je parciálně korektní vzhledem k výstupní podmínce <math>\psi</math>, která je definována <math>\psi((x, y)) = True \Leftrightarrow y = x!</math>

Konvergentnost dokážeme z demonstračních důvodů indukcí. 
**Bázový krok:**
Pro x = 0 program podle definice skončí.
**Indukční krok**
Dokazujeme, že pokud program skončí pro <math>x \in \mathbb{N}_0</math>, potom skončí i pro //x + 1//. Z definice programu vidíme, že se volá funkce ''fact'' pro ''n - 1'' = //x// a jinak se provádí jen jedno sčítání a jedno násobení. Sčítání ani násobení se nezacyklí a konvergentnost funkce ''fact'' pro //x// máme z indukčního předpokladu. Tedy ani pro //x + 1// se program ''fact'' nezacyklí.

Zkráceně bychom mohli říct, že je zřejmé, že ''n'' se vždy o 1 zmenší a proto program skončí.

Parciální korektnost opět indukcí, tentokrát to vezmeme trochu rychleji.
**Bázový krok:**
Pro //x = 0// je z definice faktoriálu zřejmé, že <math>\psi((0, 1)) = True</math>.
**Indukční krok:**
Předpokládáme platnost tvrzení pro //x//, dokážeme ho pro //x + 1//. Dosazením do definice ''fact x + 1 = (x + 1) * fact x'' a s použitím indukčního předpokladu je ''fact x + 1 = (x + 1) * x!''. Podle definice faktoriálu je i ''fact x + 1 = (x + 1)!''.
</box>


<box 95% round green | Příklad funkcionálního programu 2>Funkce ''maxim'' najde největší číslo z konečného neprázdného seznamu čísel.
  maxim [x] = x
  maxim (x:y:s) = if x > y then maxim(x:s)
                           else maxim(y:s)

//In, Out// v tomto případě budou seznamy (posloupnosti) čísel. Vstupní podmínka bude platná pro neprázdné konečné seznamy, výstupní podmínka <math>\psi</math> bude definována jako <math>\psi\left(\left((a_0, a_1, ..., a_n) , \;x\right)\right) = True \Leftrightarrow \left(\forall i \in \left\{1, ... n\right\}\right)(x \geq a_i)</math>

Konvergentost je zřejmá, neboť při každém rekurzivním volání funkce ''maxim'' se sníží délka seznamu o 1 a pro seznamy délky 1 funkce vždy skončí. 

Parciální korektnost dokážeme indukcí vzhledem k délce seznamu.
**Bázový krok:**
Pro posloupnost <math>(a_0)</math> délky 1 tvrzení triviálně platí.
**Indukční krok:**
Předpokládáme, že tvrzení platí pro posloupnost <math>(a_n,... a_1, a_0)</math> a dokážeme ho pro posloupnost <math>(a_{n+1}, a_n, ... a_0)</math> kde <math>n \geq 1</math>. Seznamy jsou řazeny stejně jako seznamy v Haskellu. Uvážíme dvě možnosti. 
  * <math>a_{n+1} > a_n</math>. Potom výsledkem bude ''maxim (a<sub>n+1</sub>, a<sub>n - 1</sub>, ... a<sub>0</sub>)''. Můžeme použít indukční předpoklad, protože je to seznam o 1 prvek kratší (má délku n + 1, my dokazujeme pro seznam délky n + 2) a proto víme, že výsledkem bude maximální prvek posloupnosti (a<sub>n+1</sub>, a<sub>n - 1</sub>, ... a<sub>0</sub>). Ten je zároveň maximálním prvkem posloupnosti (a<sub>n+1</sub>, a<sub>n</sub>, a<sub>n - 1</sub>, ... a<sub>0</sub>), protože prvek a<sub>n</sub> není maximální.
  * Druhý případ je analogický.
</box>

<box 95% round green | Příklad funkcionálního programu 3>A nakonec algoritmus třídění vkládáním.
  inssort [] = []
  inssort (x:s) = ins x (inssort s)
    where ins x [] = [x]
          ins x (y:t) = if x <= y then x:(y:t)
                                  else y:(ins x t)

Množinou všech vstupů i výstupů budou všechny posloupnosti čísel. Vstupní podmínka omezí vstupy jen na konečné posloupnosti a výstupní podmínka platí pro //(x, y)// právě tehdy, když //y// je permutací posloupnosti //x// a //y// je neklesající.

Abychom mohli dokázat totální korektnost funkce ''inssort'', musíme dokázat totální korektnost funkce ''ins'', protože ta je při výpočtu ''inssort'' používána. Její vstupní množinou je dvojice //(x, A)//, kde //x// je číslo a //A// je posloupnost čísel. Tato funkce ke své správné funkci vyžaduje, aby byl seznam //A// neklesající. Vstupní podmínka tedy je φ( (x, A) ) = True <=> A je konečná a neklesající. Výsledkem této funkce je opět neklesající seznam //A//, do kterého byl vložen prvek //x// na příslušné místo. Tedy ψ( ( (x, A), B ) ) = True <=> //B// je neklesající, //B// obsahuje //x// a //B// obsahuje všechny prvky, které obsahuje //A//.

Nejprve dokážeme totální korektnost funkce ''ins''. Konvergentnost je zřejmá z předpokladu, že každý seznam na vstupu je konečný a že při každém rekurzivním volání se velikost seznamu zmenší o 1 a funkce pro prázdný seznam triviálně skončí. Indukční krok důkazu parciální korektnosti rozdělíme na dvě možnosti:
  * Je-li ''x ≤ y'', potom je výsledkem funkce seznam ''x:y:t''. Pro něj zřejmě platí, že obsahuje všechny prvky jako seznam ''y:t'', dále zřejmě platí, že obsahuje i prvek ''x''. Rovněž platí, že je neklesající, protože seznam ''y:t'' je dle vstupní podmínky neklesající a ''x ≤ y''.
  * Jinak je výsledkem seznam ''y:(ins x t)''. Tento seznam také splňuje všechny podmínky, protože dle IP je ''ins x t'' neklesající, obsahuje prvek ''x'' a všechny prvky z ''t''. Tedy i seznam ''y:(ins x t)'' obsahuje všechny prvky jako seznam ''y:t'', prvek ''x'' a navíc je díky IP a tomu, že ''y < x'', neklesající.

Přejdeme k důkazu funkce ''inssort''. Konvergentnost je opět zřejmá z toho, že na vstupu jsou pouze konečné seznamy, že funkce ''ins'' je konvergentní a že při každém rekurzivním volání ''inssort'' je předán seznam o 1 prvek kratší. Parciální korektnost se dokáže opět indukcí vzhledem k délce seznamu. Indukční krok říká, že můžeme aplikovat ''ins x (inssort s)'', protože dle IP je ''s'' neklesající seznam. Dostaneme neklesající seznam, ve kterém budou všechny prvky z ''s'' a prvek ''x''. To je ale seznam, který splňuje výstupní podmínku funkce ''inssort'' a proto jsme hotovi.
</box>

=== Imperativní paradigma ===
Zde je situace trochu složitější. Pokud máme v imperativním jazyce napsán program funkcionálním stylem, například
  int fact(int x) {
    if (x == 0)
      return 1;
    else
      return x * fact(x - 1);
  }
potom můžeme použít stejnou techniku jako pro funkcionální paradigma. 

V ostatních případech využijeme mezilehlé podmínky a invariant cyklu.

Důkaz konvergentnosti imperativních programů spočívá obvykle v nalezení číselné hodnoty, která v žádném okamžiku výpočtu nemůže být záporná a přitom při každém průchodu tělem cyklu klesne nejméně o jedničku. ((Slidy Návrh algoritmů 1, str.14))

**Mezilehlá podmínka** je tvrzení, jehož platnost v určitém místě programu dokážeme a potom ho použijeme k dokázání další mezilehlé podmínky, invariantu cyklu nebo nakonec výstupní podmínky. Jinými slovy, mezilehlá podmínka je takový záchytný bod v programu. Mezilehlé podmínky umístíme na místa, v nichž se stav výpočtu významně mění nebo kde není zcela zřejmá správnost programu ((Pokud bychom chtěli dokázat správnost naprosto formálně, do posledního bitu, museli bychom mít k dispozici formální sémantiku daného jazyka a potom bychom umístili mezilehlou podmínku mezi každé dva příkazy a všechny bychom dokázali. To se ovšem ze zřejmých důvodů v praxi moc nedělá.))

<box 95% green round | Příklad - mezilehlá podmínka>Uvažme následující pseudokód algoritmu třídění haldou:
  int[] heapsort(int []A)
    H = prázdná halda
    pro každý prvek x v A
      vlož x do haldy H
  
    *
      
    B = prázdný seznam
    dokud H není prázdná:
      vyber nejmenší prvek m z H
      přidej m do B
    
    vrať B

Zde bychom použili mezilehlou podmínku na místě označeném hvězdičkou. Tato podmínka by říkala, že ''H'' obsahuje všechny prvky ze seznamu A a má vlastnost haldy, tedy že pro každý uzel //X// platí: je-li //Y// synem uzlu //X//, potom //X// ≤ //Y//. Jakmile bychom dokázali, že kód před hvězdičkou opravdu takovou haldu vytvoří, mohli bychom to použít k důkazu toho, že kód za hvězdičkou skutečně vytvoří uspořádaný seznam. 
</box>

Pokud náš algoritmus pracuje nad nějakou datovou strukturou, potom obvykle vyslovíme podmínku, kterou datová struktura před a po běhu algoritmu vždy splňuje. Tuto podmínku pak využijeme k důkazu správnosti algoritmu. Samozřejmě pro algoritmy modifikující datovou strukturu musíme dokázat i to, že po jeho běhu podmínka stále platí. Tato podmínka datové struktury se obvykle formuluje ve vstupní a výstupní podmínce algoritmu.

<box 95% round green| Příklad - invariant datové struktury>Mějme například binární vyhledávací strom a na něm následující algoritmus:

  int getmin(Node n)
    if n nemá levého syna
      return n.hodnota
    else
      return getmin(n.left)

Jeho správnost dokážeme snadno použitím invariantu BVS, který říká, že pro každý uzel //X// stromu platí, že všechny uzly v jeho levém podstromu mají menší hodnotu než //X// a všechny uzly v pravém podstromu mají větší hodnotu než uzel //X//.
</box>

Algoritmy obvykle obsahují cykly. Pro dokázání jejich správnosti používáme invariant cyklu.
**Invariant cyklu** je mezilehlá podmínka umístěná v cyklu. Můžeme ho umístit, kam potřebujeme, ale musíme vždy dokázat následující:
  * Z předpokladů platících před cyklem (tedy buď ze vstupní podmínky algoritmu nebo z mezilehlých podmínek) dokážeme, že invariant cyklu platí při prvním běhu.
  * Je-li splněn invariant cyklu a cyklus se provede, potom invariant cyklu opět platí.
  * Je-li splněn invariant cyklu a cyklus skončí (není splněna podmínka cyklu), potom je splněna mezilehlá podmínka za cyklem nebo výstupní podmínka algoritmu.

<box 95% green round | Příklad - invariant cyklu 1>Následující imperativní program v Pascalu dokážeme pomocí invariantu cyklu:
  function factorial(n: Integer): Integer;
  var i, k: Integer;
  begin
    i := 0;
    k := 1;
    while i < n do begin
      i := i + 1;
      k := k * i;
    end;
    factorial := k;
  end;

Vstupní a výstupní podmínku už formulovat nebudu, každý si ji jistě dokáže vymyslet sám a navíc je stejná jako pro funkcionální verzi faktoriálu. Ukončení cyklu v algoritmu je zřejmé z toho, že proměnná ''i'' vždy vzroste o 1 a proměnná ''n'' je konstantní a proto jednou musí ''i'' být větší nebo rovno ''n''. Parciální korektnost dokážeme s pomocí invariantu cyklu ''k'' = ''i''! ∧ 0 ≤ ''i'' ≤ ''n'' v místě testování podmínky cyklu.

  * Na začátku běhu je ''k = 1'' a ''i = 0''. Tedy platí ''k'' = ''i''!. Druhá část invariantu zřejmě platí také.
  * Předpokládejme, že invariant platí. Označme ''i<sub>0</sub>'' hodnotu proměnné ''i'' před provedením cyklu a ''i<sub>1</sub>'' hodnotu proměnné ''i'' po jednom provedení cyklu. Podobně zavedeme i ''k<sub>0</sub>'' a ''k<sub>1</sub>''. Podle definice programu bude platit ''i<sub>1</sub> = i<sub>0</sub> + 1'' a ''k<sub>1</sub> = k<sub>0</sub> * i<sub>1</sub>''. Dle předpokladu tedy ''k<sub>1</sub> = i<sub>0</sub>! * i<sub>1</sub> = i<sub>1</sub>!''. Dále zřejmě platí i 0 ≤ ''i'' ≤ ''n''. Tím je dokázána platnost invariantu. 
  * Po ukončení cyklu platí ''k'' = ''i''! = ''n''!.
</box>

<box 95% round green | Příklad - invariant cyklu 2>Algoritmus umocňování pomocí půlení exponentu v Pascalu:
  function power(z: Real; n: Integer): Real;
  var y, r: Real
      k: Integer;
  begin
    k := n;
    y := z;
    r := 1;
   
    while k > 0 do begin
      if odd(k) then r := r * y;
      k := k div 2;
      y := y * y;
    end;
    power := r;
  end;

Zde už máme o něco složitější algoritmus a invariant cyklu není zřejmý na první pohled. Je vidět, že při každém zmenšení ''k'' na polovinu se umocní ''y'' na druhou. Proto dokud se dá ''k'' dělit na poloviny beze zbytku, je ''y<sup>k</sup> = z<sup>n</sup>'', protože ''y'' obsahuje dosavadní umocněnou hodnotu a ''k'' říká, jak moc ještě musíme umocňovat. Když je ''k'' liché, zaokrouhlí se při dělení 2 směrem dolů a tak se jakoby přeskočí jedno umocnění. Kvůli tomu je tam proměnná ''r'', do které se přinásobují mocniny ''z'' vždy, když je dělení ''k'' nepřesné (= když je ''k'' liché). Invariant cyklu je tedy ''r*y<sup>k</sup> = z<sup>n</sup> ∧ k ≥ 0''. Dokážeme už jen hlavní část důkazu korektnosti.

Předpokládejme, že je invariant splněn. Označíme si ''y<sub>0</sub>, y<sub>1</sub>, k<sub>0</sub>,...'' podobně jako v minulém příkladu. 
  * Pokud je ''k<sub>0</sub>'' sudé, potom ''r<sub>1</sub>'' = ''r<sub>0</sub>'', ''k<sub>1</sub>'' = ''k<sub>0</sub> / 2'', ''y<sub>1</sub>'' = ''y<sub>0</sub><sup>2</sup>''. Potom <math>r_1 y_1^{k_1} = r_0 \left(y_0^2\right)^{\frac{k_0}{2}} = r_0 y_0^{k_0} = z^n</math> dle předpokladu.
  * Je-li ''k<sub>0</sub>'' liché, potom <math>r_1 = r_0 y_0, k_1 = \frac{k_0 - 1}{2}, y_1 = y_0^2</math>. Potom je <math>r_1 y_1^{k_1} = r_0 y_0 \left(y_0^2\right)^{\frac{k_0 - 1}{2}} = r_0 y_0 y_0^{k_0 - 1} = r_0 y_0^{k_0} = z^n</math> opět dle předpokladu, že před provedením těla platil invariant cyklu. 

Na konci je ''k = 0'' a proto ''y<sup>k</sup> = 1'' a proto ''r = z<sup>n</sup>'' a proto je splněna výstupní podmínka.
</box>

<box 95% green round | Příklad - invariant cyklu 3>Algoritmus řazení vkládáním v Pascalu.
  const MAX = 999;
  type Posl = array [1..MAX] of Integer;
  procedure InsSort(n:Integer; var A: Posl);
  var i, j, x:Integer;
  begin
    for i := 2 to n do begin
      x := A[i];
      j := i - 1;
      while (j > 0) and (A[j] > x) do begin
        A[j + 1] := A[j];
        j := j - 1;
      end;
      A[j + 1] := x;
    end;
   end;

Nalezení invariantů cyklu jde u tohoto algoritmu ruku v ruce s pochopením jeho funkce. Musíme si v duchu projít několik prvních kroků, abychom viděli, jak vypadá a jak se mění seznam ''A'' vlivem algoritmu. Ve vnějším cyklu vidíme, že se vezme i-tý prvek, uloží se do ''x'' a na konci se někam vloží. Místo, kam se vloží, hledá vnitřní cyklus -- postupuje od pozice i - 1 směrem k začátku seznamu a skončí až když najde hodnotu menší než x. Zároveň s tím přerovnává všechny prvky o jednu pozici doprava, aby ''x'' mohlo být do seznamu vloženo. Tímto způsobem se postupně buduje uspořádaný seznam.

Invariant vnějšího cyklu je, že prvních ''i-1'' prvků v seznamu ''A'' je seřazených, zbývající prvky jsou ve stejném pořadí jako ve vstupním seznamu a seznam ''A'' obsahuje všechny prvky jako vstupní seznam. Invariant vnitřního cyklu je <math>A_1 \leq ... A_{j-1} \leq A_j = A_{j+1} \leq A_{j+2} \leq ... A_i</math> a prvních ''i'' prvků seznamu ''A'' je permutací prvních ''i'' prvků vstupního seznamu.

Platí-li invariant vnějšího cyklu, potom platnost invariantu vnitřního cyklu je zřejmá -- cyklus kopíruje prvky o jednu pozici doprava. Dále jelikož je dle předpokladu prvních ''i-1'' seřazených a vnitřní cyklus skončí jakmile ''A<sub>j</sub> ≤ x'', bude hodnota ''x'' vložena na správné místo a invariant vnějšího cyklu bude opět splněn.
</box>

==== Induktivní metody ====
(Tato část je napsána podle učebního textu k předmětu Úvod do informatiky)

Nejen správnost programu často dokazujeme pomocí indukce. A i takový invariant cyklu je vlastně indukce. Pro důkaz indukcí existuje několik technik.

=== Fixace parametru ===
Pokud má program více parametrů, ale jeden z nich se nemění, nemusíme se o něj v indukci starat a vlastnost dokážeme obecně pro jakoukoliv hodnotu tohoto parametru. 

<box 95% green round | Příklad - fixace parametru>Mějme následující funkci implementující násobení přirozených čísel:
  mul 0 _ = 0
  mul x y = y + mul (x - 1) y

Důkaz, že jde skutečně o násobení má následující tvar. Nechť //n ∈ N// je libovolné, ale dále pevné. Dokážeme běžnou indukcí vzhledem k //m//, že pro každé //m ∈ N// je ''mul m n = m * n''.
</box>

=== Indukce k součtu parametrů ===
Tuto techniku potřebujeme použít v případě, kdy máme více parametrů, které se postupně zmenšují, ale pokaždé je to jiný z nich.

<box 95% green round | Příklad - součet parametrů>Mějme následující funkci 
  g 0 _ = 0
  g _ 0 = 0
  g x y = g (x - 1) y + g x (y - 1)

Chceme dokázat, že pro každé //m, n ∈ N// platí ''g m n = 0''. Nemůžeme použít klasickou indukci k //m// nebo //n//, protože ani u jednoho nemáme zaručeno, že se vždy zmenší. Ale vždy se zmenší alespoň jeden a proto můžeme vést důkaz vzhledem k součtu parametrů. Dokážeme tedy tvrzení
//Pro každé i ∈ N platí, že jestliže i = m + n pro libovolná m, n ∈ N, potom //''g m n = 0''.
Z tohoto tvrzení potom přímo vyplyne platnost výstupní podmínky.

**Bázový krok**:
Na začátku //i = 0//. Z toho plyne, že //m = n = 0// a platnost tvrzení je triviální.
**Indukční krok**:
Zde uvážíme tři možnosti. 
  * //m = 0//. Potom zřejmě ''g 0 n = 0''.
  * //m > 0, n = 0//. Opět zřejmě ''g m 0 = 0''.
  * //m > 0, n > 0//. Dle definice platí ''g m n = (g (m - 1) n) + (g m (n - 1))''. Nyní můžeme použít indukční předpoklad na ''g (m - 1) n'', protože součet parametrů je menší než //i//. Podobně použijeme IP i na ''g m (n - 1)''. Zbytek je zřejmý.

</box>

=== Zesílení dokazovaného tvrzení ===
Toto je často používaná indukční důkazová technika. Při důkazu indukcí potřebujeme mít dostatečně silný indukční předpoklad, abychom se od něho mohli "odpíchnout" a dokázat další krok. Proto může být nutné dokázat silnější tvrzení, ze kterého potom naše požadované tvrzení triviálně vyplývá.

<box 95% green round | Příklad - zesílení dokazovaného tvrzení>Uvažme následující definice:
  f 0 = 1
  f x = h x
  h 0 = 1
  h x = f (x - 1) + h (x - 1)

Chceme dokázat, že pro každé //x// je ''h x = 2<sup>x</sup>''. To ale nelze dokázat indukcí přímo, protože bychom neměli k dispozici žádné tvrzení o funkci ''f''. Proto musíme zesílit tvrzení na
//Pro každé n ∈ N platí f n = 2<sup>n</sup> a h n = 2<sup>n</sup>//.
Toto tvrzení už dokážeme snadno.
</box>

===== Předměty =====
IB002 Návrh algoritmů 1 RNDr. Libor Škarvada
IB000 Úvod do informatiky doc. RNDr. Petr Hliněný Ph.D.

===== Literatura =====
Zápisky k přednášce Návrh algoritmů 1, RNDr. Libor Škarvada
Skripta k IB000 Úvod do informatiky doc. RNDr. Petr Hliněný Ph.D.

===== Zpracování =====
Vypracovává Roman Plášil, quiark@mail.muni.cz

Materiál je převzat ze slidů předmětu Návrh algoritmů 1. Ty jsou trochu strohé, proto jsem se snažil látku vysvětlit podle toho, jak ji chápu já a tedy doufám, že ji chápu dobře. Dále se omlouvám všem, pro které je vysvětlení příliš zdlouhavé, ale myslím, že se najde dost lidí, pro které je tato oblast těžko uchopitelná a jim to doufám pomůže. Uvítám připomínky a opravy, pokud něco nechápete, napište.

Poznámka k označení: Výstupní podmínku píšu se dvojitými závorkami ve tvaru ψ( (x, y) ), protože jde o funkci na uspořádané dvojici a toto je čistě formální zápis. Zápis s jedinou závorkou je ale používán častěji. Podobně je to se zápisem φ(x) = True <=> podmínka. Vstupní podmínka se dá chápat jako podmnožina množiny //In//, přestože je to ve skutečnosti funkce. Já se držím zápisu odpovídajícímu definici, ale množinový zápis by se asi taky dal tolerovat. A nakonec k označování proměnných v části převzaté z textu k IB000. Volně zaměnuji proměnnou v programu a proměnnou v důkazu, čímž se odlišuji od zdrojového textu a jeho formálních definic.

Stav zpracování: z mé strany hotovo.

~~DISCUSSION~~