Module DLib

Utility definitions by David.

Require Import Utf8.
Require Import Classical.
Require Import Coqlib.
Require Import Maps.

Tactic Notation ">" tactic(t) := t.
Tactic Notation "by" tactic(t) := t; fail "this goal should be proved at this point".

Ltac destruct_bool_in_goal :=
  match goal with [ |- context[if ?x then _ else _]] => destruct x end.
Ltac destruct_option_in_goal :=
  match goal with [ |- context[match ?x with Some _ => _ | None => _ end]] => destruct x end.
Ltac case_eq_bool_in_goal :=
  match goal with [ |- context[if ?x then _ else _]] => case_eq x end.
Ltac case_eq_option_in_goal :=
  match goal with [ |- context[match ?x with Some _ => _ | None => _ end]] => case_eq x end.
Ltac destruct_bool :=
  match goal with
    [ _ : context[if ?x then _ else _] |- _] => destruct x
  | [ |- context[if ?x then _ else _]] => destruct x
  end.
Ltac destruct_option :=
  match goal with
    [ _ : context[match ?x with Some _ => _ | None => _ end] |- _] => destruct x
  | [ |- context[match ?x with Some _ => _ | None => _ end]] => destruct x
  end.

Ltac simpl_option :=
  match goal with
    [ id : Some _ = Some _ |- _ ] => inv id
  | [ id : None = Some _ |- _ ] => inv id
  | [ id : Some _ = None |- _ ] => inv id
  end.

Ltac invh f :=
    match goal with
      [ id: f |- _ ] => inv id
    | [ id: f _ |- _ ] => inv id
    | [ id: f _ _ |- _ ] => inv id
    | [ id: f _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    | [ id: f _ _ _ _ _ _ _ _ _ _ _ _ _ _ |- _ ] => inv id
    end.

Ltac bif :=
  match goal with |- context[if ?a then _ else _] => destruct a end; try congruence.

Ltac pairs :=
  repeat
  match goal with
    | |- context[let '(_,_) := ?x in _] =>
      case_eq x; intros ? ?
  end.

Ltac autorw :=
  match goal with
    | [H: _ = _ |- _] => rewrite H in *
  end.

Ltac autorw' := repeat (progress (autorw; subst)).

Ltac inj :=
  repeat
  match goal with
    | [H : ?f _ = ?f _ |- _] => injection H; intros ?; subst; clear H
    | [H : ?f _ _ = ?f _ _ |- _] => injection H; intros ? ?; subst; clear H
  end.
Definition ptree_forall {A:Type} (m:PTree.t A) (f:positive->A->bool) : bool :=
  PTree.fold (fun b0 p a => b0 && f p a) m true.

Lemma ptree_forall_correct1 : forall A (f:positive->A->bool) m,
  ptree_forall m f = true ->
  forall n ins, m!n = Some ins -> f n ins = true.

Proof.

  intros A f m; unfold ptree_forall.
  apply PTree_Properties.fold_rec
    with (P:=fun m b => b = true -> forall n ins, m!n = Some ins -> f n ins = true); intros.
  apply H0; auto.
  rewrite H; auto.
  rewrite PTree.gempty in H0; congruence.
  rewrite PTree.gsspec in H3; destruct peq.
  inv H3.
  elim andb_prop with (1:=H2); auto.
  elim andb_prop with (1:=H2); auto.
Qed.

Lemma ptree_forall_correct2 : forall A (f:positive->A->bool) m,
(forall n ins, m!n = Some ins -> f n ins = true) ->
ptree_forall m f = true.

Proof.

  intros A f m; unfold ptree_forall.
  apply PTree_Properties.fold_rec
    with (P:=fun m b => (forall n ins, m!n = Some ins -> f n ins = true) -> b = true ); intros; auto.
  apply H0; auto.
  intros n ins; rewrite H; auto.
  rewrite H1; simpl.
  apply H2.
  rewrite PTree.gss; auto.
  intros; apply H2.
  rewrite PTree.gsspec; destruct peq; auto; congruence.
Qed.

Lemma ptree_forall_correct : forall A (f:positive->A->bool) m,
ptree_forall m f = true <->
(forall n ins, m!n = Some ins -> f n ins = true).

Proof.

split; eauto using ptree_forall_correct1, ptree_forall_correct2.
Qed.

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 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.

Hint Resolve Zle_min_l Zle_min_r Z_max_le_l Z_max_le_r.

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.

Require Import Integers.

  Lemma repr_mod_prop: forall x y,
    Int.repr (x + y * Int.modulus) = Int.repr x.

Proof.

    unfold Int.repr; intros.
    apply Int.mkint_eq.
    apply Z_mod_plus_full.
  Qed.

Lemma Z_of_nat_gt: forall n, (n > 0)%nat -> Z_of_nat n > 0.

Proof.

    intros.
    apply (inj_gt n 0).
    auto.
  Qed.

  Lemma sign_ext_same : forall n m i,
    (m > 0)%nat ->
    Int.wordsize = ((S n)+m)%nat ->
    -(two_power_nat n) <= Int.signed i <= (two_power_nat n) -1 ->
    Int.sign_ext (Z_of_nat (S n)) i = i.

Proof.

    intros.
    rewrite <- Int.repr_signed.
    rewrite <- (Int.repr_signed (Int.sign_ext (Z_of_nat (S n)) i)).
    rewrite Int.sign_ext_div.
    assert (Z_of_nat Int.wordsize = Z_of_nat (S n) + Z_of_nat m).
    rewrite <- inj_plus; congruence.
    replace (Z_of_nat Int.wordsize - Z_of_nat (S n)) with (Z_of_nat m) by omega.
    unfold Int.signed in * |- ; destruct zlt.
    rewrite Int.signed_repr.
    rewrite Z_div_mult.
    rewrite Int.repr_unsigned.
    rewrite Int.repr_signed.
    auto.
    auto with zarith.
    assert (two_p (Z_of_nat m) > 0) by auto with zarith.
    generalize (Int.unsigned_range i); intros.
    split.
    unfold Int.min_signed.
    generalize Int.half_modulus_pos; intros.
    generalize (Zmult_le_compat_r 0 (Int.unsigned i) (two_p (Z_of_nat m))); intros.
    omega.
    rewrite two_power_nat_two_p in *.
    unfold Int.max_signed, Int.half_modulus.
    cut (Int.unsigned i * two_p (Z_of_nat m) < Int.modulus / 2).
    omega.
    apply Zlt_le_trans with (two_p (Z_of_nat n) * two_p (Z_of_nat m)).
    apply Zmult_lt_compat_r; omega.
    unfold Int.modulus.
    rewrite two_power_nat_two_p in *.
    rewrite <- two_p_is_exp.
    unfold Int.wordsize, Wordsize_32.wordsize in *.
    rewrite inj_S.
    rewrite two_p_S.
    rewrite Zmult_comm.
    rewrite Z_div_mult.
    assert (n+m=31)%nat by omega.
    rewrite <- inj_plus.
    rewrite H5; omega.
    omega.
    auto with zarith.
    auto with zarith.
    auto with zarith.
    rewrite <- (repr_mod_prop (Int.unsigned i * two_p (Z_of_nat m)) (-two_p (Z_of_nat m))).
    rewrite Int.signed_repr.
    replace (Int.unsigned i * two_p (Z_of_nat m) + - two_p (Z_of_nat m) * Int.modulus)
      with ((Int.unsigned i + (-1)* Int.modulus)* two_p (Z_of_nat m) ) by ring.
    rewrite Z_div_mult.
    rewrite (repr_mod_prop (Int.unsigned i) (-1)).
    rewrite Int.repr_unsigned.
    rewrite Int.repr_signed.
    auto.
    auto with zarith.
    assert (two_p (Z_of_nat m) > 0) by auto with zarith.
    replace Int.min_signed with ((- two_power_nat n) * two_p (Z_of_nat m)).
    replace Int.max_signed with ((two_power_nat n* two_p (Z_of_nat m))-1).
    replace (Int.unsigned i * two_p (Z_of_nat m) + - two_p (Z_of_nat m) * Int.modulus)
      with ((Int.unsigned i + (-1)* Int.modulus)* two_p (Z_of_nat m) ) by ring.
    split.
    apply Zmult_le_compat_r; auto with zarith.
    cut ((Int.unsigned i + -1 * Int.modulus) * two_p (Z_of_nat m) <
      two_power_nat n * two_p (Z_of_nat m) ).
    omega.
    apply Zmult_lt_compat_r; auto with zarith.
    unfold Int.max_signed, Int.half_modulus, Int.modulus.
    unfold Int.wordsize, Wordsize_32.wordsize in *.
    repeat rewrite two_power_nat_two_p in *.
    rewrite inj_S.
    rewrite two_p_S.
    rewrite (Zmult_comm 2).
    rewrite Z_div_mult.
    rewrite <- two_p_is_exp.
    rewrite <- inj_plus.
    assert (n+m=31)%nat by omega.
    congruence.
    auto with zarith.
    auto with zarith.
    auto with zarith.
    auto with zarith.
    unfold Int.min_signed, Int.half_modulus, Int.modulus.
    unfold Int.wordsize, Wordsize_32.wordsize in *.
    repeat rewrite two_power_nat_two_p in *.
    rewrite inj_S.
    rewrite two_p_S.
    rewrite (Zmult_comm 2).
    rewrite Z_div_mult.
    replace (- two_p (Z_of_nat n) * two_p (Z_of_nat m))
      with (- (two_p (Z_of_nat n) * two_p (Z_of_nat m))) by ring.
    rewrite <- two_p_is_exp.
    rewrite <- inj_plus.
    assert (n+m=31)%nat by omega.
    congruence.
    auto with zarith.
    auto with zarith.
    auto with zarith.
    auto with zarith.
    unfold Int.wordsize, Wordsize_32.wordsize in *.
    rewrite H0.
    rewrite inj_plus.
    generalize (Z_of_nat_gt (S n)).
    generalize (Z_of_nat_gt m).
    omega.
  Qed.

  Lemma zero_ext_same : forall n m i,
    (m > 0)%nat ->
    Int.wordsize = (n+m)%nat ->
    0 <= Int.signed i <= (two_power_nat n) -1 ->
    Int.zero_ext (Z_of_nat n) i = i.

Proof.

    intros n m i MGZ SZ IIN.
    rewrite <- (Int.repr_unsigned (Int.zero_ext (Z_of_nat n) i)).
    destruct n.
    simpl in *.
    assert (IEQ: i = Int.zero).
      destruct i.
      apply Int.mkint_eq.
      rewrite Zmod_0_l.
      unfold Int.signed in IIN; simpl in IIN.
      destruct (zlt intval Int.half_modulus); omega.
    subst i.
    unfold Int.zero.
    rewrite Zmod_0_l.
    auto.
    rewrite Int.zero_ext_mod.
    rewrite <- Int.repr_unsigned.
    rewrite Zmod_small; auto.
    rewrite <- two_power_nat_two_p.
    rewrite <- Int.signed_eq_unsigned.
    omega.
    apply Int.signed_positive.
    omega.
    rewrite SZ.
    zify. omega.
  Qed.

Lemma two_power_nat_div2 : forall n,
two_power_nat (S n) / 2 = two_power_nat n.

Proof.

    unfold two_power_nat; intros; simpl.
    unfold shift_nat; simpl.
    generalize (iter_nat n positive xO 1%positive); intros.
    apply Zdiv_unique with 0; try omega.
    rewrite Zmult_comm; auto.
  Qed.

Lemma neg_signed_unsigned : forall x,
Int.repr (- (Int.signed x)) = Int.repr (- (Int.unsigned x)).

Proof.

    intros.
    unfold Int.signed; destruct zlt; auto.
    replace (- (Int.unsigned x - Int.modulus)) with
      ( - Int.unsigned x + (1) * Int.modulus) by ring.
    apply repr_mod_prop.
  Qed.

Lemma zle_and_case: forall x y z t,
zle x y && zle z t = false -> x > y \/ z > t.

Proof.

    intros x1 x2 x3 x4.
    destruct zle; simpl.
    destruct zle; simpl; try congruence.
    omega.
    omega.
  Qed.

Lemma add_signed_unsigned : forall x y,
Int.repr (Int.signed x + Int.signed y) = Int.repr (Int.unsigned x + Int.unsigned y).

Proof.

    intros.
    unfold Int.signed; do 2 destruct zlt; try reflexivity.
    replace (Int.unsigned x + (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x + Int.unsigned y) + (- 1) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus) + Int.unsigned y) with
      ((Int.unsigned x + Int.unsigned y) + (-1) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus) + (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x + Int.unsigned y) + (- 2) * Int.modulus) by ring.
    apply repr_mod_prop.
  Qed.

Lemma sub_signed_unsigned : forall x y,
Int.repr (Int.signed x - Int.signed y) = Int.repr (Int.unsigned x - Int.unsigned y).

Proof.

    intros.
    unfold Int.signed; do 2 destruct zlt; try reflexivity.
    replace (Int.unsigned x - (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x - Int.unsigned y) + (1) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus) - Int.unsigned y) with
      ((Int.unsigned x - Int.unsigned y) + (-1) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus) - (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x - Int.unsigned y)) by ring.
    auto.
  Qed.

Lemma mult_signed_unsigned : forall x y,
Int.repr (Int.signed x * Int.signed y) = Int.repr (Int.unsigned x * Int.unsigned y).

Proof.

    intros.
    unfold Int.signed; do 2 destruct zlt; try reflexivity.
    replace (Int.unsigned x * (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x * Int.unsigned y) + (- Int.unsigned x) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus) * Int.unsigned y) with
      ((Int.unsigned x * Int.unsigned y) + (- Int.unsigned y) * Int.modulus) by ring.
    apply repr_mod_prop.
    replace ((Int.unsigned x - Int.modulus)* (Int.unsigned y - Int.modulus)) with
      ((Int.unsigned x * Int.unsigned y) + (- Int.unsigned x - Int.unsigned y + Int.modulus) * Int.modulus) by ring.
    apply repr_mod_prop.
  Qed.

Lemma zle_true_iff : forall x y: Z,
proj_sumbool (zle x y) = true <-> x <= y.

Proof.

intros; destruct zle; simpl; split; auto; congruence.
Qed.

Lemma unsigned_inj i j : i ≠ j → Int.unsigned i ≠ Int.unsigned j.

Proof.

intros A B; apply A. destruct i; destruct j. simpl in B. subst. f_equal. apply Axioms.proof_irr. Qed.

Lemma signed_inj i j : i ≠ j → Int.signed i ≠ Int.signed j.

Proof.

intros A B; apply A. destruct i as [i I]; destruct j as [j J].
       unfold Int.signed in *. repeat destruct zlt; simpl in *; subst.
       f_equal; apply Axioms.proof_irr.
       cut False; intuition.
       cut False; intuition.
       assert (i = j) by omega. subst.
       f_equal; apply Axioms.proof_irr.
Qed.

Lemma signed_le_unsigned x :
Int.signed x <= Int.unsigned x.

Proof.

unfold Int.signed. bif; auto; intuition.
pose proof (Int.modulus_pos). intuition.
Qed.

Lemma signed_pos_unsigned {x} :
0 <= Int.signed x → Int.signed x = Int.unsigned x.

Proof.

  unfold Int.signed. bif.
  intros H. apply False_ind. unfold Int.half_modulus in *.
  pose proof (Int.unsigned_range x). intuition.
Qed.

Lemma mod_sub : ∀ x M, M > 0 →
M <= x < M + M - 1 →
x mod M = x - M.

Proof.

  intros q M ? ?. rewrite Zmod_eq; auto.
  replace (q / M) with (((q-M) + 1 * M) / M).
  2: f_equal; ring.
  rewrite Z_div_plus; auto.
  rewrite Zdiv_small; intuition.
Qed.

Lemma z_lt_neg_gt x y : - x < - y -> y < x.

Proof.

destruct x; destruct y; intuition. Qed.

Lemma z_le_neg_ge x y : - x <= - y -> y <= x.

Proof.

destruct x; destruct y; intuition. Qed.

Lemma zdiv_lt : ∀ x y z, z > 0 -> x < 0 <= y -> x / z < y / z.

Proof.

  intros x y z H [X Y].
  apply Zlt_le_trans with 0. 2: intuition auto using Z_div_pos.
  apply z_lt_neg_gt. simpl.
  case (zeq (x mod z) 0); intros M.
  pose proof (Z_div_mod_eq x _ H) as U. rewrite M in U.
  set (q := x / z). fold q in U. clear M.
  destruct q. rewrite U in X. omega.
  simpl. assert (x>0). subst.
  destruct z; intuition. intuition.
  simpl. zify. intuition.
  cut (0 <= - (x / z) - 1). intuition.
  rewrite <- Z_div_nz_opp_full; auto. apply Z_div_pos; intuition.
Qed.

Lemma zdiv_mono : ∀ x z : Z, x < -1 → z > 0 → x <= x / z.

Proof.

  intros x z X Z.
  apply z_le_neg_ge.
  case (zeq (x mod z) 0); intros m.
  rewrite <- Z_div_zero_opp_full; auto.
  case (zlt z 2); intros.
    assert (z = 1). omega. subst. intuition.
  cut (-x/z < -x). intuition.
  apply Z_div_lt; intuition.
  cut (-(x/z)-1 < -x). intuition.
  rewrite <- Z_div_nz_opp_full; auto.
  apply Z_div_lt; intuition.
  destruct z as [|z|]; intuition. 2: discriminate.
  destruct z; intuition; zify; try omega.
  cut False; intuition.
Qed.

  Lemma ltlt i j :
    Int.min_signed <= i <= Int.max_signed ->
    Int.lt (Int.repr i) j = false ->
    Int.signed j <= i.

Proof.

    unfold Int.lt. destruct zlt. congruence. intros.
    rewrite Int.signed_repr in *; intuition.
  Qed.

  Lemma ltlt' i j :
    Int.min_signed <= i <= Int.max_signed ->
    Int.lt j (Int.repr i) = false ->
    i <= Int.signed j.

Proof.

    unfold Int.lt. destruct zlt. congruence. intros.
    rewrite Int.signed_repr in *; intuition.
  Qed.

Require Import Errors.
Require Import String.
Open Scope error_monad_scope.

Definition get_opt {A} (a:option A) (msg:string) : res A :=
  match a with
    | None => Error (MSG msg::nil)
    | Some a => OK a
  end.

Definition ptree_forall_error {A} (f: positive -> A -> res unit) (m: PTree.t A) : res unit :=
  PTree.fold
    (fun (res: res unit) (i: positive) (x: A) =>
      do _ <- res;
      f i x)
    m (OK tt).

Lemma ptree_forall_error_correct:
  forall (A: Type) (f: positive -> A -> res unit) (m: PTree.t A),
    ptree_forall_error f m = OK tt ->
    forall i x, m!i = Some x -> f i x = OK tt.

Proof.

  unfold ptree_forall_error; intros.
  set (f' := fun (r: res unit) (i: positive) (x: A) => do _ <- r; f i x).
  set (P := fun (m: PTree.t A) (r: res unit) =>
              r = OK tt -> m!i = Some x -> f i x = OK tt).
  assert (P m (OK tt)).
  rewrite <- H. fold f'. apply PTree_Properties.fold_rec.
  unfold P; intros. rewrite <- H1 in H4. auto.
  red; intros. rewrite PTree.gempty in H2. discriminate.
  unfold P; intros. unfold f' in H4.
  destruct a; inv H4.
  rewrite PTree.gsspec in H5. destruct (peq i k).
  inv H5. auto.
  destruct u; auto.
  rewrite H3; auto.
  red in H1. auto.
Qed.

Definition ptree_mem {A} n (m:PTree.t A) : bool :=
  match PTree.get n m with
    | None => false
    | Some _ => true
  end.

Lemma fold_left_cons_map_app {A B:Type} (f: A -> B) :
  forall (l: list A) (k: list B),
  fold_left (fun acc a => f a :: acc) l k = rev (map f l) ++ k.

Proof.

refine (rev_ind _ _ _). reflexivity.
intros. rewrite fold_left_app, map_app, rev_app_distr. simpl. congruence.
Qed.

Lemma flat_map_app {A B: Type} (f: A -> list B) :
forall l m,
flat_map f (l ++ m) = flat_map f l ++ flat_map f m.

Proof.

induction l. reflexivity. simpl. intros. rewrite <- app_assoc. congruence. Qed.

Lemma aux {A B C:Type} (f: A -> B -> C) :
  forall (l: list A) (m: list B) (k: list C),
  fold_left (fun acc a => rev (map (f a) m) ++ acc) l k =
  rev (flat_map (fun a => map (f a) m) l) ++ k.

Proof.

  refine (rev_ind _ _ _). reflexivity.
  intros a l IH.
  intros m k.
  rewrite fold_left_app, flat_map_app, rev_app_distr, IH.
  simpl. rewrite app_assoc. f_equal.
  now rewrite app_nil_r.
Qed.

Lemma aux' {A B C D: Type} (f: A -> B -> C -> D) :
  forall (l: list A) (m: list B) (n: list C) (k: list D),
  fold_left (fun acc a => rev (flat_map (fun b => map (f a b) n) m) ++ acc) l k =
  rev (flat_map (fun a => flat_map (fun b => map (f a b) n) m) l) ++ k.

Proof.

  refine (rev_ind _ _ _). reflexivity.
  intros x l H m n k.
  rewrite fold_left_app. simpl.
  rewrite H, app_assoc, flat_map_app, rev_app_distr. f_equal.
  simpl. rewrite app_nil_r. auto.
Qed.

Lemma fold3 {A B C D:Type} (f: A -> B -> C -> D) :
  forall (l: list A) (m: list B) (n: list C) (k: list D),
  fold_left (fun acc a => fold_left (fun acc b => fold_left (fun acc c => f a b c :: acc) n acc) m acc) l k =
  rev (flat_map (fun a => flat_map (fun b => map (f a b) n) m) l) ++ k.

Proof.

  intros.
  replace (fun acc a => fold_left (fun acc b => fold_left (fun acc c => f a b c :: acc) n acc) m acc)
  with (fun acc a => rev (flat_map (fun b => map (f a b) n) m) ++ acc).
  now rewrite aux'.
  apply Axioms.extensionality. intros o.
  apply Axioms.extensionality. intros y.
  replace (fun acc b => fold_left (fun acc c => f y b c :: acc) n acc)
  with (fun acc b => rev (map (f y b) n) ++ acc).
  now rewrite aux.
  apply Axioms.extensionality. intros.
  apply Axioms.extensionality. intros.
  now rewrite fold_left_cons_map_app.
Qed.