(* Exercise coq_nat_09 *)
(* Now, let us prove that multiplication is commutative *)
(* For this we may need to use some properties of addition and multiplication
that we proved before. *)
Require Import Arith.
Check mult_0_r.
Check plus_comm.
Check plus_assoc.
(* ... and a following auxiliary lemma *)
Lemma mult_succ : forall m n, n + n * m = n * S m.
Proof.
intros.
(* Rule of thumb: Do induction over the argument that
the function does recursion over.
For plus and mult, that is the first argument *)
induction n.
- simpl.
reflexivity.
(* General pattern that often works:
= simpl (to do some computation steps with teh defined functions)
= find a way to rewrite with the IH
= use auxiliary lemmas *)
- simpl.
rewrite <- IHn.
rewrite plus_assoc.
rewrite (plus_comm n m).
(* Note the explicit argument I give to plus_comm
to rewrite the specific subterm *)
rewrite <- plus_assoc.
reflexivity.
Qed.
Lemma mult_comm : forall m n, m * n = n * m.
Proof.
intros.
induction n.
- simpl.
rewrite mult_0_r.
reflexivity.
- simpl.
rewrite <- IHn.
rewrite mult_succ.
reflexivity.
Qed.
(* As commutativity is very much a symmetric property in the two
arguments, you can also do induction m and the proof is basically
the same *)
Lemma mult_comm' : forall m n, m * n = n * m.
Proof.
intros.
induction m.
- simpl.
rewrite mult_0_r.
reflexivity.
- simpl.
rewrite IHm.
rewrite mult_succ.
reflexivity.
Qed.