Require Coq.funind.Recdef.
Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Require Import Coq.Sorting.Permutation.
Require Import VST.msl.Coqlib2.
Require Import VST.veric.coqlib4.

Lemma power_nat_one_divede_other: forall n m : nat,
  (two_power_nat n | two_power_nat m) \/ (two_power_nat m | two_power_nat n).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: or (Z.divide (two_power_nat n) (two_power_nat m)) (Z.divide (two_power_nat m) (two_power_nat n)) *)
  pose proof Zle_0_nat n.
(* Goal: or (Z.divide (two_power_nat n) (two_power_nat m)) (Z.divide (two_power_nat m) (two_power_nat n)) *)
  pose proof Zle_0_nat m.
(* Goal: or (Z.divide (two_power_nat n) (two_power_nat m)) (Z.divide (two_power_nat m) (two_power_nat n)) *)
  rewrite !two_power_nat_two_p.
(* Goal: or (Z.divide (two_p (Z.of_nat n)) (two_p (Z.of_nat m))) (Z.divide (two_p (Z.of_nat m)) (two_p (Z.of_nat n))) *)
  destruct (zle (Z.of_nat n) (Z.of_nat m)).
  + left.
(* Goal: Z.divide (two_p (Z.of_nat n)) (two_p (Z.of_nat m)) *)
    exists (two_p (Z.of_nat m - Z.of_nat n)).
(* Goal: @eq Z (two_p (Z.of_nat n)) (Z.mul (two_p (Z.sub (Z.of_nat n) (Z.of_nat m))) (two_p (Z.of_nat m))) *)
    rewrite <- two_p_is_exp by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
    f_equal.
(* Goal: @eq Z z Z0 *)
    omega.
  + right.
(* Goal: Z.divide (two_p (Z.of_nat m)) (two_p (Z.of_nat n)) *)
    exists (two_p (Z.of_nat n - Z.of_nat m)).
(* Goal: @eq Z (two_p (Z.of_nat n)) (Z.mul (two_p (Z.sub (Z.of_nat n) (Z.of_nat m))) (two_p (Z.of_nat m))) *)
    rewrite <- two_p_is_exp by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
    f_equal.
(* Goal: @eq Z z Z0 *)
    omega.
Qed.

Lemma multiple_divide_mod: forall a b c, b > 0 -> ((a | b) \/ (b | a)) -> (a | (c * a mod b)).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq bool b0 true *)
  destruct H0.
  + apply Z.divide_add_cancel_r with (b * (c * a / b))%Z.
(* Goal: Z.divide a (Z.mul b (Z.div (Z.mul c a) b)) *)
(* Goal: Z.divide a (Z.add (Z.mul b (Z.div (Z.mul c a) b)) (Z.modulo (Z.mul c a) b)) *)
    apply Z.divide_mul_l; auto.
(* Goal: Z.divide a (Z.add (Z.mul b (Z.div (Z.mul c a) b)) (Z.modulo (Z.mul c a) b)) *)
    rewrite <- Z_div_mod_eq; auto.
(* Goal: Z.divide a (Z.mul c a) *)
    apply Z.divide_mul_r, Z.divide_refl.
  + destruct H0.
(* Goal: Z.divide a (Z.modulo b c) *)
    subst.
(* Goal: Z.divide (Z.mul x b) (Z.modulo (Z.mul c (Z.mul x b)) b) *)
    rewrite Z.mul_assoc, Z_mod_mult.
(* Goal: Z.divide a Z0 *)
    apply Z.divide_0_r.
Qed.

Lemma divide_align: forall x y: Z, x > 0 -> Z.divide x y -> align y x = y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Z (align y x) y *)
  unfold align.
(* Goal: @eq bool b0 true *)
  destruct H0.
(* Goal: @eq Z (Z.mul (Z.div (Z.sub (Z.add y x) (Zpos xH)) x) x) y *)
  rewrite H0.
  pose proof Zdiv_unique (x0 * x + x - 1) x x0 (x - 1).
  assert (x0 * x + x - 1 = x0 * x + (x - 1)) by omega.
(* Goal: @eq Z z Z0 *)
  assert (0 <= x - 1 < x) by omega.
(* Goal: @eq Z (Z.mul (Z.div (Z.sub (Z.add (Z.mul x0 x) x) (Zpos xH)) x) x) (Z.mul x0 x) *)
  rewrite (H1 H2 H3).
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  reflexivity.
Qed.

Lemma arith_aux00: forall a b, b <= a -> 0%nat = nat_of_Z (a - b) -> a - b = 0.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq nat n (Z.to_nat (Z.sub a (Z.succ b))) *)
  pose proof Z2Nat.id (a - b).
(* Goal: @eq Z (Z.sub a b) Z0 *)
  unfold nat_of_Z in H0.
(* Goal: @eq Z (Z.sub a b) Z0 *)
  rewrite <- H0 in H1.
(* Goal: @eq Z (Z.sub a b) Z0 *)
  simpl Z.of_nat in H1.
(* Goal: @eq Z z Z0 *)
  omega.
Qed.

Lemma arith_aux01: forall a b n, S n = nat_of_Z (a - b) -> b < a.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.lt b a *)
  destruct (zlt a b); auto.
  + rewrite Z2Nat_neg in H by omega.
(* Goal: Z.lt b a *)
    inversion H.
  + pose proof Z2Nat.id (a - b).
(* Goal: Z.lt b a *)
    unfold nat_of_Z in H; rewrite <- H in H0.
(* Goal: Z.lt b a *)
    spec H0; [omega |].
(* Goal: Z.lt b a *)
    rewrite Nat2Z.inj_succ in H0.
(* Goal: @eq Z z Z0 *)
    omega.
Qed.

Lemma arith_aux02: forall n a b, S n = nat_of_Z (a - b) -> n = nat_of_Z (a - Z.succ b).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq nat n (nat_of_Z (Z.sub a (Z.succ b))) *)
  pose proof arith_aux01 _ _ _ H.
(* Goal: @eq nat n (nat_of_Z (Z.sub a (Z.succ b))) *)
  unfold nat_of_Z in *.
(* Goal: @eq nat n (Z.to_nat (Z.sub a (Z.succ b))) *)
  pose proof Z2Nat.id (a - b).
(* Goal: @eq nat n (Z.to_nat (Z.sub a (Z.succ b))) *)
  spec H1; [omega |].
(* Goal: @eq nat n (Z.to_nat (Z.sub a (Z.succ b))) *)
  rewrite <- H in H1.
(* Goal: @eq Z z Z0 *)
  replace (a - Z.succ b) with (a - b - 1) by omega.
(* Goal: @eq nat n (Z.to_nat (Z.sub (Z.sub a b) (Zpos xH))) *)
  rewrite <- H1.
(* Goal: @eq nat n (Z.to_nat (Z.sub (Z.of_nat (S n)) (Zpos xH))) *)
  rewrite Nat2Z.inj_succ.
(* Goal: @eq Z z Z0 *)
  replace (Z.succ (Z.of_nat n) - 1) with (Z.of_nat n) by omega.
(* Goal: @eq nat n (Z.to_nat (Z.of_nat n)) *)
  rewrite Nat2Z.id.
(* Goal: Z.divide a b *)
  auto.
Qed.

Lemma arith_aux03: forall a b c,
  0 <= b ->
  0 <= a + b * c ->
  0 <= a + b * Z.succ c.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.le Z0 (Z.add a (Z.mul b (Z.succ c))) *)
  assert (b * c <= b * Z.succ c) by (apply Zmult_le_compat_l; omega).
(* Goal: @eq Z z Z0 *)
  omega.
Qed.

Lemma arith_aux04: forall a b c,
  0 <= b <= c ->
  (a | b) ->
  (a | b mod c).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a (Z.modulo b c) *)
  destruct (zlt b c).
  + rewrite Zmod_small by omega.
(* Goal: Z.divide a b *)
    auto.
  + assert (b = c) by omega.
(* Goal: Z.divide a (Z.modulo b c) *)
    subst.
(* Goal: Z.divide a (Z.modulo c c) *)
    rewrite Z_mod_same_full.
(* Goal: Z.divide a Z0 *)
    apply Z.divide_0_r.
Qed.

Lemma arith_aux05: forall lo hi, 0 <= lo -> 0 <= hi ->
  0 <= Z.max 0 (hi - lo) <= hi.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: and (Z.le Z0 (Z.add lo (Z.max Z0 (Z.sub hi lo)))) (Z.le (Z.add lo (Z.max Z0 (Z.sub hi lo))) n) *)
  destruct (zle lo hi).
  + rewrite Z.max_r by omega.
(* Goal: @eq Z z Z0 *)
    omega.
  + rewrite Z.max_l by omega.
(* Goal: @eq Z z Z0 *)
    omega.
Qed.

Lemma arith_aux06: forall lo hi n, 0 <= lo <= n -> 0 <= hi <= n -> 0 <= lo + Z.max 0 (hi - lo) <= n.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: and (Z.le Z0 (Z.add lo (Z.max Z0 (Z.sub hi lo)))) (Z.le (Z.add lo (Z.max Z0 (Z.sub hi lo))) n) *)
  destruct (zle lo hi).
  + rewrite Z.max_r by omega.
(* Goal: @eq Z z Z0 *)
    omega.
  + rewrite Z.max_l by omega.
(* Goal: @eq Z z Z0 *)
    omega.
Qed.

Ltac inv_int i :=
  let ofs := fresh "ofs" in
  let H := fresh "H" in
  let H0 := fresh "H" in
  let H1 := fresh "H" in
 match type of i with
 | int => 
  pose proof Int.repr_unsigned i as H;
  pose proof Int.unsigned_range i as H0;
  remember (Int.unsigned i) as ofs eqn:H1;
  rewrite <- H in *;
  clear H H1; try clear i
 | ptrofs => 
  pose proof Ptrofs.repr_unsigned i as H;
  pose proof Ptrofs.unsigned_range i as H0;
  remember (Ptrofs.unsigned i) as ofs eqn:H1;
  rewrite <- H in *;
  clear H H1; try clear i
end.

(**************************************************

Solve_mod_modulus

**************************************************)

Definition int_modm x := x mod Int.modulus.

Lemma int_modm_mod_eq: forall x y, Int.eqmod Int.modulus x y -> x mod Int.modulus = int_modm y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  apply Int.eqmod_mod_eq; auto.
(* Goal: Z.gt Int.modulus Z0 *)
  apply Int.modulus_pos.
Qed.

Lemma int_modm_mod_elim: forall x y, Int.eqmod Int.modulus x y -> Int.eqmod Int.modulus (x mod Int.modulus) y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  eapply Int.eqmod_trans; eauto.
(* Goal: Int.eqmod Int.modulus (Z.modulo x Int.modulus) x *)
  apply Int.eqmod_sym, Int.eqmod_mod.
(* Goal: Z.gt Int.modulus Z0 *)
  apply Int.modulus_pos.
Qed.

Definition int_reprm := Int.repr.

Lemma int_modm_repr_eq: forall x y, Int.eqmod Int.modulus x y -> Int.repr x = int_reprm y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  apply Int.eqm_samerepr; auto.
Qed.

Ltac int_simpl_mod A H :=
  let H0 := fresh "H" in
  let H1 := fresh "H" in
  match A with
  | (?B + ?C)%Z =>
    int_simpl_mod B H0; int_simpl_mod C H1;
    pose proof Int.eqmod_add Int.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (?B - ?C)%Z =>
    int_simpl_mod B H0; int_simpl_mod C H1;
    pose proof Int.eqmod_sub Int.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (?B * ?C)%Z =>
    int_simpl_mod B H0; int_simpl_mod C H1;
    pose proof Int.eqmod_mult Int.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (- ?B)%Z =>
    int_simpl_mod B H0;
    pose proof Int.eqmod_neg Int.modulus _ _ H0 as H;
    clear H0
  | ?B mod Int.modulus =>
    int_simpl_mod B H0;
    pose proof int_modm_mod_elim B _ H0 as H;
    clear H0
  | int_modm ?B =>
    int_simpl_mod B H0;
    pose proof int_modm_mod_elim B _ H0 as H;
    clear H0
  | _ =>
    pose proof Int.eqmod_refl Int.modulus A as H
  end.


Definition ptrofs_modm x := x mod Ptrofs.modulus.

Lemma ptrofs_modm_mod_eq: forall x y, Ptrofs.eqmod Ptrofs.modulus x y -> x mod Ptrofs.modulus = ptrofs_modm y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  apply Ptrofs.eqmod_mod_eq; auto.
(* Goal: Z.gt Ptrofs.modulus Z0 *)
  apply Ptrofs.modulus_pos.
Qed.

Lemma ptrofs_modm_mod_elim: forall x y, Ptrofs.eqmod Ptrofs.modulus x y -> Ptrofs.eqmod Ptrofs.modulus (x mod Ptrofs.modulus) y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  eapply Ptrofs.eqmod_trans; eauto.
(* Goal: Ptrofs.eqmod Ptrofs.modulus (Z.modulo x Ptrofs.modulus) x *)
  apply Ptrofs.eqmod_sym, Ptrofs.eqmod_mod.
(* Goal: Z.gt Ptrofs.modulus Z0 *)
  apply Ptrofs.modulus_pos.
Qed.

Definition ptrofs_reprm := Ptrofs.repr.

Lemma ptrofs_modm_repr_eq: forall x y, Ptrofs.eqmod Ptrofs.modulus x y -> Ptrofs.repr x = ptrofs_reprm y.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: Z.divide a b *)
  apply Ptrofs.eqm_samerepr; auto.
Qed.

Ltac ptrofs_simpl_mod A H :=
  let H0 := fresh "H" in
  let H1 := fresh "H" in
  match A with
  | (?B + ?C)%Z =>
    ptrofs_simpl_mod B H0; ptrofs_simpl_mod C H1;
    pose proof Ptrofs.eqmod_add Ptrofs.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (?B - ?C)%Z =>
    ptrofs_simpl_mod B H0; ptrofs_simpl_mod C H1;
    pose proof Ptrofs.eqmod_sub Ptrofs.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (?B * ?C)%Z =>
    ptrofs_simpl_mod B H0; ptrofs_simpl_mod C H1;
    pose proof Ptrofs.eqmod_mult Ptrofs.modulus _ _ _ _ H0 H1 as H;
    clear H1 H0
  | (- ?B)%Z =>
    ptrofs_simpl_mod B H0;
    pose proof Ptrofs.eqmod_neg Ptrofs.modulus _ _ H0 as H;
    clear H0
  | ?B mod Ptrofs.modulus =>
    ptrofs_simpl_mod B H0;
    pose proof ptrofs_modm_mod_elim B _ H0 as H;
    clear H0
  | ptrofs_modm ?B =>
    ptrofs_simpl_mod B H0;
    pose proof ptrofs_modm_mod_elim B _ H0 as H;
    clear H0
  | _ =>
    pose proof Ptrofs.eqmod_refl Ptrofs.modulus A as H
  end.

Ltac solve_mod_modulus :=
  unfold Int.add; rewrite ?Int.unsigned_repr_eq;
  unfold Ptrofs.add; rewrite ?Ptrofs.unsigned_repr_eq;
  repeat
  match goal with
  | |- context [?A mod Int.modulus] =>
         let H := fresh "H" in int_simpl_mod A H;
         rewrite (int_modm_mod_eq A _ H);
         clear H
  | |- context [Int.repr ?A] =>
         let H := fresh "H" in int_simpl_mod A H;
         rewrite (int_modm_repr_eq A _ H);
         clear H
  | |- context [?A mod Ptrofs.modulus] =>
         let H := fresh "H" in int_simpl_mod A H;
         rewrite (int_modm_mod_eq A _ H);
         clear H
  | |- context [Int.repr ?A] =>
         let H := fresh "H" in int_simpl_mod A H;
         rewrite (int_modm_repr_eq A _ H);
         clear H
  | |- context [?A mod Ptrofs.modulus] =>
         let H := fresh "H" in ptrofs_simpl_mod A H;
         rewrite (ptrofs_modm_mod_eq A _ H);
         clear H
  | |- context [Ptrofs.repr ?A] =>
         let H := fresh "H" in ptrofs_simpl_mod A H;
         rewrite (ptrofs_modm_repr_eq A _ H);
         clear H
  | |- context [?A mod Ptrofs.modulus] =>
         let H := fresh "H" in ptrofs_simpl_mod A H;
         rewrite (ptrofs_modm_mod_eq A _ H);
         clear H
  | |- context [Ptrofs.repr ?A] =>
         let H := fresh "H" in ptrofs_simpl_mod A H;
         rewrite (ptrofs_modm_repr_eq A _ H);
         clear H
  end;
  unfold int_modm, int_reprm, ptrofs_modm, ptrofs_reprm in *.  

(**************************************************

List lemmas

**************************************************)

Lemma add_repr: forall i j, Int.add (Int.repr i) (Int.repr j) = Int.repr (i+j).
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
Proof. intros.
(* Goal: @eq Int.int (Int.add (Int.repr i) (Int.repr j)) (Int.repr (Z.add i j)) *)
  rewrite Int.add_unsigned.
(* Goal: @eq Int.int (Int.repr (Z.opp (Int.unsigned (Int.repr i)))) (Int.repr (Z.opp i)) *)
 apply Int.eqm_samerepr.
(* Goal: Int.eqm (Z.sub (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j))) (Z.sub i j) *)
 unfold Int.eqm.
(* Goal: Int.eqmod Int.modulus (Z.add (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j))) (Z.add i j) *)
 apply Int.eqm_add; apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
Qed.

Lemma mul_repr:
 forall x y, Int.mul (Int.repr x) (Int.repr y) = Int.repr (x * y).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. unfold Int.mul.
(* Goal: @eq Int.int (Int.repr (Z.opp (Int.unsigned (Int.repr i)))) (Int.repr (Z.opp i)) *)
apply Int.eqm_samerepr.
(* Goal: Int.eqm (Z.mul (Int.unsigned (Int.repr x)) (Int.unsigned (Int.repr y))) (Z.mul x y) *)
repeat rewrite Int.unsigned_repr_eq.
apply Int.eqm_mult; unfold Int.eqm; apply Int.eqmod_sym;
apply Int.eqmod_mod; compute; congruence.
Qed.

Lemma sub_repr: forall i j,
  Int.sub (Int.repr i) (Int.repr j) = Int.repr (i-j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Int.int (Int.sub (Int.repr i) (Int.repr j)) (Int.repr (Z.sub i j)) *)
 unfold Int.sub.
(* Goal: @eq Int.int (Int.repr (Z.opp (Int.unsigned (Int.repr i)))) (Int.repr (Z.opp i)) *)
 apply Int.eqm_samerepr.
(* Goal: Int.eqm (Z.sub (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j))) (Z.sub i j) *)
 unfold Int.eqm.
(* Goal: Int.eqmod Int.modulus (Z.sub (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j))) (Z.sub i j) *)
 apply Int.eqm_sub; apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
Qed.

Lemma ptrofs_add_repr: forall i j, Ptrofs.add (Ptrofs.repr i) (Ptrofs.repr j) = Ptrofs.repr (i+j).
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
Proof. intros.
(* Goal: @eq Ptrofs.int (Ptrofs.add (Ptrofs.repr i) (Ptrofs.repr j)) (Ptrofs.repr (Z.add i j)) *)
  rewrite Ptrofs.add_unsigned.
(* Goal: @eq Ptrofs.int (Ptrofs.repr (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j)))) (Ptrofs.repr (Z.sub i j)) *)
 apply Ptrofs.eqm_samerepr.
(* Goal: Ptrofs.eqm (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j))) (Z.sub i j) *)
 unfold Ptrofs.eqm.
(* Goal: Ptrofs.eqmod Ptrofs.modulus (Z.add (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j))) (Z.add i j) *)
 apply Ptrofs.eqm_add; apply Ptrofs.eqm_sym; apply Ptrofs.eqm_unsigned_repr.
Qed.

Lemma ptrofs_mul_repr:
 forall x y, Ptrofs.mul (Ptrofs.repr x) (Ptrofs.repr y) = Ptrofs.repr (x * y).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. unfold Ptrofs.mul.
(* Goal: @eq Ptrofs.int (Ptrofs.repr (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j)))) (Ptrofs.repr (Z.sub i j)) *)
apply Ptrofs.eqm_samerepr.
(* Goal: Ptrofs.eqm (Z.mul (Ptrofs.unsigned (Ptrofs.repr x)) (Ptrofs.unsigned (Ptrofs.repr y))) (Z.mul x y) *)
repeat rewrite Ptrofs.unsigned_repr_eq.
apply Ptrofs.eqm_mult; unfold Ptrofs.eqm; apply Ptrofs.eqmod_sym;
apply Ptrofs.eqmod_mod; compute; congruence.
Qed.

Lemma ptrofs_sub_repr: forall i j,
  Ptrofs.sub (Ptrofs.repr i) (Ptrofs.repr j) = Ptrofs.repr (i-j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Ptrofs.int (Ptrofs.sub (Ptrofs.repr i) (Ptrofs.repr j)) (Ptrofs.repr (Z.sub i j)) *)
 unfold Ptrofs.sub.
(* Goal: @eq Ptrofs.int (Ptrofs.repr (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j)))) (Ptrofs.repr (Z.sub i j)) *)
 apply Ptrofs.eqm_samerepr.
(* Goal: Ptrofs.eqm (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j))) (Z.sub i j) *)
 unfold Ptrofs.eqm.
(* Goal: Ptrofs.eqmod Ptrofs.modulus (Z.sub (Ptrofs.unsigned (Ptrofs.repr i)) (Ptrofs.unsigned (Ptrofs.repr j))) (Z.sub i j) *)
 apply Ptrofs.eqm_sub; apply Ptrofs.eqm_sym; apply Ptrofs.eqm_unsigned_repr.
Qed.

Lemma Zland_two_p:
 forall i n, (0 <= n)%Z -> Z.land i (Z.ones n) = i mod (2 ^ n).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros.
(* Goal: Z.divide a b *)
rewrite Z.land_ones by auto.
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
reflexivity.
Qed.

Lemma and_repr
     : forall i j : Z, Int.and (Int.repr i) (Int.repr j) = Int.repr (Z.land i j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Int.int (Int.and (Int.repr i) (Int.repr j)) (Int.repr (Z.land i j)) *)
  unfold Int.and.
(* Goal: @eq Int.int (Int.repr (Z.land (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j)))) (Int.repr (Z.land i j)) *)
  rewrite <- (Int.repr_unsigned (Int.repr (Z.land i j))).
(* Goal: @eq Int.int (Int.repr (Z.lor (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j)))) (Int.repr (Int.unsigned (Int.repr (Z.lor i j)))) *)
  rewrite !Int.unsigned_repr_eq.
(* Goal: @eq Int.int (Int.repr (Z.lor (Z.modulo i Int.modulus) (Z.modulo j Int.modulus))) (Int.repr (Z.modulo (Z.lor i j) Int.modulus)) *)
  change Int.modulus with (2 ^ 32).
(* Goal: @eq Z z Z0 *)
  rewrite <- !Zland_two_p by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.land (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- !Z.land_assoc.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.land (Z.ones (Zpos (xO (xO (xO (xO (xO xH))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO xH)))))))) *)
  rewrite (Z.land_comm (Z.ones 32)).
(* Goal: @eq Z (Z.land (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- !Z.land_assoc.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
Qed.

Lemma or_repr
     : forall i j : Z, Int.or (Int.repr i) (Int.repr j) = Int.repr (Z.lor i j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Int.int (Int.or (Int.repr i) (Int.repr j)) (Int.repr (Z.lor i j)) *)
  unfold Int.or.
(* Goal: @eq Int.int (Int.repr (Z.lor (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j)))) (Int.repr (Z.lor i j)) *)
  rewrite <- (Int.repr_unsigned (Int.repr (Z.lor i j))).
(* Goal: @eq Int.int (Int.repr (Z.lor (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j)))) (Int.repr (Int.unsigned (Int.repr (Z.lor i j)))) *)
  rewrite !Int.unsigned_repr_eq.
(* Goal: @eq Int.int (Int.repr (Z.lor (Z.modulo i Int.modulus) (Z.modulo j Int.modulus))) (Int.repr (Z.modulo (Z.lor i j) Int.modulus)) *)
  change Int.modulus with (2 ^ 32).
(* Goal: @eq Z z Z0 *)
  rewrite <- !Zland_two_p by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- Z.land_lor_distr_l.
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  reflexivity.
Qed.

Lemma add64_repr: forall i j, Int64.add (Int64.repr i) (Int64.repr j) = Int64.repr (i+j).
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
Proof. intros.
(* Goal: @eq Int64.int (Int64.add (Int64.repr i) (Int64.repr j)) (Int64.repr (Z.add i j)) *)
  rewrite Int64.add_unsigned.
(* Goal: @eq Int64.int (Int64.repr (Z.opp (Int64.unsigned (Int64.repr i)))) (Int64.repr (Z.opp i)) *)
 apply Int64.eqm_samerepr.
(* Goal: Int64.eqm (Z.sub (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j))) (Z.sub i j) *)
 unfold Int64.eqm.
(* Goal: Int64.eqmod Int64.modulus (Z.add (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j))) (Z.add i j) *)
 apply Int64.eqm_add; apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
Qed.

Lemma mul64_repr:
 forall x y, Int64.mul (Int64.repr x) (Int64.repr y) = Int64.repr (x * y).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. unfold Int64.mul.
(* Goal: @eq Int64.int (Int64.repr (Z.opp (Int64.unsigned (Int64.repr i)))) (Int64.repr (Z.opp i)) *)
apply Int64.eqm_samerepr.
(* Goal: Int64.eqm (Z.mul (Int64.unsigned (Int64.repr x)) (Int64.unsigned (Int64.repr y))) (Z.mul x y) *)
repeat rewrite Int64.unsigned_repr_eq.
apply Int64.eqm_mult; unfold Int64.eqm; apply Int64.eqmod_sym;
apply Int64.eqmod_mod; compute; congruence.
Qed.

Lemma sub64_repr: forall i j,
  Int64.sub (Int64.repr i) (Int64.repr j) = Int64.repr (i-j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
 intros. unfold Int64.sub.
(* Goal: @eq Int64.int (Int64.repr (Z.opp (Int64.unsigned (Int64.repr i)))) (Int64.repr (Z.opp i)) *)
 apply Int64.eqm_samerepr.
(* Goal: Int64.eqm (Z.sub (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j))) (Z.sub i j) *)
 unfold Int64.eqm.
(* Goal: Int64.eqmod Int64.modulus (Z.sub (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j))) (Z.sub i j) *)
 apply Int64.eqm_sub; apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr.
Qed.

Lemma and64_repr
     : forall i j : Z, Int64.and (Int64.repr i) (Int64.repr j) = Int64.repr (Z.land i j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Int64.int (Int64.and (Int64.repr i) (Int64.repr j)) (Int64.repr (Z.land i j)) *)
  unfold Int64.and.
(* Goal: @eq Int64.int (Int64.repr (Z.land (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j)))) (Int64.repr (Z.land i j)) *)
  rewrite <- (Int64.repr_unsigned (Int64.repr (Z.land i j))).
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j)))) (Int64.repr (Int64.unsigned (Int64.repr (Z.lor i j)))) *)
  rewrite !Int64.unsigned_repr_eq.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.modulo i Int64.modulus) (Z.modulo j Int64.modulus))) (Int64.repr (Z.modulo (Z.lor i j) Int64.modulus)) *)
  change Int64.modulus with (2 ^ 64).
(* Goal: @eq Z z Z0 *)
  rewrite <- !Zland_two_p by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.land (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- !Z.land_assoc.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.land (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite (Z.land_comm (Z.ones 64)).
(* Goal: @eq Z (Z.land (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- !Z.land_assoc.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
Qed.

Lemma or64_repr
     : forall i j : Z, Int64.or (Int64.repr i) (Int64.repr j) = Int64.repr (Z.lor i j).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Int64.int (Int64.or (Int64.repr i) (Int64.repr j)) (Int64.repr (Z.lor i j)) *)
  unfold Int64.or.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j)))) (Int64.repr (Z.lor i j)) *)
  rewrite <- (Int64.repr_unsigned (Int64.repr (Z.lor i j))).
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Int64.unsigned (Int64.repr i)) (Int64.unsigned (Int64.repr j)))) (Int64.repr (Int64.unsigned (Int64.repr (Z.lor i j)))) *)
  rewrite !Int64.unsigned_repr_eq.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.modulo i Int64.modulus) (Z.modulo j Int64.modulus))) (Int64.repr (Z.modulo (Z.lor i j) Int64.modulus)) *)
  change Int64.modulus with (2 ^ 64).
(* Goal: @eq Z z Z0 *)
  rewrite <- !Zland_two_p by omega.
(* Goal: @eq Int64.int (Int64.repr (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))))) (Int64.repr (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) *)
  f_equal.
(* Goal: @eq Z (Z.lor (Z.land i (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land j (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH)))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  rewrite <- Z.land_lor_distr_l.
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
  reflexivity.
Qed.

Lemma neg_repr: forall i, Int.neg (Int.repr i) = Int.repr (-i).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. unfold Int.neg.
(* Goal: @eq Int.int (Int.repr (Z.opp (Int.unsigned (Int.repr i)))) (Int.repr (Z.opp i)) *)
apply Int.eqm_samerepr.
(* Goal: Int.eqm (Z.opp (Int.unsigned (Int.repr i))) (Z.opp i) *)
apply Int.eqm_neg.
(* Goal: Int.eqm (Int.unsigned (Int.repr i)) i *)
apply Int.eqm_unsigned_repr_l.
(* Goal: Int.eqm i i *)
apply Int.eqm_refl.
Qed.

Lemma neg64_repr: forall i, Int64.neg (Int64.repr i) = Int64.repr (-i).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. unfold Int64.neg.
(* Goal: @eq Int64.int (Int64.repr (Z.opp (Int64.unsigned (Int64.repr i)))) (Int64.repr (Z.opp i)) *)
apply Int64.eqm_samerepr.
(* Goal: Int64.eqm (Z.opp (Int64.unsigned (Int64.repr i))) (Z.opp i) *)
apply Int64.eqm_neg.
(* Goal: Int64.eqm (Int64.unsigned (Int64.repr i)) i *)
apply Int64.eqm_unsigned_repr_l.
(* Goal: Int64.eqm i i *)
apply Int64.eqm_refl.
Qed.

Arguments Int.unsigned n : simpl never.
Arguments Ptrofs.unsigned n : simpl never.
Arguments Pos.to_nat !x / .

Lemma align_0: forall z,
    z > 0 -> align 0 z = 0.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
Proof. unfold align; intros. rewrite Zdiv_small; omega.
Qed.
Hint Rewrite align_0 using omega : norm.

Lemma align_1: forall n, align n 1 = n.
(* Goal: @eq Z z Z0 *)
Proof.  intros; unfold align. rewrite Z.div_1_r. rewrite Z.mul_1_r. omega.
Qed.
Hint Rewrite align_1 using omega : norm.

Lemma fold_right_andb: forall bl b, fold_right andb b bl = true -> forall b0, In b0 bl -> b0 = true.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq bool b0 true *)
  induction bl.
  + inversion H0.
  + destruct H0.
    - simpl in H.
(* Goal: @eq bool b0 true *)
      rewrite andb_true_iff in H.
(* Goal: Z.divide a b *)
      subst; tauto.
    - simpl in H.
(* Goal: @eq bool b0 true *)
      rewrite andb_true_iff in H.
(* Goal: Z.divide a b *)
      tauto.
Qed.

Lemma Z2Nat_inj_0: forall z, z >= 0 -> Z.to_nat z = 0%nat -> z = 0.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @eq Z z Z0 *)
  destruct (zlt 0 z).
  + replace z with (1 + (z - 1)) in H0 by omega.
(* Goal: @eq Z z Z0 *)
    rewrite Z2Nat.inj_add in H0 by omega.
(* Goal: @eq Z z Z0 *)
    change (Z.to_nat 1) with (1%nat) in H0.
(* Goal: @eq Z z Z0 *)
    inversion H0.
  + omega.
Qed.

Lemma Z2Nat_id': forall n, Z.of_nat (Z.to_nat n) = Z.max 0 n.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros.
(* Goal: @eq Z (Z.of_nat (Z.to_nat n)) (Z.max Z0 n) *)
 destruct (zlt n 0).
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
 rewrite Z2Nat_neg by auto. rewrite Z.max_l by omega; reflexivity.
(* Goal: @eq Z z Z0 *)
 rewrite Z2Nat.id, Z.max_r by omega; omega.
Qed.

Lemma nil_or_non_nil: forall {A} (a: list A), {a = nil} + {a <> nil}.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: sumbool (@eq (list A) a (@nil A)) (not (@eq (list A) a (@nil A))) *)
  destruct a; [left | right]; congruence.
Qed.

Lemma Permutation_concat: forall {A} (P Q: list (list A)),
  Permutation P Q ->
  Permutation (concat P) (concat Q).
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
  intros.
(* Goal: @Permutation A (@concat A P) (@concat A Q) *)
  induction H.
  + apply Permutation_refl.
  + simpl.
(* Goal: Z.divide a b *)
    apply Permutation_app_head; auto.
  + simpl.
(* Goal: @Permutation A (@app A y (@app A x (@concat A l))) (@app A x (@app A y (@concat A l))) *)
    rewrite !app_assoc.
(* Goal: @Permutation A (@app A (@app A y x) (@concat A l)) (@app A (@app A x y) (@concat A l)) *)
    apply Permutation_app_tail.
(* Goal: @Permutation A (@app A y x) (@app A x y) *)
    apply Permutation_app_comm.
  + eapply Permutation_trans; eauto.
Qed.

Lemma proj_sumbool_is_false:
  forall (P: Prop) (a: {P}+{~P}), ~P -> proj_sumbool a = false.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros. destruct a; auto; contradiction.
Qed.
Hint Rewrite proj_sumbool_is_true using (solve [auto 3]) : norm.
Hint Rewrite proj_sumbool_is_false using (solve [auto 3]) : norm.

Lemma ptrofs_to_int_repr: 
 forall x, (Ptrofs.to_int (Ptrofs.repr x)) = Int.repr x.
Proof.
(* Goal: forall (P : Prop) (a : sumbool P (not P)) (_ : not P), @eq bool (@proj_sumbool P (not P) a) false *)
intros.
destruct Archi.ptr64 eqn:Hp.
*
unfold Ptrofs.to_int. 
(* Goal: @eq Int.int (Int.repr (Z.opp (Int.unsigned (Int.repr i)))) (Int.repr (Z.opp i)) *)
apply Int.eqm_samerepr.
(* Goal: Int.eqm (Z.sub (Int.unsigned (Int.repr i)) (Int.unsigned (Int.repr j))) (Z.sub i j) *)
unfold Int.eqm.
rewrite Ptrofs.unsigned_repr_eq.
unfold Ptrofs.modulus.
unfold Ptrofs.wordsize.
unfold Wordsize_Ptrofs.wordsize.
rewrite Hp.
unfold Int.modulus.
unfold Int.wordsize.
unfold Wordsize_32.wordsize.
apply Int.eqmod_divides with (two_power_nat 64).
apply Int.eqmod_sym.
apply Int.eqmod_mod.
(* Goal: Z.divide a b *)
compute. auto.
exists (two_power_nat 32).
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
reflexivity.
*
(* Goal: @eq Z (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) (Z.land (Z.lor i j) (Z.ones (Zpos (xO (xO (xO (xO (xO (xO xH))))))))) *)
erewrite Ptrofs.agree32_to_int_eq. reflexivity.
apply Ptrofs.agree32_repr.
(* Goal: Z.divide a b *)
auto.
Qed.




