.. coq::

   From CoqBook Require Export Taktiky.

Implikace a konjunkce
=====================

Tato kapitola slouží k opakování a prohloubení znalostí získaných v kapitolách týkajících se konjunkce a implikace.

Naleznete zde sedm důkazových úloh, v jejichž zadání se vyskytují výroky obsahující jak konjunkce, tak implikace. Ke správnému řešení tedy budete potřebovat kombinovat všechna zatím probraná odvozovací pravidla.

Příklady a úlohy
----------------

.. coq::

   Section ulohy_implikace_konjunkce.

     Context (A B C : Prop).

   Lemma impl_konj_priklad_1 (ab : A /\ B) : A -> B.
   Proof.
     destruct ab as [a b].
     intro a'.
     assumption.
   Qed.

   Lemma impl_konj_priklad_2 : (A /\ B) -> B.
   Proof.
   Admitted.

   Lemma impl_konj_priklad_3 (h : A -> (B /\ C)) : A -> B.
   Proof.
   Admitted.

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

Možná jste si všimli, že po použití ``impl_elim h`` bylo vaším cílem dokázat tvrzení, které jste dokazovali už v příkladu ``impl_konj_priklad_2``. Toho můžeme využít a "nevynalézat znovu kolo": Coq umožňuje již dokázaná tvrzení používat znovu jako stavební bloky do dalších důkazů. V tomto případě je relevantní příkaz ``apply impl_konj_priklad_2``.

.. coq::

   Lemma impl_konj_priklad_4'
     (h : ((A /\ B) -> B) -> (B -> A)) : B -> A.
   Proof.
     impl_elim h.
     apply impl_konj_priklad_2.
   Qed.


   Lemma impl_konj_priklad_5 (h : (A /\ B) -> C) : A -> (B -> C).
   Proof.
   Admitted.

Následující úloha je pro vás vyřešena "zpětným" způsobem dokazování níže. Zvládnete ji dokázat "dopředným" způsobem? Který způsob se vám líbí více?

.. coq::

   Lemma impl_konj_priklad_6 (h : (A -> B) /\ (A -> C)) : A -> (B /\ C).
   Proof.
   Admitted.

   Lemma impl_konj_priklad_6' (h : (A -> B) /\ (A -> C)) : A -> (B /\ C).
   Proof.
     intro a.
     destruct h as [ab ac].
     split.
     - impl_elim ab.
       assumption.
     - impl_elim ac.
       assumption.
   Qed.

V následující úloze se vám "dopředný" způsob eliminace implikace bude hodit.

.. coq::

   Lemma impl_konj_priklad_7 (h : A -> (B /\ C)) : (A -> B) /\ (A -> C).
   Proof.
   Admitted.

   End ulohy_implikace_konjunkce.