Proving that Multiplication is commutative

If you'd like to write this more concisely (and without the use of tactics, solvers, etc...), you can rely on the fact that most of your needed lemmas are expressible in terms of your main goal theorems.

For example:

• n * 0 = 0 follows from mult_comm.
• n + 0 = n follows from plus_comm.
• S (n + m) = n + S m follows from plus_comm (by two rewrites and reduction).

With such things taken into account, mult_comm is relatively comfortably provable with just plus_assoc and plus_comm as lemmas:

Theorem plus_assoc : forall a b c, a + (b + c) = a + b + c.
Proof.
  intros.
  induction a.
    (* Case Z *)   reflexivity.
    (* Case S a *) simpl. rewrite IHa. reflexivity.
Qed.

Theorem plus_comm : forall a b, a + b = b + a.
Proof.
  induction a.
    (* Case Z *)
      induction b.
        (* Case Z *)   reflexivity.
        (* Case S b *) simpl. rewrite <- IHb. reflexivity.
    (* Case a = S a *)
      induction b.
        (* Case Z  *)
          simpl. rewrite (IHa 0). reflexivity.
        (* Case S b *)
          simpl. rewrite <- IHb.
          simpl. rewrite (IHa (S b)).
          simpl. rewrite (IHa b).
          reflexivity.
Qed.

Theorem mul_comm : forall a b, a * b = b * a.
Proof.
  induction a.
  (* Case Z *)
    induction b.
      (* Case Z *)   reflexivity.
      (* Case S b *) simpl. rewrite <- IHb. reflexivity.
  (* Case S a *)
    induction b.
      (* Case Z *)
        simpl. rewrite (IHa 0). reflexivity.
      (* Case S b *)
        simpl. rewrite <- IHb.
        rewrite (IHa (S b)).
        simpl. rewrite (IHa b).
        rewrite (plus_assoc b a (b * a)).
        rewrite (plus_assoc a b (b * a)).
        rewrite (plus_comm a b).
        reflexivity.
Qed.

---

NB: the lazy standard library way to do this would be the ring tactic:

Require Import Arith.

Theorem plus_comm2 : forall a b, a * b = b * a.
Proof. intros. ring. Qed.

Well, this is probably not what you wanted, but since you (originally) tagged in Haskell, and I just happened to work out how to do this in Haskell today, have some code!

{-# LANGUAGE TypeFamilies, GADTs, TypeOperators,
             ScopedTypeVariables, UndecidableInstances,
             PolyKinds, DataKinds #-}

import Data.Type.Equality
import Data.Proxy

data Nat = Z | S Nat
data SNat :: Nat -> * where
  Zy :: SNat 'Z
  Sy :: SNat n -> SNat ('S n)

infixl 6 :+
type family (:+) (m :: Nat) (n :: Nat) :: Nat where
  'Z :+ n = n
  'S m :+ n = 'S (m :+ n)

infixl 7 :*
type family (:*) (m :: Nat) (n :: Nat) :: Nat where
  'Z :* n = 'Z
  ('S m) :* n = n :+ (m :* n)

add :: SNat m -> SNat n -> SNat (m :+ n)
add Zy n = n
add (Sy m) n = Sy (add m n)

mul :: SNat m -> SNat n -> SNat (m :* n)
mul Zy _n = Zy
mul (Sy m) n = add n (mul m n)

addP :: proxy1 m -> proxy2 n -> Proxy (m :+ n)
addP _ _ = Proxy

mulP :: proxy1 m -> proxy2 n -> Proxy (m :* n)
mulP _ _ = Proxy

addAssoc :: SNat m -> proxy1 n -> proxy2 o ->
            m :+ (n :+ o) :~: (m :+ n) :+ o
addAssoc Zy _ _ = Refl
addAssoc (Sy m) n o = case addAssoc m n o of Refl -> Refl

zeroAddRightUnit :: SNat m -> m :+ 'Z :~: m
zeroAddRightUnit Zy = Refl
zeroAddRightUnit (Sy n) =
  case zeroAddRightUnit n of Refl -> Refl

plusSuccRightSucc :: SNat m -> proxy n ->
                     'S (m :+ n) :~: (m :+ 'S n)
plusSuccRightSucc Zy _ = Refl
plusSuccRightSucc (Sy m) n =
  case plusSuccRightSucc m n of Refl -> Refl

addComm :: SNat m -> SNat n ->
           m :+ n :~: n :+ m
addComm Zy n = sym $ zeroAddRightUnit n
addComm (Sy m) n =
  case addComm m n of
    Refl -> plusSuccRightSucc n m

mulComm :: SNat m -> SNat n ->
           m :* n :~: n :* m
mulComm Zy Zy = Refl
mulComm (Sy pm) Zy =
  case mulComm pm Zy of Refl -> Refl
mulComm Zy (Sy pn) = 
  case mulComm Zy pn of Refl -> Refl
mulComm (Sy m) (Sy n) =
  case mulComm m (Sy n) of {Refl ->
  case mulComm n (Sy m) of {Refl ->
  case addAssoc n m (mulP n m) of {Refl ->
  case addAssoc m n (mulP m n) of {Refl ->
  case addComm m n of {Refl ->
  case mulComm m n of Refl -> Refl}}}}}

---

Some extra free stuff!

distrR :: forall m n o proxy . SNat m -> proxy n -> SNat o ->
          (m :+ n) :* o :~: m :* o :+ n :* o
distrR Zy _ _ = Refl
distrR (Sy pm) n o =
  case distrR pm n o of {Refl ->
  case addAssoc o (mulP pm o) (mulP n o) of
    Refl -> Refl}

distrL :: SNat m -> SNat n -> SNat o ->
          m :* (n :+ o) :~: m :* n :+ m :* o
distrL m n o =
  case mulComm m (add n o) of {Refl ->
  case distrR n o m of {Refl ->
  case mulComm n m of {Refl ->
  case mulComm o m of Refl -> Refl}}}

mulAssoc :: SNat m -> SNat n -> SNat o ->
            m :* (n :* o) :~: (m :* n) :* o
mulAssoc Zy _ _ = Refl
mulAssoc (Sy pm) n o = case mulAssoc pm n o of {Refl ->
                       case distrR n (mulP pm n) o of Refl -> Refl}