Library Coq.omega.OmegaLemmas
Require
Import
BinInt
Znat
.
Local Open
Scope
Z_scope
.
Factorization lemmas
Theorem
Zred_factor0
n
:
n
=
n
*
1.
Theorem
Zred_factor1
n
:
n
+
n
=
n
*
2.
Theorem
Zred_factor2
n
m
:
n
+
n
*
m
=
n
*
(
1
+
m
)
.
Theorem
Zred_factor3
n
m
:
n
*
m
+
n
=
n
*
(
1
+
m
)
.
Theorem
Zred_factor4
n
m
p
:
n
*
m
+
n
*
p
=
n
*
(
m
+
p
)
.
Theorem
Zred_factor5
n
m
:
n
*
0
+
m
=
m
.
Theorem
Zred_factor6
n
:
n
=
n
+
0.
Other specific variants of theorems dedicated for the Omega tactic
Lemma
new_var
:
forall
x
:
Z
,
exists
y
:
Z
,
x
=
y
.
Lemma
OMEGA1
x
y
:
x
=
y
->
0
<=
x
->
0
<=
y
.
Lemma
OMEGA2
x
y
: 0
<=
x
->
0
<=
y
->
0
<=
x
+
y
.
Lemma
OMEGA3
x
y
k
:
k
>
0
->
x
=
y
*
k
->
x
=
0
->
y
=
0.
Lemma
OMEGA4
x
y
z
:
x
>
0
->
y
>
x
->
z
*
y
+
x
<>
0.
Lemma
OMEGA5
x
y
z
:
x
=
0
->
y
=
0
->
x
+
y
*
z
=
0.
Lemma
OMEGA6
x
y
z
: 0
<=
x
->
y
=
0
->
0
<=
x
+
y
*
z
.
Lemma
OMEGA7
x
y
z
t
:
z
>
0
->
t
>
0
->
0
<=
x
->
0
<=
y
->
0
<=
x
*
z
+
y
*
t
.
Lemma
OMEGA8
x
y
: 0
<=
x
->
0
<=
y
->
x
=
-
y
->
x
=
0.
Lemma
OMEGA9
x
y
z
t
:
y
=
0
->
x
=
z
->
y
+
(
-
x
+
z
)
*
t
=
0.
Lemma
OMEGA10
v
c1
c2
l1
l2
k1
k2
:
(
v
*
c1
+
l1
)
*
k1
+
(
v
*
c2
+
l2
)
*
k2
=
v
*
(
c1
*
k1
+
c2
*
k2
)
+
(
l1
*
k1
+
l2
*
k2
)
.
Lemma
OMEGA11
v1
c1
l1
l2
k1
:
(
v1
*
c1
+
l1
)
*
k1
+
l2
=
v1
*
(
c1
*
k1
)
+
(
l1
*
k1
+
l2
)
.
Lemma
OMEGA12
v2
c2
l1
l2
k2
:
l1
+
(
v2
*
c2
+
l2
)
*
k2
=
v2
*
(
c2
*
k2
)
+
(
l1
+
l2
*
k2
)
.
Lemma
OMEGA13
(
v
l1
l2
:
Z
) (
x
:
positive
) :
v
*
Zpos
x
+
l1
+
(
v
*
Zneg
x
+
l2
)
=
l1
+
l2
.
Lemma
OMEGA14
(
v
l1
l2
:
Z
) (
x
:
positive
) :
v
*
Zneg
x
+
l1
+
(
v
*
Zpos
x
+
l2
)
=
l1
+
l2
.
Lemma
OMEGA15
v
c1
c2
l1
l2
k2
:
v
*
c1
+
l1
+
(
v
*
c2
+
l2
)
*
k2
=
v
*
(
c1
+
c2
*
k2
)
+
(
l1
+
l2
*
k2
)
.
Lemma
OMEGA16
v
c
l
k
:
(
v
*
c
+
l
)
*
k
=
v
*
(
c
*
k
)
+
l
*
k
.
Lemma
OMEGA17
x
y
z
:
Zne
x
0
->
y
=
0
->
Zne
(
x
+
y
*
z
) 0.
Lemma
OMEGA18
x
y
k
:
x
=
y
*
k
->
Zne
x
0
->
Zne
y
0.
Lemma
OMEGA19
x
:
Zne
x
0
->
0
<=
x
+
-1
\/
0
<=
x
*
-1
+
-1.
Lemma
OMEGA20
x
y
z
:
Zne
x
0
->
y
=
0
->
Zne
(
x
+
y
*
z
) 0.
Definition
fast_Zplus_comm
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
y
+
x
)) :=
eq_ind_r
P
H
(
Z.add_comm
x
y
).
Definition
fast_Zplus_assoc_reverse
(
n
m
p
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
n
+
(
m
+
p
)
)) :=
eq_ind_r
P
H
(
Zplus_assoc_reverse
n
m
p
).
Definition
fast_Zplus_assoc
(
n
m
p
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
n
+
m
+
p
)) :=
eq_ind_r
P
H
(
Z.add_assoc
n
m
p
).
Definition
fast_Zplus_permute
(
n
m
p
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
m
+
(
n
+
p
)
)) :=
eq_ind_r
P
H
(
Z.add_shuffle3
n
m
p
).
Definition
fast_OMEGA10
(
v
c1
c2
l1
l2
k1
k2
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
v
*
(
c1
*
k1
+
c2
*
k2
)
+
(
l1
*
k1
+
l2
*
k2
)
)) :=
eq_ind_r
P
H
(
OMEGA10
v
c1
c2
l1
l2
k1
k2
).
Definition
fast_OMEGA11
(
v1
c1
l1
l2
k1
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
v1
*
(
c1
*
k1
)
+
(
l1
*
k1
+
l2
)
)) :=
eq_ind_r
P
H
(
OMEGA11
v1
c1
l1
l2
k1
).
Definition
fast_OMEGA12
(
v2
c2
l1
l2
k2
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
v2
*
(
c2
*
k2
)
+
(
l1
+
l2
*
k2
)
)) :=
eq_ind_r
P
H
(
OMEGA12
v2
c2
l1
l2
k2
).
Definition
fast_OMEGA15
(
v
c1
c2
l1
l2
k2
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
v
*
(
c1
+
c2
*
k2
)
+
(
l1
+
l2
*
k2
)
)) :=
eq_ind_r
P
H
(
OMEGA15
v
c1
c2
l1
l2
k2
).
Definition
fast_OMEGA16
(
v
c
l
k
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
v
*
(
c
*
k
)
+
l
*
k
)) :=
eq_ind_r
P
H
(
OMEGA16
v
c
l
k
).
Definition
fast_OMEGA13
(
v
l1
l2
:
Z
) (
x
:
positive
) (
P
:
Z
->
Prop
)
(
H
:
P
(
l1
+
l2
)) :=
eq_ind_r
P
H
(
OMEGA13
v
l1
l2
x
).
Definition
fast_OMEGA14
(
v
l1
l2
:
Z
) (
x
:
positive
) (
P
:
Z
->
Prop
)
(
H
:
P
(
l1
+
l2
)) :=
eq_ind_r
P
H
(
OMEGA14
v
l1
l2
x
).
Definition
fast_Zred_factor0
(
x
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
1)) :=
eq_ind_r
P
H
(
Zred_factor0
x
).
Definition
fast_Zopp_eq_mult_neg_1
(
x
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
-1)) :=
eq_ind_r
P
H
(
Z.opp_eq_mul_m1
x
).
Definition
fast_Zmult_comm
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
y
*
x
)) :=
eq_ind_r
P
H
(
Z.mul_comm
x
y
).
Definition
fast_Zopp_plus_distr
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
-
x
+
-
y
)) :=
eq_ind_r
P
H
(
Z.opp_add_distr
x
y
).
Definition
fast_Zopp_mult_distr_r
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
-
y
)) :=
eq_ind_r
P
H
(
Zopp_mult_distr_r
x
y
).
Definition
fast_Zmult_plus_distr_l
(
n
m
p
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
n
*
p
+
m
*
p
)) :=
eq_ind_r
P
H
(
Z.mul_add_distr_r
n
m
p
).
Definition
fast_Zmult_assoc_reverse
(
n
m
p
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
n
*
(
m
*
p
)
)) :=
eq_ind_r
P
H
(
Zmult_assoc_reverse
n
m
p
).
Definition
fast_Zred_factor1
(
x
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
2)) :=
eq_ind_r
P
H
(
Zred_factor1
x
).
Definition
fast_Zred_factor2
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
(
1
+
y
)
)) :=
eq_ind_r
P
H
(
Zred_factor2
x
y
).
Definition
fast_Zred_factor3
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
(
1
+
y
)
)) :=
eq_ind_r
P
H
(
Zred_factor3
x
y
).
Definition
fast_Zred_factor4
(
x
y
z
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
*
(
y
+
z
)
)) :=
eq_ind_r
P
H
(
Zred_factor4
x
y
z
).
Definition
fast_Zred_factor5
(
x
y
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
y
) :=
eq_ind_r
P
H
(
Zred_factor5
x
y
).
Definition
fast_Zred_factor6
(
x
:
Z
) (
P
:
Z
->
Prop
)
(
H
:
P
(
x
+
0)) :=
eq_ind_r
P
H
(
Zred_factor6
x
).
Theorem
intro_Z
:
forall
n
:
nat
,
exists
y
:
Z
,
Z.of_nat
n
=
y
/\
0
<=
y
*
1
+
0.