Geek Answers Handbook

Proving that multiplication is commutative

So, this is one of the exercises that I worked from Software Foundations , in which I have to prove that animation is commutative. And this is my solution:

Theorem brack_help : forall nmp: nat, n + (m + p) = n + m + p. Proof. intros nm p. induction n as [| n']. Case "n = 0". simpl. reflexivity. Case "n = S n'". simpl. rewrite -> IHn'. reflexivity. Qed. Lemma plus_help: forall nm: 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 nm : 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 nmp : nat, n + (m + p) = m + (n + p). Proof. intros nm 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 mn : 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 mn : 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 mn : 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 rather cumbersome. Is there a more concise way to do this without using any library? (Note that to use Case tactics, you need a certain predefined code. The stand-alone working code is as follows: https://gist.github.com/psibi/1c80d61ca574ae62c23e ).

+6
source share
2 answers

If you want to write this more briefly (and without using tactics, solvers, etc.), you can rely on the fact that most of your necessary lemmas are expressed in terms of your main goal theorem.

For instance:

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

When accounting for such things, mult_comm relatively conveniently provable only with plus_assoc and plus_comm in the form of lemmas:

 Theorem plus_assoc : forall abc, 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 ab, 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 ab, 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 ba (b * a)). rewrite (plus_assoc ab (b * a)). rewrite (plus_comm ab). reflexivity. Qed.

NB: the lazy standard library way to do this is ring tactics:

 Require Import Arith. Theorem plus_comm2 : forall ab, a * b = b * a. Proof. intros. ring. Qed.
+11
source

Well, this is probably not what you wanted, but since you were (originally) tagged in Haskell, and I just managed to figure out how to do it in Haskell today, you have the 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 ( n) infixl 6 :+ type family (:+) (m :: Nat) (n :: Nat) :: Nat where 'Z :+ n = n m :+ n = (m :+ n) infixl 7 :* type family (:*) (m :: Nat) (n :: Nat) :: Nat where 'Z :* n = 'Z ( m) :* n = n :+ (m :* n) add :: SNat m -> SNat n -> SNat (m :+ n) add Zy n = n add (Sy m) n = Sy (add mn) mul :: SNat m -> SNat n -> SNat (m :* n) mul Zy _n = Zy mul (Sy m) n = add n (mul mn) 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) no = case addAssoc mno 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 -> (m :+ n) :~: (m :+ n) plusSuccRightSucc Zy _ = Refl plusSuccRightSucc (Sy m) n = case plusSuccRightSucc mn of Refl -> Refl addComm :: SNat m -> SNat n -> m :+ n :~: n :+ m addComm Zy n = sym $ zeroAddRightUnit n addComm (Sy m) n = case addComm mn of Refl -> plusSuccRightSucc nm 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 nm (mulP nm) of {Refl -> case addAssoc mn (mulP mn) of {Refl -> case addComm mn of {Refl -> case mulComm mn of Refl -> Refl}}}}}

Some additional free stuff!

 distrR :: forall mno proxy . SNat m -> proxy n -> SNat o -> (m :+ n) :* o :~: m :* o :+ n :* o distrR Zy _ _ = Refl distrR (Sy pm) no = case distrR pm no of {Refl -> case addAssoc o (mulP pm o) (mulP no) of Refl -> Refl} distrL :: SNat m -> SNat n -> SNat o -> m :* (n :+ o) :~: m :* n :+ m :* o distrL mno = case mulComm m (add no) of {Refl -> case distrR nom of {Refl -> case mulComm nm of {Refl -> case mulComm om of Refl -> Refl}}} mulAssoc :: SNat m -> SNat n -> SNat o -> m :* (n :* o) :~: (m :* n) :* o mulAssoc Zy _ _ = Refl mulAssoc (Sy pm) no = case mulAssoc pm no of {Refl -> case distrR n (mulP pm n) o of Refl -> Refl}
+9
source

More articles:


All Articles