Library Coq.omega.OmegaLemmas
Factorization lemmas
Other specific variants of theorems dedicated for the Omega tactic
Lemma new_var :
forall x :
Z,
exists y : Z, x = y.
Lemma OMEGA1 :
forall x y :
Z,
x = y -> 0
<= x -> 0
<= y.
Lemma OMEGA2 :
forall x y :
Z, 0
<= x -> 0
<= y -> 0
<= x + y.
Lemma OMEGA3 :
forall x y k :
Z,
k > 0 ->
x = y * k ->
x = 0 ->
y = 0.
Lemma OMEGA4 :
forall x y z :
Z,
x > 0 ->
y > x ->
z * y + x <> 0.
Lemma OMEGA5 :
forall x y z :
Z,
x = 0 ->
y = 0 ->
x + y * z = 0.
Lemma OMEGA6 :
forall x y z :
Z, 0
<= x ->
y = 0 -> 0
<= x + y * z.
Lemma OMEGA7 :
forall x y z t :
Z,
z > 0 ->
t > 0 -> 0
<= x -> 0
<= y -> 0
<= x * z + y * t.
Lemma OMEGA8 :
forall x y :
Z, 0
<= x -> 0
<= y ->
x = - y ->
x = 0.
Lemma OMEGA9 :
forall x y z t :
Z,
y = 0 ->
x = z ->
y + (- x + z) * t = 0.
Lemma OMEGA10 :
forall v c1 c2 l1 l2 k1 k2 :
Z,
(v * c1 + l1) * k1 + (v * c2 + l2) * k2 =
v * (c1 * k1 + c2 * k2) + (l1 * k1 + l2 * k2).
Lemma OMEGA11 :
forall v1 c1 l1 l2 k1 :
Z,
(v1 * c1 + l1) * k1 + l2 = v1 * (c1 * k1) + (l1 * k1 + l2).
Lemma OMEGA12 :
forall v2 c2 l1 l2 k2 :
Z,
l1 + (v2 * c2 + l2) * k2 = v2 * (c2 * k2) + (l1 + l2 * k2).
Lemma OMEGA13 :
forall (
v l1 l2 :
Z) (
x :
positive),
v * Zpos x + l1 + (v * Zneg x + l2) = l1 + l2.
Lemma OMEGA14 :
forall (
v l1 l2 :
Z) (
x :
positive),
v * Zneg x + l1 + (v * Zpos x + l2) = l1 + l2.
Lemma OMEGA15 :
forall v c1 c2 l1 l2 k2 :
Z,
v * c1 + l1 + (v * c2 + l2) * k2 = v * (c1 + c2 * k2) + (l1 + l2 * k2).
Lemma OMEGA16 :
forall v c l k :
Z,
(v * c + l) * k = v * (c * k) + l * k.
Lemma OMEGA17 :
forall x y z :
Z,
Zne x 0 ->
y = 0 ->
Zne (
x + y * z) 0.
Lemma OMEGA18 :
forall x y k :
Z,
x = y * k ->
Zne x 0 ->
Zne y 0.
Lemma OMEGA19 :
forall x :
Z,
Zne x 0 -> 0
<= x + -1
\/ 0
<= x * -1
+ -1.
Lemma OMEGA20 :
forall x y z :
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 (
Zplus_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 (
Zplus_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 (
Zplus_permute 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 (
Zopp_eq_mult_neg_1 x).
Definition fast_Zmult_comm (
x y :
Z) (
P :
Z ->
Prop)
(
H :
P (
y * x)) :=
eq_ind_r P H (
Zmult_comm x y).
Definition fast_Zopp_plus_distr (
x y :
Z) (
P :
Z ->
Prop)
(
H :
P (
- x + - y)) :=
eq_ind_r P H (
Zopp_plus_distr x y).
Definition fast_Zopp_involutive (
x :
Z) (
P :
Z ->
Prop) (
H :
P x) :=
eq_ind_r P H (
Zopp_involutive x).
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 (
Zmult_plus_distr_l n m p).
Definition fast_Zmult_opp_comm (
x y :
Z) (
P :
Z ->
Prop)
(
H :
P (
x * - y)) :=
eq_ind_r P H (
Zmult_opp_comm x y).
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).