(*** Semantics, Coq part of Assignment 1 ***) (*** Solutions ***) (*** Use Coq to complete the file below. If you have any questions, please use the discussion board. http://www.ps.uni-saarland.de/courses/cl-ss11/forum/ ***) Inductive bool : Type := | false : bool | true : bool. Definition negb (x : bool) : bool := match x with | false => true | true => false end. Definition andb (x y : bool) : bool := match x with | false => false | true => y end. (*** Exercise 1.1 ***) Definition orb (x y : bool) : bool := match x with | false => y | true => true end. Lemma ex_1_1b (x y : bool) : negb (orb x y) = andb (negb x) (negb y). Proof. destruct x ; destruct y ; reflexivity. Qed. Inductive nat := | O : nat | S : nat -> nat. Fixpoint add (x y : nat) : nat := match x with | O => y | S x' => S (add x' y) end. Fixpoint mul (x y: nat) : nat := match x with | O => O | S x' => add (mul x' y) y end. Definition pred (x : nat) : nat := match x with | O => O | S x' => x' end. (*** Exercise 1.2 ***) Fixpoint power (x n : nat) : nat := match n with | O => (S O) | S n' => mul x (power x n') end. Fixpoint fac (n : nat) : nat := match n with | O => (S O) | S n' => mul n (fac n') end. Fixpoint even (n : nat) : bool := match n with | O => true | S n => negb (even n) end. Fixpoint mod3 (n : nat) : nat := match n with | S (S (S n)) => mod3 n | n => n end. Lemma add_O (x : nat) : add x O = x. Proof. induction x ; simpl. reflexivity. rewrite IHx. reflexivity. Qed. Lemma add_S (x y : nat) : add x (S y) = S (add x y). Proof. induction x ; simpl. reflexivity. rewrite IHx. reflexivity. Qed. Lemma add_com (x y : nat) : add x y = add y x. Proof. induction x ; simpl. rewrite add_O. reflexivity. rewrite add_S. rewrite IHx. reflexivity. Qed. Lemma add_asso (x y z: nat) : add (add x y) z = add x (add y z). Proof. induction x ; simpl. reflexivity. rewrite IHx. reflexivity. Qed. (*** Exercise 1.3 ***) Lemma mul_O (x:nat): mul x O = O. Proof. induction x. reflexivity. simpl. rewrite IHx. reflexivity. Qed. Lemma mul_S (x y:nat): mul x (S y) = add (mul x y) x. (*** (*** Solution 1 ***) Proof. induction x; simpl. reflexivity. rewrite IHx. rewrite add_S. rewrite add_asso. rewrite add_S. rewrite add_asso. rewrite (add_com y). reflexivity. Qed. ***) (*** Solution 2 ***) Proof. induction x; simpl. reflexivity. rewrite IHx. rewrite add_asso. rewrite add_asso. f_equal. rewrite add_S. rewrite add_S. rewrite add_com. reflexivity. Qed. Lemma mul_com (x y:nat): mul x y = mul y x. Proof. induction x ; simpl. rewrite mul_O. reflexivity. rewrite mul_S. rewrite IHx. reflexivity. Qed. Lemma mul_dist (x y z:nat): mul (add x y) z = add (mul x z) (mul y z). (*** (*** Solution 1 ***) Proof. induction x ; simpl. reflexivity. rewrite IHx. rewrite add_asso. rewrite add_asso. rewrite (add_com (mul y z)). reflexivity. Qed. ***) (*** Solution 2 ***) Proof. induction x ; simpl. reflexivity. rewrite IHx. rewrite add_asso. rewrite add_asso. f_equal. rewrite add_com. reflexivity. Qed. Lemma mul_asso (x y z:nat): mul (mul x y) z = mul x (mul y z). induction x ; simpl. reflexivity. rewrite mul_dist. rewrite IHx. reflexivity. Qed.