Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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.

nat is a semi-ring

Zero property

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

1 is neutral

Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *)
Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *)

Hint Resolve mult_1_l mult_1_r: arith.

Commutativity

Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *)

Hint Resolve mult_comm: arith.

Distributivity

Notation mult_plus_distr_r :=
  Nat.mul_add_distr_r (only parsing). (* (n+m)*p = n*p + m*p *)

Notation mult_plus_distr_l :=
  Nat.mul_add_distr_l (only parsing). (* n*(m+p) = n*m + n*p *)

Notation mult_minus_distr_r :=
  Nat.mul_sub_distr_r (only parsing). (* (n-m)*p = n*p - m*p *)

Notation mult_minus_distr_l :=
  Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *)

Hint Resolve mult_plus_distr_r: arith.
Hint Resolve mult_minus_distr_r: arith.
Hint Resolve mult_minus_distr_l: arith.

Associativity

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

Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p).n, m, p:nat
n * m * p = n * (m * p)
Proof.n, m, p:nat
n * m * p = n * (m * p)
 symmetry.n, m, p:nat
n * (m * p) = n * m * p apply Nat.mul_assoc.
Qed.

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

Inversion lemmas

Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0.n, m:nat
n * m = 0 -> n = 0 \/ m = 0
Proof.n, m:nat
n * m = 0 -> n = 0 \/ m = 0
 apply Nat.eq_mul_0.
Qed.

Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1.n, m:nat
n * m = 1 -> n = 1 /\ m = 1
Proof.n, m:nat
n * m = 1 -> n = 1 /\ m = 1
 apply Nat.eq_mul_1.
Qed.

Multiplication and successor

Notation mult_succ_l := Nat.mul_succ_l (only parsing). (* S n * m = n * m + m *)
Notation mult_succ_r := Nat.mul_succ_r (only parsing). (* n * S m = n * m + n *)

Compatibility with orders

Lemma mult_O_le n m : m = 0 \/ n <= m * n.n, m:nat
m = 0 \/ n <= m * n
Proof.n, m:nat
m = 0 \/ n <= m * n
 destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
Qed.
Hint Resolve mult_O_le: arith.

Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.n, m, p:nat
n <= m -> p * n <= p * m
Proof.n, m, p:nat
n <= m -> p * n <= p * m
 apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *)
Qed.
Hint Resolve mult_le_compat_l: arith.

Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p.n, m, p:nat
n <= m -> n * p <= m * p
Proof.n, m, p:nat
n <= m -> n * p <= m * p
 apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l.
Qed.

Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q.n, m, p, q:nat
n <= m -> p <= q -> n * p <= m * q
Proof.n, m, p, q:nat
n <= m -> p <= q -> n * p <= m * q
  intros.n, m, p, q:nat
H:n <= m
H0:p <= q
n * p <= m * q apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l.
Qed.

Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p.n, m, p:nat
m < p -> S n * m < S n * p
Proof.n, m, p:nat
m < p -> S n * m < S n * p
  apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ.
Qed.

Hint Resolve mult_S_lt_compat_l: arith.

Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m.n, m, p:nat
n < m -> 0 < p -> p * n < p * m
Proof.n, m, p:nat
n < m -> 0 < p -> p * n < p * m
 intros.n, m, p:nat
H:n < m
H0:0 < p
p * n < p * m now apply Nat.mul_lt_mono_pos_l.
Qed.

Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p.n, m, p:nat
n < m -> 0 < p -> n * p < m * p
Proof.n, m, p:nat
n < m -> 0 < p -> n * p < m * p
 intros.n, m, p:nat
H:n < m
H0:0 < p
n * p < m * p now apply Nat.mul_lt_mono_pos_r.
Qed.

Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p.n, m, p:nat
S n * m <= S n * p -> m <= p
Proof.n, m, p:nat
S n * m <= S n * p -> m <= p
 apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ.
Qed.

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

Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q.p, q:nat
2 * p + 1 <> 2 * q
Proof.p, q:nat
2 * p + 1 <> 2 * q
 intro.p, q:nat
H:2 * p + 1 = 2 * q
False apply (Nat.Even_Odd_False (2*q)).p, q:nat
H:2 * p + 1 = 2 * q
Nat.Even (2 * q)
p, q:nat
H:2 * p + 1 = 2 * q
Nat.Odd (2 * q)
 -p, q:nat
H:2 * p + 1 = 2 * q
Nat.Even (2 * q) now exists q.
 -p, q:nat
H:2 * p + 1 = 2 * q
Nat.Odd (2 * q) now exists p.
Qed.

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.forall n m p : nat, m + n * p = mult_acc m p n
Proof.forall n m p : nat, m + n * p = mult_acc m p n
  induction n as [| n IHn]; simpl; auto.n:nat
IHn:forall m p : nat, m + n * p = mult_acc m p n
forall m p : nat,
m + (p + n * p) = mult_acc (tail_plus p m) p n
  intros.n:nat
IHn:forall m0 p0 : nat, m0 + n * p0 = mult_acc m0 p0 n
m, p:nat
m + (p + n * p) = mult_acc (tail_plus p m) p n rewrite Nat.add_assoc, IHn.n:nat
IHn:forall m0 p0 : nat, m0 + n * p0 = mult_acc m0 p0 n
m, p:nat
mult_acc (m + p) p n = mult_acc (tail_plus p m) p n f_equal.n:nat
IHn:forall m0 p0 : nat, m0 + n * p0 = mult_acc m0 p0 n
m, p:nat
m + p = tail_plus p m
  rewrite Nat.add_comm.n:nat
IHn:forall m0 p0 : nat, m0 + n * p0 = mult_acc m0 p0 n
m, p:nat
p + m = tail_plus p m apply plus_tail_plus.
Qed.

Definition tail_mult n m := mult_acc 0 m n.

Lemma mult_tail_mult : forall n m, n * m = tail_mult n m.forall n m : nat, n * m = tail_mult n m
Proof.forall n m : nat, n * m = tail_mult n m
  intros; unfold tail_mult; rewrite <- mult_acc_aux; auto.
Qed.

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.