Library Stdlib.Numbers.NatInt.NZMul


Some properties of the multiplication for modules implementing NZBasicFunsSig'

This file defines the NZMulProp functor type on top of NZAddProp. This functor type is meant to be Included in a module implementing NZBasicFunsSig'.
This gives the following basic lemmas:
  • mul_0_r, mul_1_l, mul_1_r
  • mul_succ_r, mul_comm
  • mul_add_distr_r, mul_add_distr_l
  • mul_assoc
  • mul_shuffle0 and mul_shuffle3 to rearrange products of 3 terms
  • mul_shuffle1 and mul_shuffle2 to rearrange products of 4 terms
Notice that NZMulProp itself Includes NZAddProp.

From Stdlib.Numbers.NatInt Require Import NZAxioms NZBase NZAdd.

Module Type NZMulProp (Import NZ : NZBasicFunsSig')(Import NZBase : NZBaseProp NZ).
Include NZAddProp NZ NZBase.

Theorem mul_0_r : forall n, n * 0 == 0.

Theorem mul_succ_r : forall n m, n * (S m) == n * m + n.

Global Hint Rewrite mul_0_r mul_succ_r : nz.

Theorem mul_comm : forall n m, n * m == m * n.

Theorem mul_add_distr_r : forall n m p, (n + m) * p == n * p + m * p.

Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.

Theorem mul_assoc : forall n m p, n * (m * p) == (n * m) * p.

Theorem mul_1_l : forall n, 1 * n == n.

Theorem mul_1_r : forall n, n * 1 == n.

Global Hint Rewrite mul_1_l mul_1_r : nz.

Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m.

Theorem mul_shuffle1 : forall n m p q, (n * m) * (p * q) == (n * p) * (m * q).

Theorem mul_shuffle2 : forall n m p q, (n * m) * (p * q) == (n * q) * (m * p).

Theorem mul_shuffle3 : forall n m p, n * (m * p) == m * (n * p).

End NZMulProp.