Konjunkce ========= V této kapitole se budeme zabývat logickou spojkou konjunkce. Je to spojka přibližně odpovídající spoje "a" v přirozeném jazyce, a práce s ní je v přirozené dedukci velmi intuitivní. Konjunkce umožňuje spojit dva výroky ``A`` a ``B`` do složeného výroku, jehož význam je "``A`` a ``B`` platí současně". Uvidíme, že pravidla pro práci s konjunkcí věrně kopírují způsob, jakým se spojkou "a" obvykle pracujeme. Syntax konjunkce ---------------- V matematické logice se konjunkce výroků ``A`` a ``B`` obvykle zapisuje stříškou jako ``A ∧ B``. Pro naše účely je vhodné používat syntax bez speciálního symbolu, aby bylo snazší ji rychle zapsat. Konjunkci ``A`` a ``B`` tedy budeme značit ``A /\ B`` - stříšku zapisujeme dopředným a zpětným lomítkem. Pravidla pro práci se spojkou konjunkce --------------------------------------- Téměř u všech spojek, které zavedeme, budeme potřebovat zavést i dvě pravidla pro práci s nimi: pravidlo *zavedení* dané spojky a pravidlo *eliminace* dané spojky. Pravidlo zavedení nám říká, co vše musíme vědět, abychom byli přesvědčeni o platnosti výroku, ve kterém se daná spojka vyskytuje. Pravidlo eliminace nám dává návod, jak využít platnost výroku využívajícího danou spojku k odvození dalších tvrzení. V případě konjunkce je velmi snadné pravidla zavedení a eliminace vyslovit a pochopit. Pravidlo zavedení konjunkce ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Nejprve neformálně: když víme, že prší, a když navíc víme, že je mlha, tak můžeme naše dvě znalosti spojit do jedné (větší) znalosti "prší a je mlha". Tak se spojka "a" v přirozeném jazyce používá: skládá několik tvrzení dohromady. Mírně formálněji: když víme, že platí výrok ``A`` a víme, že platí výrok ``B``, pak můžeme začít tvrdit, že platí výrok ``A /\ B``. Tím jsme *zavedli* konjunkci výroků ``A`` a ``B``. Nyní už můžeme naše odvozovací pravidlo vyslovit přesně: umíme-li z množiny předpokladů ``Gamma`` odvodit ``A`` (to zapisujeme symbolicky jako ``Gamma |- A``), a umíme-li z ``Gamma`` odvodit i ``B`` (symbolicky ``Gamma |- B``), pak z množiny předpokladů ``Gamma`` umíme odvodit i ``A /\ B``. Tento fakt zapisujeme jako odvozovací pravidlo: :: Gamma |- A Gamma |- B ---------------------- Gamma |- A /\ B Toto pravidlo nazýváme **zavedení konjunkce**. Pravidlo eliminace konjunkce ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Znovu zmíníme nejprve neformální příklad: když víme, že sněží a fouká, tak speciálně víme, že sněží. Tento úsudek nám přijde zcela trivální. Proč tomu tak je? Protože přesně takto se spojka "a" v našem jazyce chová: když víme více věcí dohromady, tak jistě víme i každou z daných věcí zvlášť. Mírně formálněji: když víme, že platí výrok ``A /\ B``, pak můžeme tvrdit, že platí i výrok ``A``. (A samozřejmě také můžeme tvrdit, že platí i výrok ``B``.) Tím jsme *eliminovali* konjunkci ``A /\ B``, využili jsme ji k "extrakci" informace v ní uložené. Jak přesně formulovat toto odvozovací pravidlo? Umíme-li z množiny předpokladů ``Gamma`` odvodit ``A /\ B`` (symbolicky ``Gamma |- A /\ B``), pak umíme z ``Gamma`` odvodit i ``A`` (symbolicky ``Gamma |- A``). A podobně umíme z ``Gamma |- A /\ B`` odvodit i ``Gamma |- B``. Tento fakt zapisujeme jako *dvě* odvozovací pravidla: :: Gamma |- A /\ B --------------- Gamma |- A Gamma |- A /\ B --------------- Gamma |- B Tato dvě pravidla nazýváme **eliminace konjunkce**. Práce s konjunkcí v Coq ~~~~~~~~~~~~~~~~~~~~~~~ Nyní si ukážeme několik jednoduchých příkladů, na kterých předvedeme, jak se s konjunkcí dá pracovat v Coqu. Nejprve zavedeme novou sekci, ve které do kontextu přidáme výroky ``A, B, C, D``. Připomeňme: zavedením těchto výroků netvrdíme, že platí! Pouze se o nich díky zavedení můžeme začít vyjadřovat. Podobně v přirozeném jazyce můžeme vyřknout výrok "Prší.", aniž by byl pravdivý. .. coq:: Section priklady_konjunkce. Set Printing Parentheses. Context (A B C D : Prop). V Coqu pravidlo zavedení konjunkce používáme příkazem ``split``. Když máme za cíl dokázat ``A /\ B``, rozdělí se nám cíl na dva *podcíle*: v jednom budeme muset dokázat ``A`` a ve druhém ``B``. V následujícím příkladu máme dokázat právě ``A /\ B`` (výrok za dvojtečkou), a naše *předpoklady* jsou ``A`` a ``B``. Značením ``a : A`` uvádíme, že výrok ``A`` platí, a důkaz jeho platnosti označujeme jako ``a``. Podobně ``b`` je důkazem platnosti ``B``. .. coq:: Lemma konj_priklad_1 (a : A) (b : B) : A /\ B. Proof. split. - assumption. - assumption. Qed. V obou podcílech jsme měli dokázat něco, co jsme předpokládali: použili jsme tedy příkaz ``assumption``. Všimněte si, že jednotlivé podcíle označujeme značkou ``-``, aby byl důkazový skript přehlednější. V dalším příkladu máme za cíl dokázat ``B`` z předpokladu ``(A /\ B) /\ C``. Zde bude zjevně potřeba eliminovat konjunkci, kterou předpokládáme. Důkaz dané konjunkce označen jako ``d``; eliminace se provádí příkazem ``destruct d``. Tím se změní naše množina předpokladů: místo jednoho předpokladu tvaru ``(A /\ B) /\ C`` budeme mít k disposici dva předpoklady: jeden tvaru ``A /\ B``, a jeden tvaru ``C``. Všimněte si, že jsme skutečně "eliminovali" spojku konjunkce. Příkazu ``destruct d`` jsme přidali nepovinný argument ``as [ab c]``, který slouží k tomu, abychom označili důkazy nově vzniklých předpokladů ``A /\ B`` a ``C``. Jejich pojmenování (``ab`` a ``c``) je čistě na nás. .. coq:: Lemma konj_priklad_2 (d : (A /\ B) /\ C) : B. Proof. destruct d as [ab c]. destruct ab as [a b]. assumption. Qed. Ve třetím příkladu budeme potřebovat jak pravidlo zavedení, tak pravidlo eliminace. Naším cílem je dokázat, že spojka konjunkce je "významově komutativní": výroky ``A /\ B`` a ``B /\ A`` sice nejsou *totožné*, ale mají "stejný význam": z prvního lze dokázat druhý, a naopak z druhého lze dokázat první. My provedeme jen jeden směr důkazu, druhý můžete zkusit sami formulovat a dokázat (nicméně důkaz je v podstatě totožný). .. coq:: Lemma konj_priklad_3 (ab : A /\ B) : B /\ A. Proof. destruct ab as [a b]. split. - assumption. - assumption. Qed. Čtvrtý příklad už není konceptuálně obtížnější. Pouze zde již máme dva složitější předpoklady a máme dokázat složitější závěr. \ .. coq:: Lemma konj_priklad_4 (ba : B /\ A) (c : C) : A /\ (C /\ B). Proof. destruct ba as [b a]. split. - assumption. - split. + assumption. + assumption. Qed. End priklady_konjunkce. Nyní jste již vybaveni vším, co potřebujete k důkazům tvrzení týkajících se čistě spojky konjunkce. 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_konjunkce. Context (A B C D E : Prop). Lemma konj_uloha_1 (ab : A /\ B) (cde: (C /\ D) /\ E) : (A /\ D) /\ E. Proof. Admitted. Lemma konj_uloha_2 (abc: A /\ (B /\ C)) : (C /\ A) /\ B. Proof. Admitted. End ulohy_konjunkce.