Proving that Multiplication is commutative

Question

So this is one of the exercise I have been working from Software Foundations in which I have to prove that multipication is commutative. And this is my solution:

Theorem brack_help : forall n m p: nat,
  n + (m + p) = n + m + p.
Proof.
  intros n m p.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Lemma plus_help: forall n m: nat,
  S (n + m) = n + S m.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    reflexivity.
Qed.

Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
  intros n.
  induction n as [|n'].
  Case "n = 0".
    simpl.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite -> IHn'.
    reflexivity.
Qed.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros n m.
  induction n as [| n].
  Case "n = 0".
    simpl.
    rewrite <- plus_n_O.
    reflexivity.
  Case "n = S n".
    simpl.
    rewrite -> IHn.
    rewrite -> plus_help.
    reflexivity.
Qed.

Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.  
  intros n m p.
  rewrite -> brack_help.
  assert (H: n + m = m + n).
    Case "Proof of assertion".
    rewrite -> plus_comm.
    reflexivity.
  rewrite -> H.
  rewrite <- brack_help.
  reflexivity.
Qed.

Lemma mult_help : forall m n : nat,
  m + (m * n) = m * (S n).
Proof.
  intros m n.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite <- IHm'.
    rewrite -> plus_swap.
    reflexivity.
Qed.    

Lemma mult_identity : forall m : nat,
 m * 1 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Lemma plus_0_r : forall m : nat,
 m + 0 = m.
Proof.
  intros m.
  induction m as [| m'].
  Case "m = 0".
    simpl.
    reflexivity.
  Case "m = S m'".
    simpl.
    rewrite -> IHm'.
    reflexivity.
Qed.

Theorem mult_comm_helper : forall m n : nat,
  m * S n = m + m * n.
Proof.
  intros m n.
  simpl.
  induction n as [| n'].
  Case "n = 0".
    assert (H: m * 0 = 0).
    rewrite -> mult_0_r.
    reflexivity.
    rewrite -> H.
    rewrite -> mult_identity.
    assert (H2: m + 0 = m).
    rewrite -> plus_0_r.
    reflexivity.
    rewrite -> H2.
    reflexivity.
  Case "n = S n'".
    rewrite -> IHn'.
    assert (H3: m + m * n' = m * S n').
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H3.
    assert (H4: m + m * S n' = m * S (S n')).
    rewrite -> mult_help.
    reflexivity.
    rewrite -> H4.
    reflexivity.
Qed.

Theorem mult_comm : forall m n : nat,
 m * n = n * m.
Proof.
  intros m n.
  induction n as [| n'].
  Case "n = 0".
    simpl.
    rewrite -> mult_0_r.
    reflexivity.
  Case "n = S n'".
    simpl.
    rewrite <- IHn'.
    rewrite -> mult_comm_helper.
    reflexivity.
Qed.

Now in my opinion, this proof is quite bulky. Is there a more concise way of doing this without using any library ? (Note that for using the Case tactic you need some predefined code. A self contained working code is in the following gist: https://gist.github.com/psibi/1c80d61ca574ae62c23e).

Filings

@Carsten makes a good point—there are several slightly different ways to define multiplication, and exactly what's easy and what's hard seems pretty sensitive to which you choose. Of course, what makes one thing easy is almost certain to make another hard. – Stunk

@Carsten Even if i did induction on m, I would still need mult_comm_helper (Just the rewrite direction would be different in the proof in that case). The * is defined in terms of addition. :) – Filings

@Filings - as I said it's probably not true (I just remembered something similar where the choice did matter a lot) - that * is defined in terms of addition is obvious - the question is if you define it with n * S m = ... or S n * m = ... - but nevermind it probably will not help you at all - hopefully someone who did the exercises too will eventually come around and enlighten us (maybe I'll have a look this evening) – Lailaibach

Your solution is the same as in the Agda standard library. – Aekerly

@user3237465 I only see commutative property of addition proved there. Is it proved for multiplication there ? – Filings

@Filings It's here. – Izy

Answer 1

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.

Kubis

Answer 2

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}

Stunk

Works good when removing E. from that. Thanks for this. +1. Although I'm more interested in a Coq solution. :) – Filings

@Sibi, I figured. I've played with Haskell a lot, and Idris a decent bit, and Agda a very small amount. I've never even touched Coq, so you'll probably have to wait for someone else. I think some of this stuff is a slog no matter how you do it. It's nowhere near as painful as constructing the integers though. – Stunk

Answer 3

You can also solve it like this :

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros.
  induction m.
  - rewrite <- mult_n_O. reflexivity.
  - rewrite <- mult_n_Sm.
    rewrite <- plus_1_l.
    simpl.
    rewrite <- IHm.
    rewrite -> plus_comm.
    reflexivity.
Qed.

the trick is to rewrite S m * n to (1 + m) * n (using plus_1_l)

which will then simplify to n + m * n

for reference :

mult_n_O : forall n : nat, 0 = n * 0
mult_n_Sm : forall n m : nat, n * m + n = n * S m
plus_1_l : forall n : nat, 1 + n = S n
plus_comm : forall n m : nat, n + m = m + n

Penalize

Answer 4

Here's the solution I came up with for this problem using assert to create a helper theorem, which I believe was the topic the book is discussing in this particular section.

Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Proof.
  intros m n.
  induction m as [| m' IHm'].
  - rewrite mul_0_r.
    reflexivity.
  - simpl.
    rewrite -> IHm'.
    assert (H: forall a b : nat, a * (1 + b) = a + a * b).
    {
      intros a b.
      induction a as [| a' IHa'].
      - reflexivity.
      - rewrite <- mult_n_Sm.
        rewrite -> add_comm.
        reflexivity.
    }
    rewrite -> H.
    reflexivity.
Qed.

Anselme