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).
Commutative comes from the word “commute”, which can be defined as moving around or traveling. According to the commutative property of multiplication, changing the order of the numbers we are multiplying does not change the product.
The commutative property can be verified using addition or multiplication. This is because the order of terms does not affect the result when adding or multiplying. For example, when multiplying 5 and 7, the order does not matter. (5)×(7)=35 and (7)×(5)=35.
We know that for any two integers a and b, commutativity holds for the operations addition and multiplication. Thus, we have \[a+b=b+a\] and \[ab=ba\]. So, we have \[b*a=b+a+ba=a+b+ab=a*b\]. Thus, commutative property holds for the binary relation \['*'\].
The commutative property is a math rule that says that the order in which we multiply numbers does not change the product.
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}
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With