From CoqBook Require Export Taktiky.

Disjunkce

Disjunkce je logická spojka, jejíž význam je (narozdíl od implikace) snadné vysvětlit: velmi věrně odpovídá spojce „nebo“ v přirozeném jazyce (v nevylučovacím smyslu). Pro dva výroky A a B tedy významem výroku „A disjunkce B“ je složený výrok „A nebo B“. Jakkoli je toto přímočaré vysvětlení snadné, uvidíme, že formální odvozovací pravidla pro disjunkci jsou spíše složitější, a na práci s nimi je třeba si chvíli zvykat.

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 disjunkce

V matematické logice se disjunkce výroků A a B obvykle zapisuje obrácenou stříškou jako A ∨ B. My budeme disjunkci zapisovat bez speciálních symbolů jako A \/ B - zpětným a dopředným lomítkem.

Pravidla pro práci se spojkou disjunkce

Chování spojky disjunkce je jako u konjunkce a implikace popsáno dvěma typy pravidel - potřebujeme dvě pravidla pro zavedení disjunkce, a jedno (složitější) pravidlo pro eliminaci disjunkce. Uvidíme, že pravidlo pro eliminaci disjunkce kopíruje důkazový postup známý jako „proof by cases“ - důkaz rozborem případů. Je to způsob, jak využít znalost toho, že platí jeden ze dvou faktů, když nevíme, který z nich platí.

Pravidlo zavedení disjunkce

Víte-li, že venku prší, pak jistě i víte, že venku prší nebo hřmí. Říci, že „prší nebo je mlha“ je slabší tvrzení, než říci „prší“. Pravidlo zavedení konjunkce říká, že silnější tvrzení můžeme tímto způsobem oslabit.

Přirozenou otázkou však je, proč bychom kdy měli chtít nějaké tvrzení oslabovat. Uvedeme klasickou situaci, kdy je to potřeba: představte si, že máte za cíl někoho přesvědčit, že venku prší nebo je mlha. Jak mu dokázat, že venku skutečně prší nebo je mlha? Stačí, když ho přesvědčíte o pravdivosti kteréhokoli z daných dvou výroků: buď mu ukážete, že prší, nebo ho přesvědčíte, že je mlha.

Formulujeme nyní přesněji odvozovací pravidla zavedení disjunkce. Umíme-li z množiny předpokladů Gamma odvodit výrok A (symbolicky zapsáno jako Gamma |- A), pak z množiny předpokladů Gamma umíme odvodit i A \/ B. Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma |- A
---------------
Gamma |- A \/ B

Stejně tak platí, že umíme-li z množiny předpokladů Gamma odvodit výrok B (symbolicky zapsáno jako Gamma |- B), pak z množiny předpokladů Gamma umíme odvodit i A \/ B. Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma |- B
---------------
Gamma |- A \/ B

Tato dvě pravidla nazýváme zavedení disjunkce.

Pravidlo eliminace disjunkce

Představme si, že z vyšetřování vraždy víme tři fakta: 1. Vražda proběhla v noci nebo brzy ráno. 2. Pokud vražda proběhla v noci, je vrahem Ondřej. 3. Pokud vražda proběhla brzy ráno, je vrahem Ondřej.

Z těchto třech fakt se dá usoudit, že vrahem byl Ondřej. Je to úsudek, který již není třeba hlouběji zdůvodňovat: závěr plyne z předpokladů čistě na základě významu spojek „nebo“ a významu podmíněných tvrzení. Sice nevíme, kdy přesně vražda proběhla, ale víme, že v obou případech by vrahem byl Ondřej, a tedy Ondřej vrahem je. Mírně formálněji: když víme, že platí výrok A \/ B, že z platnosti výroku A lze vyvodit C, ale i z platnosti výroku B lze vyvodit C, pak můžeme tvrdit, že platí i výrok C. Tím jsme eliminovali disjunkci A \/ B, využili jsme ji k „extrakci“ informace v ní uložené.

Využijeme (stejně jako u ostatních spojek) náš neformální popis k přesné formulaci tohoto způsobu odvození. Umíme-li 1. z množiny předpokladů Gamma odvodit A \/ B (symbolicky Gamma |- A \/ B ``), 2. z množiny předpokladů ``Gamma s přidaným předpokladem A odvodit C (symbolicky Gamma, A |- C), a 3. z množiny předpokladů Gamma s přidaným předpokladem B odvodit C (symbolicky Gamma, B |- C),

pak umíme z množiny Gamma odvodit C (Gamma |- C). Tento fakt zapisujeme jako odvozovací pravidlo:

Gamma |- A \/ B  Gamma, A |- C  Gamma, B |- C
---------------------------------------------
Gamma |- C

Toto pravidlo nazýváme eliminace disjunkce.

Všimněte si, že zatímco nad „odvozovací čarou“ přidáváme k množině předpokladů Gamma jednou výrok A a jednou výrok B, závěr našeho pravidla už využívá jen množinu předpokladů Gamma. K důkazu výroku C již nepotřebujeme A ani B předpokládat: předpokládali jsme je pouze „lokálně“ při rozboru případů.

Práce s disjunkcí v Coq

Práce s disjunkcí v Coqu pro vás nebude překvapivá, pokud jste již zvládli práci s implikací. Podobně jako u implikace stačí pochopit, jakým způsobem se při dokazování mění množina předpokladů, které máme k disposici. Zbytek práce je již relativně přímočarý.

Jako vždy si v nové sekci zavedeme výroky A, B, C, abychom se o nich mohli začít vyjadřovat.

Section priklady_disjunkce. Set Printing Parentheses. Context (A B C: Prop).

V prvním příkladu si předvedeme pravidlo zavedení disjunkce. Používáme ho příkazem left či right podle potřeby. Naším předpokladem je výrok A, dokázat máme tvrzení A \/ B (to je tedy náš cíl ). Taktiky (příkazy) left a right používají „zpětné“ odvozování. Pokud na cíl A \/ B použijeme taktiku left, říkáme, že se pro důkaz A \/ B pokusíme dokázat A. Podobně příkazem right by se náš cíl změnil na B. Zde je zjevně vhodné použít left, neboť výrok A je jedním z našich předpokladů. Důkaz tedy dokončíme příkazem assumption.

Lemma disj_priklad_1 (a : A) : A \/ B. Proof. left. assumption. Qed.

Když máme dokázat disjunkci A \/ B z předpokladu B, použijeme taktiku right.

Lemma disj_priklad_2 (b : B) : A \/ B. Proof. right. assumption. Qed.

Následující příklad ilustruje použití pravidla eliminace disjunkce. Neformálně řečeno máme ukázat, že pokud z A plyne B, pak i z „A nebo B“ plyne B. Nejprve tedy předpokládáme A \/ B (to je nám již známe pravidlo zavedení implikace). V množině předpokladů se nám tedy objeví avb : A \/ B, nyní tedy víme, že platí A nebo B.

Provedeme rozbor případů: co se stane, když platí A? Co se stane, když platí B? K rozboru případů použijeme pravidlo eliminace disjunkce, které se v Coqu nazývá též destruct. Toto pravidlo má pro disjunkci mírně odlišnou syntax: destruct avb as [a | b] zde znamená „vezměme avb, což je důkaz tvrzení A \/ B, a rozeberme ho na případ, kdy platí A (označíme důkaz tvrzení A jako a), a na případ, kdy platí B (označíme důkaz tvrzení B jako b)“. Použitím tohoto pravidla se nám cíl rozdělí na dva podcíle: to je právě smysl rozboru případů. V obou cílech máme dokázat to samé tvrzení (zde (A \/ B) -> B), každý podcíl však bude mít odlišnou množinu předpokladů.

Rozdíl syntaxe oproti eliminaci konjunkce zde spočívá v tom, že nové předpoklady oddělujeme znakem |, píšeme tedy [a | b] a nikoli [a b].

Jednotlivé podcíle označujeme pomlčkou - a řešíme je zvlášť. (Případné další větvení podcílů označujeme značkou + či *, zde to není třeba.)

Lemma disj_priklad_3 (h : A -> B) : (A \/ B) -> B. Proof. intro avb. destruct avb as [a | b]. - impl_elim h. assumption. - assumption. Qed.

Důkladně promyslete, zda rozumíte důkazu „komutativity disjunkce“. Dokázali byste ho samostatně rekonstruovat?

Lemma disj_priklad_4 (avb : A \/ B) : B \/ A. Proof. destruct avb as [a | b]. - right. assumption. - left. assumption. Qed. End priklady_disjunkce.

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_disjunkce. Context (A B C : Prop).

Úlohy s disjunkcí

Lemma disj_priklad_5 (h : A \/ B) : A \/ (B \/ C). Proof. Admitted.

V následujícím příkladu budete potřebovat hlouběji větvit důkaz. Použijte oddělovače - a +. Doplňte náznak důkazu.

Lemma disj_priklad_6 (h : (A \/ B) \/ C) : A \/ (B \/ C). Proof. destruct h as [avb | c]. - destruct avb as [a | b]. + left. assumption. + Admitted.

Úlohy s disjunkcí a konjunkcí

V následujících čtyřech úlohách samostatně dokážete takzvaná distributivní pravidla pro konjunkci a disjunkci.

Lemma disj_priklad_7 (h : A /\ (B \/ C)) : (A /\ B) \/ (A /\ C). Proof. Admitted. Lemma disj_priklad_8 (h : (A \/ B) /\ (A \/ C)) : A \/ (B /\ C). Proof. Admitted. Lemma disj_priklad_9 (h : (A /\ B) \/ (A /\ C)) : A /\ (B \/ C). Proof. Admitted. Lemma disj_priklad_10 (h : A \/ (B /\ C)) : (A \/ B) /\ (A \/ C). Proof. Admitted.

Úlohy s disjunkcí a implikací

Lemma disj_priklad_11 (h : (A -> B) \/ B) : A -> B. Proof. Admitted. Lemma disj_priklad_12 (h : A \/ B) : (A -> B) -> B. Proof. Admitted. Lemma disj_priklad_13 (h : (A -> B) -> (A -> C)) : (A \/ C) -> (B -> C). Proof. Admitted. Lemma disj_priklad_14 (h : (A -> B) \/ (A -> C)) : A -> (B \/ C). Proof. Admitted.

Disjunkce, konjunkce a implikace

Lemma disj_priklad_15 (h : (A -> B) /\ (B -> A)) : (A \/ B) -> (A /\ B). Proof. Admitted. Lemma disj_priklad_16 (h : (A \/ B) -> (A /\ B)) : (A -> B) /\ (B -> A). Proof. Admitted. Lemma disj_priklad_17 (h : (B -> C) /\ (B \/ A)) : (A -> B) -> (C /\ B). Proof. Admitted. End ulohy_disjunkce.