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

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.

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?

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.

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