.. coq:: From CoqBook Require Export Taktiky. Negace, True a False ==================== Občas potřebujeme vyjádřit negativní tvrzení: něco není pravda, některé předpoklady vedou ke sporu (jsou nesmyslné), a tak dále. Spojky, které jsme zatím zavedli, tvoří "positivní fragment" logiky, se kterou budeme pracovat. Abychom přidali "negativní" část, přidáme spojku *negace*, která nám umožní tvrzení vyvracet přesně tím, že *dokážeme jejich negaci*. Z technických důvodů budeme také potřebovat zavést speciální typ spojky (spíše konstanty), která bude representovat *nepravdivý výrok*, spojku ``False``. Uvidíme, že na základě této spojky lze negaci definovat. Syntax True, False a negace --------------------------- Výroky representující pravdivý a nepravdivý výrok budeme značit jednoduše jako ``True`` a ``False``. Negaci výroku ``A`` budeme značit jako ``~ A``. Toto značení ale budeme chápat pouze jako *syntaktickou zkratku*: ``~ A`` vnímejme jako makro, které po svém rozbalení značí výrok ``A -> False``. Proč dává takováto definice smysl? To si vysvětlíme v dalších odstavcích. Pravidla pro True, False a negaci --------------------------------- Spojky ``True`` a ``False`` jsou mezi ostatními spojkami výjimečné. Zatímco ``True`` má pouze pravidlo zaváděcí, ``False`` má pouze pravidlo eliminační. Pravidlo zavedení True ~~~~~~~~~~~~~~~~~~~~~~ Toto pravidlo uvádíme pouze pro úplnost. Se spojkou ``True`` se v příkladech nesetkáme; nehraje tak důležitou roli jako ``False``. K tomu, abychom mohli odvodit ``True``, nepotřebujeme *nic*. To plyne z toho, že ``True`` (representace pravdivého výroku) je pravdivé samo od sebe. Máme-li libovolnou množinu předpokladů, můžeme z ní odvodit výrok ``True``. Jako odvozovací pravidlo zapisujeme tento fakt následovně: :: ------------- Gamma |- True Tomuto pravidlu říkáme **zavedení ``True``**. Povšimněte si, že v odvozovacím pravidlu nad odvozovací čarou není nic napsáno. To přesně znamená, že odvození pod čarou můžeme provést bez jakýchkoli dalších požadavků. Pravidlo eliminace ``True`` nemáme. Znalost ``True`` nám nepomůže odvodit žádné netriviální tvrzení právě kvůli tomu, že je platné za všech situací. Pravidlo eliminace False ~~~~~~~~~~~~~~~~~~~~~~~~ Pravidlo eliminace ``False`` se občas nazývá svým latinským názvem "ex falso quodlibet": z nepravdy plyne cokoli. Obšírněji vysvětleno, pokud je vaše množina předpokladů sporná (plyne z ní nepravdivé tvrzení), pak jsou tyto předpoklady nesmyslné a stejně tak byste z nich mohli vyvodit cokoli. V přirozeném jazyce se občas používá komunikační obrat "Jestli je *tohle* pravda, tak jsem čínský bůh srandy", čímž řečník nepřímo říká, že to, co mu tvrdíte, je nesmysl, a lze z toho tedy i libovolný zjevný nesmysl vyvodit. Pravidlo nyní popíšeme přesněji. Umíme-li z množiny předpokladů ``Gamma`` odvodit ``False``, pak z ``Gamma`` umíme odvodit i libovolný výrok ``A``. V odvozovacím zápisu: :: Gamma |- False -------------- Gamma |- A Toto pravidlo nazýváme **eliminace False**. Využití tohoto pravidla v logické praxi uvidíme při diskusi pravidel pro spojku negace. Proč nemáme pravidlo pro *zavedení* ``False``? Uvědomme si, že zavést ``False`` by znamenalo *odvodit nepravdu*. To je ale něco, čemu se chceme za každou cenu vyhnout! Spojku ``False`` budeme používat pouze jako nástroj pro vyjádření negací výroků; při odvozování s negacemi občas v průběhu důkazu ``False`` odvodíme, bude to však pouze krátkodobý stav, který nám umožní o nějakém tvrzení vyvodit, že je nepravdivé. Pravidlo eliminace negace ~~~~~~~~~~~~~~~~~~~~~~~~~ Co se stane s výrokem, když ho znegujeme? Jak se negace jako logická spojka chová? Pravidlo eliminace negace nám dává polovinu obrázku. Když jsme přesvědčeni o nějakém výroku a současně o jeho negaci, je to špatná zpráva pro naši konsistenci: taková situace by neměla nastat. Obecně jsme přesvědčeni, že *z definice toho, jak negaci používáme*, nemůže být výrok pravdivý současně s jeho negací. Toto pozorování lze formalisovat: Dokážeme-li z množiny předpokladů ``Gamma`` odvodit výrok ``A`` a dokážeme-li z ``Gamma`` současně odvodit ``~ A``, pak (je množina ``Gamma`` sporná a) dokážeme odvodit i ``False``. V zápisu odvozovacích pravidel: :: Gamma |- A Gamma |- ~A ----------------------- Gamma |- False Tomuto pravidlu říkáme **eliminace negace**. Pravidlo zavedení negace ~~~~~~~~~~~~~~~~~~~~~~~~ Druhá polovina chování negace je popsána způsobem, jakým vyvozujeme, že nějaké tvrzení neplatí. Z matematické praxe jsme zvyklí, že negace tvrzení se dá dokázat tak, že dané tvrzení předpokládáme a odvodíme spor. V neformálním uvažování postupujeme podobně: pokud nějaké tvrzení "vezmeme za své", prozkoumáváme, k jakým důsledkům vede, a vidíme, že z něj plynou nesmyslné závěry, pak dané tvrzení opouštíme a prohlašujeme ho za vyvrácené. Z předchozí diskuse už odvozovací pravidlo zavedení disjunkce můžeme formalisovat. Umíme-li z množiny předpokladů ``Gamma`` s přidaným předpokladem ``A`` vyvodit ``False`` (symbolicky zapsáno jako ``Gamma, A |- False``), pak z množiny předpokladů ``Gamma`` umíme odvodit ``~ A``. Tento fakt zapisujeme jako odvozovací pravidlo: :: Gamma, A |- False ----------------- Gamma |- ~ A Toto pravidlo nazýváme **zavedení negace**. Vztah negace a implikace ~~~~~~~~~~~~~~~~~~~~~~~~ Pravidla pro zavedení a eliminaci negace jsme vysvětlili, aby dávala intuitivní smysl. Mnoho učebnic tato pravidla skutečně používá přesně tak, jak jsme je zapsali. Připomeňme si ale ze sekce o syntaxi negace, že negaci výroku ``A`` jsme zavedli jako syntaktickou zkratku: zápis ``~ A`` pro nás znamená výrok ``A -> False``. Můžeme si tedy vůbec dovolit pro negaci zavádět speciální pravidla? Vždyť podle naší prvotní dohody není negace nic jiného než zvláštní druh implikace! Ve skutečnosti pravidla zavedení a eliminace negace tak, jak jsme je zapsali, skutečně můžeme používat, protože jejich forma naprosto přesně kopíruje formu pravidel pro zavedení a eliminaci implikace. Přečtěme si naše pravidla ještě jednou, a tentokrát zapišme negaci ``~ A`` v "rozvinutém tvaru", tedy jako ``A -> False``. Pravidlo pro eliminaci negace: :: Gamma |- A Gamma |- A -> False ------------------------------- Gamma |- False Toto pravidlo je pravidlem pro eliminaci implikace ``A -> B``, kde jsme za výrok ``B`` zvolili speciálně výrok ``False``. Pravidlo pro zavedení negace: :: Gamma, A |- False ------------------- Gamma |- A -> False Toto pravidlo je pravidlem pro zavedení implikace ``A -> B``, kde jsme za výrok ``B`` opět zvolili speciálně výrok ``False``. Jak je vidět, pravidla pro chování negace jsme tedy zvolili velmi opatrně tak, aby nebyla odlišná od pravidel pro chování implikace, která jsme již zavedli dříve. Ještě lepší vysvětlení je ale opačné. Negace se zjevně řídí námi zvolenými pravidly, a to, že její chování můžeme "simulovat" syntaktickou zkratkou (``~ A`` je ``A -> False``), je pouze příjemné překvapení. Práce s negací v Coq -------------------- Jak jsme si vysvětlili, negace je velmi zvláštní druh implikace. Podobně jako u disjunkce tedy pro vás nebude práce s negací příliš obtížná, pokud jste již implikaci dobře pochopili. Jako vždy si v nové sekci zavedeme výroky ``A, B, C``, abychom se o nich mohli začít vyjadřovat. .. coq:: Section priklady_negace. Context (A B C : Prop). Pravidlo eliminace ``False`` (ex falso quodlibet) se v Coq využívá příkazem (taktikou) `exfalso`. Ať už máme za cíl dokázat jakékoli tvrzení, ``exfalso`` tento cíl změní na výrok ``False``. .. coq:: Lemma neg_priklad_1 (f : False) : A. Proof. exfalso. assumption. Qed. V dalším příkladu máme z nekonsistentní množiny předpokladů (``A`` a ``~ A``) odvodit ``False``. To je práce pro pravidlo eliminace negace: označíme-li důkazy tvrzení ``A`` a ``~ A`` jako ``a`` a ``nota``, pak můžeme pravidlo eliminace negace použít příkazem ``neg_elim a, nota``. .. coq:: Lemma neg_priklad_2 (a : A) (nota: ~ A) : False. Proof. neg_elim a, nota. Qed. My však víme, že negace je pouze syntaktickou zkratkou: ``~ A`` znamená ``A -> False``. Ten samý příklad nyní dokážeme metodou, kterou známe již ze studia spojky implikace. Příkaz ``unfold not in *`` je pomocný příkaz v Coqu, který prozkoumá předpoklady i cíl, který dokazujeme, a všechny výskyty negace ``~V`` jakéhokoli výroku ``V`` nahradí implikacemi ``V -> False``. Pak již stačí použít pravidlo eliminace implikace, které odpovídá pravidlu eliminace negace. Tento postup se často hodí, když v naší množině předpokladů nemáme přímo výrok a jeho negaci, ale pouze výroky, z nichž lze spor (``False``) odvodit. .. coq:: Lemma neg_priklad_2' (a : A) (nota: ~ A) : False. Proof. unfold not in *. impl_elim nota. assumption. Qed. Ve třetím příkladu si ukážeme práci se zavedením negace. Pro toto pravidlo využíváme příkaz ``neg_intro``. Přímo v našem zadání máme dokázat výrok ``~ A``, příkaz ``neg_intro`` tedy zavede nový předpoklad ``A`` a cíl (to, co máme dokázat) změní na ``False``. Znovu platí naše obecné pozorování: jelikož je negace pouze syntaktickou zkratkou, můžeme se k ní chovat jako k implikaci. Místo příkazu ``neg_intro`` jsme tedy mohli použít i příkaz ``intro`` (zavedení implikace), a výsledek by byl stejný. Vyzkoušejte! .. coq:: Lemma neg_priklad_3 (h: A -> (B /\ C)) (k : (B /\ C) -> False) : ~ A. Proof. neg_intro a. (* intro a. *) impl_elim k. impl_elim h. assumption. Qed. Alternativní postup řešení předchozího příkladu je vytvořit v množině předpokladů přímo výrok a jeho negace, zde ``B /\ C`` a ``~ B /\ C)`` (zde zapsáno jako ``(B /\ C) -> False``). Poté lze použít přímo pravidlo eliminace negace, tedy příkaz ``neg_elim``. .. coq:: Lemma neg_priklad_3' (h: A -> (B /\ C)) (k : (B /\ C) -> False) : ~ A. Proof. neg_intro a. (* intro a. *) impl_elim h in a as bc. neg_elim bc, k. Qed. Uvedeme další příklad, ve kterém se nad negací vyplatí přemýšlet jako nad implikací. Všimněte si, jak znovu používáme příkaz ``unfold`` k "rozbalení makra" pro negaci. Poté pracujeme v důkazu s implikacemi. .. coq:: Lemma neg_priklad_4 (h : ~ (A -> B)) : ~B. Proof. neg_intro b. unfold not in *. impl_elim h. intro a. assumption. Qed. End priklady_negace. 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_negace. Context (A B C : Prop). Několik prvních úloh slouží k procvičení pravidla zavedení negace. .. coq:: Lemma neg_priklad_5 (a : A) : ~ ~ A. Proof. Admitted. Lemma neg_priklad_6 (nega : ~ A) : ~ (A /\ B). Proof. Admitted. Lemma neg_priklad_7 (h : A -> ~ A) : ~ A. Proof. Admitted. Lemma neg_priklad_8 (h : ~ (A /\ B)) : A -> ~ B. Proof. Admitted. Lemma neg_priklad_9 (h : A -> B) : ~ B -> ~ A. Proof. Admitted. Lemma neg_priklad_10 (h : ~ (A \/ B)) : ~ A /\ ~ B. Proof. Admitted. Další úlohy slouží k procvičení pravidla *ex falso quodlibet*, tedy eliminace ``False``. .. coq:: Lemma neg_priklad_11 (h : ~ A) : A -> B. Proof. Admitted. Lemma neg_priklad_12 (h : A \/ B) : ~ A -> B. Proof. Admitted. Lemma neg_priklad_13 (h : A -> B) (k : A /\ ~ B) : C. Proof. Admitted. Lemma neg_priklad_14 (h : A \/ B) (p : A -> B) (q : B -> A) (k : ~ (A /\ B)) : C. Proof. Admitted. Poslední série příkladů sestává ze smíšených úloh; zde je nutno použít více druhů pravidel dohromady. .. coq:: Lemma neg_priklad_15 (h : ~ A /\ ~ B) : ~ (A \/ B). Proof. Admitted. Lemma neg_priklad_16 (h : ~ A \/ ~ B) : ~ (A /\ B). Proof. Admitted. End ulohy_negace.