Ćwiczenie 2. dobrze byłoby zrobić wielokrotnie :) Za pierwszym razem bez zmiennych egzystencjalnych, używając taktyk "bez e", potem ze zmiennymi egzystencjalnymi, aż do zrobienia dowodu (prawie) automatycznego.

1. Prove these tautologies of propositional logic, using only the tactics apply, assumption, constructor, destruct, intro, intros, left, right, split, and unfold.

• (True ∨ False) ∧ (False ∨ True)
• P → ¬ ¬ P
• P ∧ (Q ∨ R) → (P ∧ Q) ∨ (P ∧ R)

2. Prove the following tautology of first-order logic, using only the tactics apply, assert, assumption, destruct, eapply, eassumption, and exists. You will probably find the assert tactic useful for stating and proving an intermediate lemma, enabling a kind of “forward reasoning,” in contrast to the “backward reasoning” that is the default for Coq tactics. The tactic eassumption is a version of assumption that will do matching of unification variables. Let some variable T of type Set be the set of individuals. x is a constant symbol, p is a unary predicate symbol, q is a binary predicate symbol, and f is a unary function symbol.

• p x → (∀ x, p x → ∃ y, q x y) → (∀ x y, q x y → q y (f y)) → ∃ z, q z (f z )

3. Define an inductive predicate capturing when a natural number is an integer multiple of either 6 or 10. Prove that 13 does not satisfy your predicate, and prove that any number satisfying the predicate is not odd. It is probably easiest to prove the second theorem by indicating “odd-ness” as equality to 2 × n + 1 for some n.