# Library Coq.Arith.Mult

Require Export Plus.
Require Export Minus.
Require Export Lt.
Require Export Le.
Local Open Scope nat_scope.
Implicit Types m n p : nat.
Theorems about multiplication in nat. mult is defined in module Init/Peano.v.

# nat is a semi-ring

## Zero property

Lemma mult_0_r : forall n, n * 0 = 0.
Lemma mult_0_l : forall n, 0 * n = 0.

## 1 is neutral

Lemma mult_1_l : forall n, 1 * n = n.
Hint Resolve mult_1_l: arith v62.
Lemma mult_1_r : forall n, n * 1 = n.
Hint Resolve mult_1_r: arith v62.

## Commutativity

Lemma mult_comm : forall n m, n * m = m * n.
Hint Resolve mult_comm: arith v62.

## Distributivity

Lemma mult_plus_distr_r : forall n m p, ( n + m ) * p = n * p + m * p.
Hint Resolve mult_plus_distr_r: arith v62.
Lemma mult_plus_distr_l : forall n m p, n * ( m + p ) = n * m + n * p.
Lemma mult_minus_distr_r : forall n m p, ( n - m ) * p = n * p - m * p.
Hint Resolve mult_minus_distr_r: arith v62.
Lemma mult_minus_distr_l : forall n m p, n * ( m - p ) = n * m - n * p.
Hint Resolve mult_minus_distr_l: arith v62.

## Associativity

Lemma mult_assoc_reverse : forall n m p, n * m * p = n * ( m * p ).
Hint Resolve mult_assoc_reverse: arith v62.
Lemma mult_assoc : forall n m p, n * ( m * p ) = n * m * p.
Hint Resolve mult_assoc: arith v62.

## Inversion lemmas

Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0.
Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1.

## Multiplication and successor

Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m.
Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n.

# Compatibility with orders

Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n.
Hint Resolve mult_O_le: arith v62.
Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m.
Hint Resolve mult_le_compat_l: arith.
Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p.
Lemma mult_le_compat :
forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q.
Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p.
Hint Resolve mult_S_lt_compat_l: arith.
Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m.
Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p.
Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p.

# n|->2*n and n|->2n+1 have disjoint image

Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q.

# Tail-recursive mult

tail_mult is an alternative definition for mult which is tail-recursive, whereas mult is not. This can be useful when extracting programs.
Fixpoint mult_acc (s:nat) m n : nat :=
match n with
| O => s
| S p => mult_acc (tail_plus m s) m p
end.
Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n.
Definition tail_mult n m := mult_acc 0 m n.
Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.
TailSimpl transforms any tail_plus and tail_mult into plus and mult and simplify
Ltac tail_simpl :=
repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;
simpl.