Properties about integers, imported from CompCertSSA.
Require Export ZArith.
Open Scope Z_scope.
Lemma Zmult_bounds1 :
forall x1 x2 y1 y2 :
Z,
0 <=
x1 <=
x2 ->
0 <=
y1 <=
y2 ->
x1 *
y1 <=
x2 *
y2.
Proof.
intros; apply Zmult_le_compat; omega.
Qed.
Lemma Zmult_opp :
forall x y :
Z,
x*
y=(-
x)*(-
y).
Proof.
intros; ring.
Qed.
Lemma Zmult_bounds2 :
forall x1 x2 y1 y2 :
Z,
x1 <=
x2 <= 0->
y1 <=
y2 <= 0 ->
x2 *
y2 <=
x1 *
y1.
Proof.
intuition.
rewrite (Zmult_opp x2); rewrite (Zmult_opp x1).
apply Zmult_bounds1; omega.
Qed.
Lemma Zmult_interval_right_right :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
0 <=
a -> 0 <=
c ->
a*
c <=
x*
y <=
b*
d.
Proof.
intuition.
apply Zmult_bounds1; split; try omega.
apply Zmult_bounds1; split; try omega.
Qed.
Lemma Zmult_ineq1 :
forall a b c d,
c*(-
d) <=
a*(-
b) ->
a*
b <=
c*
d.
Proof.
intuition.
replace (c*d) with (-(c*-d)).
replace (a*b) with (-(a*-b)).
omega.
ring.
ring.
Qed.
Lemma Zmult_ineq2 :
forall a b c d,
(-
c)*
d <= (-
a)*
b ->
a*
b <=
c*
d.
Proof.
intuition.
replace (c*d) with (-(-c*d)).
replace (a*b) with (-(-a*b)).
omega.
ring.
ring.
Qed.
Lemma Zmult_split :
forall a b c d,
a*
b <= 0 -> 0 <=
c*
d ->
a*
b <=
c*
d.
Proof.
intros; apply Zle_trans with 0; auto.
Qed.
Hint Resolve Zmult_split Zmult_ineq1.
Lemma sign_rule1 :
forall x y :
Z,
x >= 0 ->
y <= 0 ->
x *
y <= 0.
Proof.
intros.
replace 0 with (x*0)%Z; auto with zarith.
Qed.
Lemma sign_rule2 :
forall x y :
Z,
x >= 0 ->
y >= 0 -> 0 <=
x *
y.
Proof.
intros.
replace 0 with (x*0)%Z; auto with zarith.
Qed.
Lemma sign_rule3 :
forall x y :
Z,
x <= 0 ->
y <= 0 -> 0 <=
x *
y.
Proof.
intros.
rewrite (Zmult_opp x).
apply sign_rule2; omega.
Qed.
Lemma sign_rule4 :
forall x y :
Z,
x <= 0 ->
y >= 0 ->
x *
y <= 0.
Proof.
intros.
rewrite Zmult_comm.
apply sign_rule1; auto.
Qed.
Hint Resolve sign_rule1 sign_rule2 sign_rule3 sign_rule4 :
sign.
Lemma Zpos_or_not :
forall x :
Z, {
x>=0}+{
x<0}.
Proof.
intros x; destruct (Z_le_dec 0 x); auto.
left; omega.
right; omega.
Qed.
Lemma Zpos_strict_or_not :
forall x :
Z, {
x>0}+{
x<=0}.
Proof.
intros x; destruct (Z_lt_dec 0 x).
left; omega.
right; omega.
Qed.
Hint Resolve Zmult_bounds1 Zmult_ineq1.
Lemma Zmult_interval_right_mid :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
0 <=
a ->
c < 0 -> 0 <=
d ->
b*
c <=
x*
y <=
b*
d.
Proof.
intuition;
(assert (b>=0); [omega|idtac]);
(assert (x>=0); [omega|idtac]);
destruct (Zpos_or_not y); auto with sign zarith.
Qed.
Hint Resolve Zmult_bounds2 Zmult_ineq2.
Lemma Zmult_interval_left_mid :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
b < 0 ->
c < 0 -> 0 <=
d ->
a*
d <=
x*
y <=
a*
c.
Proof.
intuition;
(assert (a<0); [omega|idtac]);
(assert (x<0); [omega|idtac]);
destruct (Zpos_or_not y); auto with sign zarith.
Qed.
Lemma Zmult_interval_right_left :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
0 <=
a ->
d < 0 ->
b*
c <=
x*
y <=
a*
d.
Proof.
intuition; auto with zarith.
Qed.
Lemma Zmult_interval_left_left :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
b < 0 ->
d < 0 ->
b*
d <=
x*
y <=
a*
c.
Proof.
intuition; auto with zarith.
Qed.
Lemma case_Zmax :
forall (
P:
Z->
Type)
x y,
(
y<=
x ->
P x) -> (
x<=
y ->
P y )->
P (
Zmax x y).
Proof.
unfold Zmax, Zle; intros.
case_eq (x ?= y); intros.
apply X; rewrite <- Zcompare_antisym.
rewrite H; discriminate.
apply X0; rewrite H; discriminate.
apply X; rewrite <- Zcompare_antisym.
rewrite H; discriminate.
Qed.
Lemma Z_max_le_r :
forall x y :
Z,
y <= (
Zmax x y).
Proof.
intros; apply Zmax2.
Qed.
Lemma Z_max_le_l :
forall x y :
Z,
x <= (
Zmax x y).
Proof.
intros; apply Zmax1.
Qed.
Lemma case_Zmin :
forall (
P:
Z->
Type)
x y,
(
x<=
y ->
P x) -> (
y<=
x ->
P y )->
P (
Zmin x y).
Proof.
unfold Zmin, Zle; intros P x y.
generalize (Zcompare_antisym x y).
destruct (x ?= y); intros.
apply X; discriminate.
apply X; discriminate.
apply X0.
rewrite <- H; discriminate.
Qed.
Lemma Zmin_comm :
forall n m,
Zmin n m =
Zmin m n.
Proof.
intros; repeat (apply case_Zmin; intros); omega.
Qed.
Lemma Zmin_glb :
forall n m p,
p <=
n ->
p <=
m ->
p <=
Zmin n m.
Proof.
intros; repeat (apply case_Zmin; intros); omega.
Qed.
Hint Resolve Zle_min_l Zle_min_r Z_max_le_l Z_max_le_r.
Lemma Zmult_interval_mid_mid :
forall a b c d x y,
a <=
x <=
b ->
c <=
y <=
d ->
a < 0 -> 0 <=
b ->
c < 0 -> 0 <=
d ->
Zmin (
b*
c) (
a*
d) <=
x*
y <=
Zmax (
a*
c) (
b*
d).
Proof.
intuition.
apply case_Zmin; intros.
destruct (Zpos_or_not y).
destruct (Zpos_or_not x).
apply Zmult_split; auto with zarith sign.
apply Zle_trans with (a*d); auto.
apply Zmult_ineq2; apply Zmult_bounds1; intuition.
destruct (Zpos_or_not x).
apply Zmult_ineq1; apply Zmult_bounds1; intuition.
apply Zmult_split; auto with zarith sign.
destruct (Zpos_or_not y); destruct (Zpos_or_not x).
apply Zmult_split; auto with zarith sign.
apply Zmult_ineq2; apply Zmult_bounds1; intuition.
apply Zle_trans with (b*c); auto.
apply Zmult_ineq1; apply Zmult_bounds1; intuition.
apply Zmult_split; auto with zarith sign.
apply case_Zmax; intros.
destruct (Zpos_or_not y); destruct (Zpos_or_not x).
apply Zle_trans with (b*d); auto.
apply Zmult_bounds1; intuition.
apply Zmult_split; auto with zarith sign.
apply Zmult_split; auto with zarith sign.
apply Zmult_ineq2; apply Zmult_ineq1; intuition.
destruct (Zpos_or_not y); destruct (Zpos_or_not x).
apply Zmult_bounds1; intuition.
apply Zmult_split; auto with zarith sign.
apply Zmult_split; auto with zarith sign.
apply Zle_trans with (a*c); auto.
apply Zmult_ineq2; apply Zmult_ineq1; intuition.
Qed.
Lemma ineq_trans :
forall a b c d e :
Z,
a <=
b ->
c <=
d ->
b <=
e <=
c ->
a <=
e <=
d.
Proof.
intuition; omega.
Qed.
Lemma Z_min4_le_1 :
forall x y z t:
Z,
Zmin (
Zmin x y) (
Zmin z t) <=
x.
Proof.
intros.
apply Zle_trans with (Zmin x y); auto.
Qed.
Lemma Z_min4_le_2 :
forall x y z t:
Z,
Zmin (
Zmin x y) (
Zmin z t) <=
y.
Proof.
intros.
apply Zle_trans with (Zmin x y); auto.
Qed.
Lemma Z_min4_le_3 :
forall x y z t:
Z,
Zmin (
Zmin x y) (
Zmin z t) <=
z.
Proof.
intros.
apply Zle_trans with (Zmin z t); auto.
Qed.
Lemma Z_min4_le_4 :
forall x y z t:
Z,
Zmin (
Zmin x y) (
Zmin z t) <=
t.
Proof.
intros.
apply Zle_trans with (Zmin z t); auto.
Qed.
Lemma Z_max4_le_1 :
forall x y z t:
Z,
x <=
Zmax (
Zmax x y) (
Zmax z t).
Proof.
intros.
apply Zle_trans with (Zmax x y); auto.
Qed.
Lemma Z_max4_le_2 :
forall x y z t:
Z,
y <=
Zmax (
Zmax x y) (
Zmax z t).
Proof.
intros.
apply Zle_trans with (Zmax x y); auto.
Qed.
Lemma Z_max4_le_3 :
forall x y z t:
Z,
z <=
Zmax (
Zmax x y) (
Zmax z t).
Proof.
intros.
apply Zle_trans with (Zmax z t); auto.
Qed.
Lemma Z_max4_le_4 :
forall x y z t:
Z,
t <=
Zmax (
Zmax x y) (
Zmax z t).
Proof.
intros.
apply Zle_trans with (Zmax z t); auto.
Qed.
Hint Resolve Z_max4_le_1 Z_max4_le_2 Z_max4_le_3 Z_max4_le_4
Z_min4_le_1 Z_min4_le_2 Z_min4_le_3 Z_min4_le_4.
Lemma Mult_interval_correct_min_max :
forall a b c d x y :
Z,
a <=
x <=
b ->
c <=
y <=
d ->
Zmin (
Zmin (
a*
c) (
b*
d)) (
Zmin (
b*
c) (
a*
d)) <=
x *
y
<=
Zmax (
Zmax (
a*
c) (
b*
d)) (
Zmax (
b*
c) (
a*
d)).
Proof.
intros.
destruct (Zpos_or_not a).
destruct (Zpos_or_not c).
apply ineq_trans with (a*c) (b*d); auto.
apply Zmult_interval_right_right; auto with zarith.
destruct (Zpos_or_not d).
apply ineq_trans with (b*c) (b*d); auto.
apply Zmult_interval_right_mid with a; auto with zarith.
apply ineq_trans with (b*c) (a*d); auto.
apply Zmult_interval_right_left; auto with zarith.
destruct (Zpos_or_not b); destruct (Zpos_or_not c).
apply ineq_trans with (a*d) (b*d); auto.
rewrite (Zmult_comm a d); rewrite (Zmult_comm x y); rewrite (Zmult_comm b d).
apply Zmult_interval_right_mid with c; auto with zarith.
destruct (Zpos_or_not d).
apply ineq_trans with (Zmin (b*c) (a*d)) (Zmax (a*c) (b*d)); auto.
apply Zmult_interval_mid_mid; auto with zarith.
apply ineq_trans with (b*c) (a*c); auto.
rewrite (Zmult_comm a c); rewrite (Zmult_comm x y); rewrite (Zmult_comm b c).
apply Zmult_interval_left_mid with d; auto with zarith.
apply ineq_trans with (a*d) (b*c); auto.
rewrite (Zmult_comm b c); rewrite (Zmult_comm x y); rewrite (Zmult_comm a d).
apply Zmult_interval_right_left; auto with zarith.
destruct (Zpos_or_not d).
apply ineq_trans with (a*d) (a*c); auto.
apply Zmult_interval_left_mid with b; auto with zarith.
apply ineq_trans with (b*d) (a*c); auto.
apply Zmult_interval_left_left; auto with zarith.
Qed.