(** Mathematics for Computer Scientists 2 (G52MC2) Thorsten Altenkirch Exercise 6 published 5/11/08, deadline 12/11/08, 17:00 electronic submission Use $ cw submit ex06.v on one of the CS servers then look for the coursework 227 labelled 'g52mc2 coursework 6' and enter the associated code. Multiple submissions are allowed, up to the deadline. Fill in the missing proofs. You are only supposed to use the tactics introduced in the lectures, e.g. cut, exact, assumption, intro(s), apply, split, elim, left, right, case, exists, reflexivity, rewrite(<-), pattern, discriminate, destruct, induction, injective. If you want to use another simple tactic not on the list, please check with your tutor. **) Section ex6. (* repeating some definitions from the lecture. *) Fixpoint is_even (n : nat) {struct n} : bool := match n with | 0 => true | S m => negb (is_even m) end. Fixpoint double (n : nat) {struct n} : nat := match n with | 0 => 0 | S m => S (S (double m)) end. (* show that double always produce even numbers. Use induction! *) Goal forall n : nat, is_even (double n) = true. (* insert your proof here. *) (* For the following we import a library module: *) Require Import Coq.Arith.Plus. (* It provides the following lemmas: Lemma plus_0_l : forall n, 0 + n = n. Lemma plus_0_r : forall n, n + 0 = n. Lemma plus_comm : forall n m, n + m = m + n. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. and more, see http://coq.inria.fr/stdlib/Coq.Arith.Plus.html *) Lemma double_lem : forall n:nat, double n = n+n. (* Hint: pattern is useful! *) (* We are (re)defining multiplication: *) Fixpoint mult (n m:nat) {struct n} : nat := match n with | O => 0 | S n' => m + mult n' m end. Notation "n * m" := (mult n m). (* Show that the law of distributivity holds: *) Goal forall (i j k:nat), i*(j+k) = i*j + i*k. (* insert your proof here. *) (* We define Le m n = less or equal *) Definition Le (m n : nat) := exists k:nat, k+m = n. Notation "n <= m" := (Le n m). (* Show that <= is a "partial order", i.e. it is reflexive, transitive and antisymmetric. Hint: You don't always need induction, try algebra instead. *) Lemma le_refl: forall n:nat,n <= n. (* insert your proof here *) Lemma le_trans : forall (l m n : nat), l <= m -> m <= n -> l <= n. (* insert your proof here *) Lemma le_asym : forall (m n : nat), m <= n -> n <= m -> m=n. (* insert your proof here *) (* Hint: The last lemma is not so easy. You should first try to show the following: Lemma asym_lem1 : forall (k j : nat), j+k=0 -> k=0. Lemma asym_lem2 : forall (k n : nat), n+k = n -> k=0. *)