Library Coq.Arith.Mult

Properties of multiplication.

This file is mostly OBSOLETE now, see module PeanoNat.Nat instead.

Nat.mul is defined in Init/Nat.v.

Require Import PeanoNat.

For Compatibility:

Require Export Plus Minus Le Lt.

Local Open Scope nat_scope.

Notation mult_0_l := Nat.mul_0_l (only parsing). Notation mult_0_r := Nat.mul_0_r (only parsing).

Notation mult_1_l := Nat.mul_1_l (only parsing). Notation mult_1_r := Nat.mul_1_r (only parsing).
Hint Resolve mult_1_l mult_1_r: arith.

Notation mult_comm := Nat.mul_comm (only parsing).
Hint Resolve mult_comm: arith.

Notation mult_plus_distr_r :=
  Nat.mul_add_distr_r (only parsing).
Notation mult_plus_distr_l :=
  Nat.mul_add_distr_l (only parsing).
Notation mult_minus_distr_r :=
  Nat.mul_sub_distr_r (only parsing).
Notation mult_minus_distr_l :=
  Nat.mul_sub_distr_l (only parsing).
Hint Resolve mult_plus_distr_r: arith.
Hint Resolve mult_minus_distr_r: arith.
Hint Resolve mult_minus_distr_l: arith.

Notation mult_assoc := Nat.mul_assoc (only parsing).
Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p ).

Hint Resolve mult_assoc_reverse: arith.
Hint Resolve mult_assoc: arith.

Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0.

Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1.

Notation mult_succ_l := Nat.mul_succ_l (only parsing). Notation mult_succ_r := Nat.mul_succ_r (only parsing).

Lemma mult_O_le n m : m = 0 \/ n <= m * n.
Hint Resolve mult_O_le: arith.

Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
Hint Resolve mult_le_compat_l: arith.

Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.

Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q.

Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p.

Hint Resolve mult_S_lt_compat_l: arith.

Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.

Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p.

Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p.

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

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.