Set Implicit Arguments. Require Import Coq.Arith.Arith. Require Import Setoid. Fixpoint mult (n m : nat) : nat := match n with | O => O | S n' => plus m (mult n' m) end. Fixpoint plus (n : nat) (m : nat) : nat := match n with | O => m | S n' => S (plus n' m) end. Fixpoint minus (n m:nat) : nat := match n, m with | O , _ => O | S _ , O => n | S n', S m' => minus n' m' end. Lemma plus_asso x y z : plus (plus x y) z = plus x (plus y z). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma plus_S x y: plus x (S y) = S (plus x y). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma plus_com : forall x y : nat, plus x y = plus y x. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_S x y : mult x (S y) = plus (mult x y) x. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_O (x : nat) : mult x O = O. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_S' (x y : nat) : mult x (S y) = plus (mult x y) x. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_com (x y : nat) : mult x y = mult y x. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_dist (x y z: nat) : mult (plus x y) z = plus (mult x z) (mult y z). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_asso (x y z: nat) : mult (mult x y) z = mult x (mult y z). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma mult_dist' x y z : x * (y + z) = x*y + x*z. (* Hint: you might find the tactic f_equal, a variant of reflexivity, that leverages the principle of functional extensionality useful here. *) Proof. (* FILL IN HERE *) Admitted. (** [] *) Fixpoint iter (n : nat) (X : Type) (f : X -> X) (x : X) : X := match n with | 0 => x | S n' => f (iter n' f x) end. Lemma iter_plus x y : x + y = iter x S y. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma iter_minus x y : x - y = iter y pred x. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma iter_mult x y : x * y = iter x (plus y) 0. Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma iter_shift X (f : X -> X) x n : iter (S n) f x = iter n f (f x). Proof. (* FILL IN HERE *) Admitted. (** [] *) Lemma iter_power x n : power x n = iter n (mult x) 1. Proof. (* FILL IN HERE *) Admitted. (** [] *)