Module DLib

Utility definitions by David.

Require Export Classical.
Require Export Coqlib.
Require Export 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 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.

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

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.

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.

Generated by coq2html