.. coq:: From CoqBook Require Export Taktiky. Výroky, předpoklady, závěry =========================== Hlavním cílem této učebnice je představit praktickým způsobem důkazový systém nazvaný *přirozená dedukce* v takzvané (intuicionistické) výrokové logice. Co tento cíl znamená prakticky? Naučíte se dokazovat jednoduchá logická tvrzení: rozhodovat, zda vyplývají z předpokladů, které máte k disposici. Nejsnazší způsob přiblížení toho, co vás učebnice naučí, je ukázat příklad toho, co budete umět po jejím pročtení (a po zpracování všech úloh k procvičení). Ukázkový příklad ---------------- Vyzkoušíme si odvození jednoduchého důsledku ve výrokové logice. Představme si, že následující tři tvrzení bereme jako fakta: 1. Pokud se mi stal úraz hlavy, ztratím práci. 2. Pokud ztratím práci a rozvedu se, budu alkoholik. 3. Stal se mi úraz hlavy. Plyne z těchto třech tvrzení následující tvrzení? - Pokud se rozvedu, budu alkoholik. Ukážeme, že ano. Využijeme k tomu *důkazový asistent* Coq, který vás bude celou učebnicí doprovázet. Coq spustíte tlačítkem "power", které byste měli vidět v pravém horním rohu učebnice, "krokovat" příkazy můžete pomocí ``Alt + šipka dolů``. .. coq:: Section ukazkovy_priklad. Nejprve *deklarujeme* výroky, které budeme dále používat. .. coq:: Context (Uraz_hlavy Ztratim_praci Rozvedu_se Budu_alkoholik : Prop). Deklarací jsme vytvořili formální výroky ``Uraz_hlavy``, ``Ztratim_praci``, ``Rozvedu_se`` a ``Budu_alkoholik``, což jsou takzvané *atomické výroky*, z nichž budeme skládat výroky složitější. Představujeme si, že námi deklarované výroky representují výroky v přirozeném jazyce, a to "stal se mi úraz hlavy", "ztratím práci", "rozvedu se", a "budu alkoholik". díky tomu, že jsme výroky deklarovali, s nimi teď můžeme dál pracovat. Pozor! Deklarací výše jsme netvrdili, že dané výroky *platí* či jsou pravdivé. Srovnejte s přirozenou komunikací: mohu vyřknout například větu "Prší.", a je to výrok v přirozeném jazyce, ať už ve skutečnosti prší, či nikoli. Pokud např. chceme skutečně tvrdit, že jsem utrpěl úraz hlavy, musíme platnost tohoto výroku dosvědčit (zde spíše předpokládat) tím, že ho zavedeme jako hypotézu ``u : Uraz_hlavy``. Zde ``Uraz_hlavy`` je výrok representující výrok "stal se mi úraz hlavy", a ``u`` je označení *důkazu* ( *dosvědčení* ), že daný výrok skutečně platí. .. coq:: Hypothesis (u : Uraz_hlavy). Zavedeme nyní ještě dva předpoklady ("hypotheses") representující složené výroky z bodů 1. a 2. výše: .. coq:: Hypotheses (u_z : Uraz_hlavy -> Ztratim_praci) (zr_a : (Ztratim_praci /\ Rozvedu_se) -> Budu_alkoholik). Zatím není třeba, abyste rozuměli syntaxi, kterou používáme. Zápis ``u_z : Uraz_hlavy -> Ztratim_praci`` zde nicméně znamená, že ``u_z`` je označení pro důkaz (náš předpoklad), že "pokud se mi stal úraz hlavy, ztratím práci". Zápis ``zr_a : (Ztratim_praci /\ Rozvedu_se) -> Budu_alkoholik`` značí, že předpokládáme další tvrzení, a to složený výrok "pokud ztratím práci a rozvedu se, budu alkoholik". Atomické výroky skládáme pomocí takzvaných *logických spojek*. Nyní tedy předpokládáme všechna tři tvrzení, která jsme formulovali jako předpoklady v našem úvodním příkladu. Plyne z těchto předpokladů závěr, že pokud se rozvedu, budu alkoholik? To jest, lze vyvodit z výše zavedených "hypotéz" důsledek ``rozvedu_se -> budu_alkoholik``? Důsledek formulujeme jako lemma pojmenované ``r_a`` a dokážeme ho. Zkuste si důkaz "krokovat"! .. coq:: Lemma r_a : Rozvedu_se -> Budu_alkoholik. Proof. intro r. impl_elim zr_a. split. - impl_elim u_z. assumption. - assumption. Qed. Co se děje mezi klíčovými slovy ``Proof`` a ``Qed``? Používáme takzvané *taktiky*, příkazy v Coqu, které (zjednodušeně řečeno) odpovídají logickým *odvozovacím pravidlům*, krokům důkazu, ze kterých se celý důkaz nakonec skládá. Po celou dobu důkazu máte k disposici interaktivní přehled, v němž je vidět, *co* máte právě dokazovat, a *jaké předpoklady* zrovna můžete používat. Tedy například na začátku důkazu přehled vypadá přibližně takto: :: Uraz_hlavy, Ztratim_praci, Rozvedu_se, Budu_alkoholik : Prop u : Uraz_hlavy u_z : Uraz_hlavy -> Ztratim_praci zr_a : Ztratim_praci /\ Rozvedu_se -> Budu_alkoholik ______________________________________(1/1) Rozvedu_se -> Budu_alkoholik Přehled přesně odpovídá naší úloze: deklarovali jsme čtyři atomické výroky zmíněné v prvním řádku, v dalších třech řádcích vidíme naše tři předpoklady, a pod dlouhou vodorovnou čarou vidíme to, co máme dokázat: takzvaný *cíl*. Už po dvou krocích důkazu však vypadá náš přehled jinak: :: Uraz_hlavy, Ztratim_praci, Rozvedu_se, Budu_alkoholik : Prop u : Uraz_hlavy u_z : Uraz_hlavy -> Ztratim_praci zr_a : Ztratim_praci /\ Rozvedu_se -> Budu_alkoholik r : Rozvedu_se ______________________________________(1/1) Ztratim_praci /\ Rozvedu_se Z nějakého důvodu nám přibyl jeden předpoklad: ``r : Rozvedu_se``. Také se změnil náš cíl: máme dokázat (složený) výrok "ztratím práci a rozvedu se" (pouze formálně zapsán). Proč přibyl zrovna daný předpoklad a proč máme dokazovat zrovna daný cíl? V této učebnici si klademe za úkol přesně tyto otázky vysvětlit a zodpovědět. Potěšujícím koncem důkazu je, že po provedení posledního příkazu (taktiky) přehled zmizí a Coq vrací hlášku :: No more goals. což znamená, že důkaz byl správně (korektně) proveden a my ho můžeme uložit příkazem ``Qed``. Díky důkazovému asistentu jsme získali jistotu, že pokud jsme naši původní úlohu správně *formalisovali*, pak si o tom, že daný závěr vyplývá z našich předpokladů, můžeme být jisti. .. coq:: End ukazkovy_priklad. Co nám ukázkový příklad osvětluje? Budeme se snažit tvořit formální důkazy: vyvozovat závěry z předpokladů. Důkaz v Coq budujeme interaktivně tak, že se snažíme splnit *cíl*, a cíl postupně měníme (zjednodušujeme) *taktikami*. Tvrzení, která předpokládáme a dokazujeme, tvoříme z *atomických výroků* pomocí *logických spojek*. Význam a chování jednotlivých logických spojek si vysvětlíme v následujících kapitolách. Předpoklady a závěr ------------------- Jelikož nyní ještě logické spojky používat neumíme, vysvětlíme prozatím pouze jednu nejjednodušší formu logického úsudku. Řekněme, že jsme přesvědčeni o třech výrocích, např. "prší", "je mlhavo", "je tma". Co vše z těchto výroků můžeme vyvodit? Přinejmenším můžeme vyvodit to, co předpokládáme, tedy každý z daných třech výroků, například "prší". Formálně budeme takovýto úsudek značit jako ``prší, je mlhavo, je tma |- prší``. Znak ``|-`` je symbolem logického důsledku: před něj doleva píšeme množinu předpokladů, se kterými pracujeme, za něj doprava píšeme důsledek daných předpokladů. Druh úsudku z minulého odstavce nyní zformalisujeme jako *odvozovací pravidlo*: označme si nějakou množinu výroků jako ``Gamma``. Dále budeme používat značení ``Gamma, A`` pro množinu výroků ``Gamma``, do které jsme přidali ještě výrok ``A``. Z množiny předpokladů ``Gamma, A`` lze odvodit výrok ``A``, jelikož tento výrok již předpokládáme. Tomuto pravidlu se říká **pravidlo předpokladu** a je značeno následovně: :: ------------- Gamma, A |- A Vodorovné čáře v odvozovacím pravidlu říkáme odvozovací čára. Nad ní jsou zapsány podmínky, za kterých lze pravidlo použít (tedy naše pravidlo nemá žádné podmínky), a pod ní je napsáno, co lze díky odvozovacímu pravidlu odvodit. Předvedeme si nyní na příkladu užití pravidla předpokladu v Coqu. Příklad nutně nemůže být příliš zajímavý, protože samotné pravidlo předpokladu neumožňuje tvořit zajímavé a složité důkazy. Je to pouze základní stavební kámen, který budeme v dalších kapitolách pravidelně využívat. .. coq:: Section predpoklad_priklad. Deklarujeme výroky ``A``, ``B`` a ``C``. .. coq:: Context (A B C: Prop). Nyní budeme předpokládat, že námi zavedené výroky platí. .. coq:: Hypotheses (a : A) (b: B) (c : C). Co znamená zápis ``(a : A)``? Symbolem ``a`` zde označujeme důkaz toho, že ``A`` pro nás nyní platí, a podobně tomu je u ``b`` a ``c``. Dokážeme tvrzení (lemma) s názvem ``z_A_B_C_plyne_A``, jehož závěrem je ``B``. Důkaz v Coqu začínáme příkazem ``Proof.``, končíme ho příkazem ``Qed.``, a pravidlo předpokladu v Coqu používáme příkazem ``assumption``. .. coq:: Lemma z_A_B_C_plyne_B : B. Proof. assumption. Qed. Jelikož jsme závěr lemmatu skutečně předpokládali, je náš důkaz korektní a Coq nehlásí problém. .. coq:: End predpoklad_priklad. Předvedeme ještě alternativní způsob zápisu našeho příkladu, který bude obvyklejší v následujících kapitolách. .. coq:: Section predpoklad_priklad'. Znovu zavedeme výroky ``A``, ``B`` a ``C``. Obor platnosti zavedení výroků (jejich *scope* ) je pouze uvnitř sekce, zavedení výroků ``A``, ``B``, ``C`` z minulé sekce zde tedy již neplatí. .. coq:: Context (A B C : Prop). Nyní místo použití příkazu ``Hypotheses`` pro zavedení předpokladů tyto předpoklady zmíníme přímo ve znění našeho lemmatu: .. coq:: Lemma z_A_B_C_plyne_B' (a : A) (b : B) (c : C) : B. Proof. assumption. Qed. Lemma má stejný důkaz i stejný závěr, jen nyní obsahuje předpoklad platnosti výroků ``A``, ``B`` a ``C``, důkazy těchto třech výroků postupně označujeme jako ``a``, ``b`` a ``c``. Předpoklady píšeme za název lemmatu, a oddělujeme je od závěru dvojtečkou. .. coq:: End predpoklad_priklad'. Nyní jste již připraveni na opravdový začátek: studium logických spojek a jejich chování. V dalších kapitolách probereme spojky konjunkce, implikace, disjunkce a negace, a uvidíme, jak jejich využití umožňuje formulovat výrazně složitější a zajímavější důkazy.