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.

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.

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.

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.

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!

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.

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.

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.

Section ulohy_negace. Context (A B C : Prop).

Několik prvních úloh slouží k procvičení pravidla zavedení negace.

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.

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.

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.