Require Import Bool Arith List. (* 6. Write the script that proves the following formula forall (P Q : nat -> Prop), forall (x y : nat), (forall z, P z -> Q z) -> x = y -> P x -> P x /\ Q y. *) Lemma ex6 : ... (* 8. Write the script that proves the following formula forall P : nat -> Prop, (forall x, P x) -> exists y:nat, P y /\ y = 0 *) Lemma ex8 : ... (* 1. Write a predicate multiple_of type nat -> nat -> Prop, so that multiple a b expresses that a is a multiple of b (in other words, there exists a number k such that a = k * b). *) Definition multiple_of a b := ... (* 2. Write a formula using natural numbers that expresses that when n is even (a multiple of 2) then n * n is even. *) ... even n ... Check forall n, even n -> even (n * n). (* 3. Write a formula using natural numbers that expresses that when a number n is a multiple of some k, then n * n is a multiple of k (you donâ€™t have to prove it yet). *) Check ... (* 4. Write a predicate odd of type nat -> Prop that characterize odd numbers like 3, 5, 37. Avoid ~ (even ..). *) ... odd n ... (* 9. Search the lemma proving associativity of multiplication *) SearchAbout ... (* 10. Write the script that proves that when n is a multiple of k, then n * n is also a multiple of k. *) Lemma ex10 : ... (* 11. Search the lemmas proving the following properties: - distributivity of plus and mult - associativity of plus - 1 is a neutral elelemt for multiplication *) ... (* 12. Show that the sum of two even numbers is even *) Lemma ex12 : ... (* 13. Write the script that proves that when n is odd, then n * n is also odd. *) Lemma ex13 : ...