.. coq:: From CoqBook Require Export Taktiky. Implikace ========= V této kapitole se budeme zabývat logickou spojkou implikace. Narozdíl od spojky konjunkce, která celkem přesně v přirozeném jazyce odpovídá spojce "a", vysvětlit neformálně význam implikace je výrazně obtížnější. Pokud máme dva výroky ``A`` a ``B``, pak výroku "``A`` implikuje ``B``" občas bývá přiřazován význam "pokud ``A``, pak ``B``". Takovéto chápání implikace je dobrým prvním přiblížením významu implikace, při hlubším zkoumání však neobstojí. My se spokojíme s vysvětlením implikace na základě toho, jak je obvykle používána v matematické praxi a rozebereme příklady jejího použití. Ukážeme také, jak se implikace dá chápat pohledem typovaného programovacího jazyka. Syntax implikace ---------------- V matematické logice se implikace výroků ``A`` a ``B`` obvykle zapisuje šipkou jako ``A → B``, případně dvojitou šipkou ``A ⇒ B``. Podobně jako u konjunkce pro nás bude vhodnější nepoužívat speciální symboly. Implikaci ``A`` a ``B`` tedy budeme zapisovat jako ``A -> B`` - jednoduchou šipku zapisujeme pomlčkou a znakem "je větší než". Pravidla pro práci se spojkou konjunkce --------------------------------------- I u implikace budeme potřebovat dvě pravidla, abychom s ní mohli pracovat a používat ji v důkazech. Pravidlo *eliminace* implikace má velmi snadné vysvětlení, pravidlo *zavedení* implikace je mírně složitější na pochopení, ale osvětlíme ho na několika příkladech. Eliminační pravidlo slouží k využití informace, která je uložena ve výroku tvaru ``A -> B``, zaváděcí pravidlo nám říká, co musíme vědět, abychom mohli tvrdit, že výrok tvaru ``A -> B`` platí. Jako první představíme pravidlo eliminace implikace. Pravidlo eliminace implikace ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Představme si, že z vyšetřování vraždy víme dvě fakta: 1. Vraždil muž. 2. Pokud vraždil muž, pak byl vrahem Ondřej. Z těchto dvou fakt se dá usoudit, že vrahem byl Ondřej. Tento úsudek nám znovu přijde zcela triviální: závěr plyne z předpokladů čistě na základě struktury daných předpokladů. Tomuto druhu úsudku se občas v logice říká *modus ponens*. Mírně formálněji: když víme, že platí výrok ``A`` a že platí výrok ``A -> B``, pak můžeme tvrdit, že platí i výrok ``B``. Tedy víme, že ``B`` je důsledkem ``A`` a ``A -> B``. Tím jsme *eliminovali* implikaci ``A -> B``, využili jsme ji k "extrakci" informace v ní uložené. Tento způsob odvození nyní přesně zformulujeme. Umíme-li z množiny předpokladů ``Gamma`` odvodit ``A`` (symbolicky ``Gamma |- A`` ), a umíme-li navíc z ``Gamma`` odvodit ``A -> B``, pak umíme z ``Gamma`` odvodit i ``B`` (symbolicky ``Gamma |- B`` ). Tento fakt zapisujeme jako odvozovací pravidlo: :: Gamma |- A Gamma |- A -> B --------------------------- Gamma |- B Toto pravidlo nazýváme **eliminace implikace**. Pravidlo zavedení implikace ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Pravidlo zavedení implikace je prvním pravidlem, ve kterém je pro nás nutné netriviálně pracovat s množinou předpokladů, které máme k disposici. To mírně ztěžuje jeho pochopení. Pokusíme se tedy nejprve vysvětlit jeho funkci neformálně. Představte si, že jste naprogramovali program ``P``, který se snaží řešit nějakou jednoduchou úlohu. Pochlubíte se s ním spolužákovi, necháte jej váš program vyzkoušet, a on se vám ozve zpět s následujícím tvrzením: "Když jsem vyzkoušel tvůj program ``P``, havaroval na vstupu ``15``". Jak se dá jeho tvrzení ověřit? Tvrzení spolužáka je tvaru ``Spustím P se vstupem 15 -> P havaruje``. Abychom ukázali (dokázali), že je pravdivé, stačí program ``P`` skutečně pustit se vstupem ``15`` a ověřit, zda havaruje. Tedy nám stačí dokázat tvrzení ``P havaruje`` s využitím předpokladu ``Spustím se vstupem 15``. Stejně tak můžeme uvažovat obráceně: když víme, že jsme ``P`` spustili se vstupem ``15`` a vidíme před sebou potemnělý monitor s chybovou hláškou (tedy důkaz výroku ``P havaruje``), můžeme vyvodit platnost výroku ``Spustím P se vstupem 15 -> P havaruje``. Tím jsme *zavedli* implikaci daných dvou výroků. Předcházející příklad nám umožňuje formulovat toto pravidlo přesně. Umíme-li z množiny předpokladů ``Gamma`` **s přidaným předpokladem** ``A`` odvodit výrok ``B`` (to zapisujeme symbolicky jako ``Gamma, A |- B`` ), pak z množiny předpokladů ``Gamma`` umíme odvodit ``A -> B``. Tento fakt zapisujeme jako odvozovací pravidlo: :: Gamma, A |- B --------------- Gamma |- A -> B Toto pravidlo nazýváme **zavedení implikace**. Všimněte si především toho, že v závěru daného pravidla se již výrok ``A`` nevyskytuje jako předpoklad. Vrátíme-li se k našemu intuitivnímu příkladu ze začátku, jakmile jsme již jednou vyzkoušeli, že na vstupu ``15`` program ``P`` havaruje, nemusíme to zkoušet dál, danou implikaci již víme i bez dalšího testování. (Tento příklad mírně nerealisticky předpokládá, že se ``P`` chová deterministicky.) Práce s implikací v Coq ----------------------- Na několika jednoduchých příkladech zase předvedeme, jak se s implikací dá pracovat v Coqu. Zavedeme novou sekci, ve které do kontextu přidáme výroky ``A, B, C``, o kterých se díky jejich zavedení můžeme začít vyjadřovat. .. coq:: Section priklady_implikace. Set Printing Parentheses. Context (A B C: Prop). V prvním příkladu si předvedeme pravidlo eliminace implikace. Používáme ho příkazem (tzv. *taktikou* ) ``impl_elim``. Našimi předpoklady jsou výroky ``A`` a ``A -> B``, dokázat máme tvrzení ``B``. Příkaz ``impl_elim ab`` vezme náš předpoklad ``A -> B`` a cíl ``B``, a používá zpětné odvozování: když máme dokázat ``B`` a víme ``A -> B``, stačí nám dokázat ``A`` a důkaz bude u konce. My však ``A`` také předpokládáme, a po použití ``impl_elim`` tedy stačí ještě použít příkaz ``assumption`` a důkaz je hotov. .. coq:: Lemma impl_priklad_1 (a : A) (ab : A -> B) : B. Proof. impl_elim ab. assumption. Qed. Předcházející důkaz může vypadat na první pohled překvapivě; předvedeme ještě alternativní důkaz "dopředným způsobem". V tomto důkazu si všímáme, že předpokládáme ``A`` i ``A -> B``, a používáme příkaz ``impl_elim`` k *přidání nového předpokladu*. Syntax ``impl_elim ab in a as b`` funguje následovně: ``ab`` je označení důkazu implikace ``A -> B``, ``a`` je označení důkazu výroku ``A``, a ``b`` je označení, které chceme použít k označení vyvozeného závěru, důkazu výroku ``B``. V našem konkrétním příkladu tím získáme novou množinu předpokladů obsahující důkazy výroků ``A``, ``A -> B`` i ``B``. Jelikož máme dokázat ``B``, stačí poukázat na to, že ``B`` již předpokládáme, příkazem ``assumption``. .. coq:: Lemma impl_priklad_1' (a : A) (ab : A -> B) : B. Proof. impl_elim ab in a as b. assumption. Qed. V dalším příkladu si ukážeme práci s pravidlem *zavedení implikace*. V Coqu toto pravidlo umožňuje použít příkaz ``intro``. Máme (bez dalších předpokladů) dokázat implikaci ``A -> A``. Jako vždy u důkazu implikace můžeme předpokládat její předpoklad a pokusit se dokázat závěr. To jest, abychom dokázali ``|- A -> A``, stačí nám důkaz ``A |- A``. Tuto přeměnu cíle zajistí právě příkaz ``intro``. Jelikož tento příkaz zavádí nový předpoklad, používáme parametr (zde ``a``), abychom tento nový předpoklad pojmenovali. Jelikož je předpoklad i závěr implikace ze zadání totožný, máme tedy dokázat něco, co už předpokládáme: to svede ``assumption``. .. coq:: Lemma impl_priklad_2 : A -> A. Proof. intro a. assumption. Qed. Dalším příklad (který popisuje "transitivitu" implikace) dokážeme zase dvěma způsoby: "zpětným" a "dopředným". Porovnejte oba způsoby a promyslete, který způsob by vás napadl první, popř. který způsob vám přijde elegantnější. .. coq:: Lemma impl_priklad_3 (ab : A -> B) (bc : B -> C) : A -> C. Proof. intro a. impl_elim bc. impl_elim ab. assumption. Qed. Lemma impl_priklad_3' (ab : A -> B) (bc : B -> C) : A -> C. Proof. intro a. impl_elim ab in a as b. impl_elim bc in b as c. assumption. Qed. Mírně složitější příklad ukazuje, jak lze pracovat s vnořenými implikacemi. Coq mírně zjednodušuje notaci *asociováním vpravo*: výrok ``A -> (B -> (C -> D))`` zapisuje bez závorek jako ``A -> B -> C -> D``. .. coq:: Lemma impl_priklad_4 (abc : A -> (B -> C)) : B -> (A -> C). Proof. intro b. intro a. impl_elim abc in a as bc. impl_elim bc in b as c. assumption. Qed. End priklady_implikace. Další příklady a úlohy ---------------------- Zkuste samostatně vyřešit následující úlohy (dokažte zadaná tvrzení). Za klíčové slovo ``Proof.`` začněte tvořit důkazový skript, a po úspěšné tvorbě důkazu nahraďte klíčové slovo ``Admitted.`` slovem ``Qed.`` .. coq:: Section ulohy_implikace. Context (A B C : Prop). Lemma impl_priklad_5 : A -> (B -> A). Proof. Admitted. Lemma impl_priklad_6 : A -> ((A -> B) -> B). Proof. Admitted. Lemma impl_priklad_7 (h : (A -> B) -> (A -> C)) : B -> (A -> C). Proof. Admitted. Lemma impl_priklad_8 (h : (A -> B) -> A) : B -> A. Proof. Admitted. Lemma impl_priklad_9 (h: A -> (B -> C)) (k : A -> B) : A -> C. Proof. Admitted. Lemma impl_priklad_10 (h : (A -> A) -> B) : (B -> C) -> C. Proof. Admitted. Lemma impl_priklad_11 : (A -> (B -> C)) -> ((A -> B) -> (A -> C)). Proof. Admitted. End ulohy_implikace.