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
.
nat
is a semi-ring
Zero property
Notation
mult_0_l
:=
Nat.mul_0_l
(
only
parsing
).
Notation
mult_0_r
:=
Nat.mul_0_r
(
only
parsing
).
1 is neutral
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
.
Commutativity
Notation
mult_comm
:=
Nat.mul_comm
(
only
parsing
).
Hint Resolve
mult_comm
:
arith
.
Distributivity
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
.
Associativity
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
.
Inversion lemmas
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.
Multiplication and successor
Notation
mult_succ_l
:=
Nat.mul_succ_l
(
only
parsing
).
Notation
mult_succ_r
:=
Nat.mul_succ_r
(
only
parsing
).
Compatibility with orders
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
.
n|->2*n and n|->2n+1 have disjoint image
Theorem
odd_even_lem
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
.