Module z_extra

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.

Module z_extra_props