(** Use [assert] to help prove this theorem. You shouldn't need to use induction. *) Theorem plus_swap : forall n m p : nat, n + (m + p) = m + (n + p). Proof. Admitted. (** Now prove commutativity of multiplication. (You will probably need to define and prove a separate subsidiary theorem to be used in the proof of this one.) You may find that [plus_swap] comes in handy. *) Theorem mult_comm : forall m n : nat, m * n = n * m. Proof. Admitted. (** Consider a different, more efficient representation of natural numbers using a binary rather than unary system. That is, instead of saying that each natural number is either zero or the successor of a natural number, we can say that each binary number is either - zero, - twice a binary number, or - one more than twice a binary number. (a) First, write an inductive definition of the type [bin] corresponding to this description of binary numbers. (Hint: recall that the definition of [nat] from class, [[ Inductive nat : Type := | O : nat | S : nat -> nat. ]] says nothing about what [O] and [S] "mean". It just says "[O] is a nat (whatever that is), and if [n] is a nat then so is [S n]". The interpretation of [O] as zero and [S] as successor/plus one comes from the way that we use nat values, by writing functions to do things with them, proving things about them, and so on. Your definition of [bin] should be correspondingly simple; it is the functions you will write next that will give it mathematical meaning.) (b) Next, write an increment function for binary numbers, and a function to convert binary numbers to unary numbers. (c) Finally, prove that your increment and binary-to-unary functions commute: that is, incrementing a binary number and then converting it to unary yields the same result as first converting it to unary and then incrementing. *) Inductive bin : Type := (* Fill in *) Fixpoint incr (m:bin) : bin := (* Fill in *) Fixpoint bin_to_nat(m:bin) : nat := (* Fill in *) Fixpoint bin_to_nat (m:bin) : nat := (* Fill in *) Theorem bin_to_nat_pres_incr : forall b : bin, bin_to_nat (incr b) = 1 + bin_to_nat b. Proof. Admitted.