Require Import Coq.Arith.EqNat.
Require Import Coq.Relations.Relations.

Require Import compcert.lib.Coqlib.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Floats.
Require Import compcert.common.Values.

Require Import VST.msl.Coqlib2.
Set Implicit Arguments.

(*Open Scope Z.*)

Set Implicit Arguments.
Definition is_true (b: bool) :=
  match b with true => True | false => False end.

Definition force_val (v: option val) : val :=
 match v with Some v' => v' | None => Vundef end.

Definition force_val1 (f: val -> option val) (v: val) := force_val (f v).
Definition force_val2 (f: val -> val -> option val) (v1 v2: val) := force_val (f v1 v2).

Arguments force_val1 f v /.
Arguments force_val2 f v1 v2 /.

Definition force_int (v: val) :=
 match v with
 | Vint i => i | _ => Int.zero
 end.
Arguments force_int !v / .

Definition force_signed_int v := Int.signed (force_int v).
Arguments force_signed_int !v / .

Lemma force_Vint:  forall i, force_int (Vint i) = i.
(* Goal: @eq Int.int (Int.zero_ext Z0 (Int.repr Z0)) (Int.repr Z0) *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
Proof.  reflexivity. Qed.
Hint Rewrite force_Vint : norm.

Definition force_ptr (v: val) : val :=
              match v with Vptr l ofs => v | _ => Vundef  end.

Definition always {A B: Type} (b: B) (a: A) := b.

Definition offset_val (ofs: Z) (v: val) : val :=
  match v with
  | Vptr b z => Vptr b (Ptrofs.add z (Ptrofs.repr ofs))
  | _ => Vundef
 end.

Definition range_s32 (i: Z) : bool := 
   andb (Z.leb Int.min_signed i) (Z.leb i Int.max_signed).

Definition range_s64 (i: Z) : bool := 
   andb (Z.leb Int64.min_signed i) (Z.leb i Int64.max_signed).

Definition is_long (v: val) :=
 match v with Vlong i => True | _ => False end.
Definition is_float (v: val) :=
 match v with Vfloat i => True | _ => False end.
Definition is_single (v: val) :=
 match v with Vsingle i => True | _ => False end.

Definition is_pointer_or_null (v: val) :=
 match v with
 | Vint i => if Archi.ptr64 then False else  i = Int.zero
 | Vlong i => if Archi.ptr64 then i=Int64.zero else False
 | Vptr _ _ => True
 | _ => False
 end.

Definition is_pointer_or_integer (v: val) :=
 match v with
 | Vint i => if Archi.ptr64 then False else True
 | Vlong i => if Archi.ptr64 then True else False
 | Vptr _ _ => True
 | _ => False
 end.

Definition isptr v :=
   match v with | Vptr _ _ => True | _ => False end.

Lemma int_eq_e: forall i j, Int.eq i j = true -> i=j.
Proof. intros. pose proof (Int.eq_spec i j); rewrite H in H0; auto. Qed.

Lemma two_p_neg:
 forall n, n<0 -> two_p n = 0.
Proof.
(* Goal: forall (n : Z) (_ : Z.lt n Z0), @eq Z (two_p n) Z0 *)
destruct n; intros; simpl; auto; try omega.
(* Goal: @eq Z (two_power_pos p) Z0 *)
pose proof (Zgt_pos_0 p); omega.
Qed.

Unset Implicit Arguments.

Lemma testbit_signed_neg:
 forall i j n,
   - two_p n <= Int.signed i < 0 ->
    0 <= n <= j ->
    j < Int.zwordsize ->
   Int.testbit i j = true.
Proof.
(* Goal: forall (n : Z) (i : Int.int) (_ : Z.le (Int.unsigned i) (Z.sub (two_p n) (Zpos xH))), @eq Int.int (Int.zero_ext n i) i *)
intros. rename H1 into Wj.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
pose proof (Int.unsigned_range i).
(* Goal: @eq bool (Int.testbit i j) true *)
unfold Int.signed in H.
(* Goal: @eq bool (Int.testbit i j) true *)
if_tac in H. omega.
(* Goal: @eq bool (Int.testbit i j) false *)
unfold Int.testbit.
(* Goal: @eq bool (Z.testbit (Int.unsigned i) j) true *)
forget (Int.unsigned i) as i'; clear i; rename i' into i.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite <- (Z2Nat.id j) in * by omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
unfold Int.half_modulus in *.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
unfold Int.modulus in *.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
unfold Int.zwordsize in Wj.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
forget Int.wordsize as W.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
assert (Z.to_nat j < W)%nat by (apply Nat2Z.inj_lt; auto).
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
clear Wj.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (W = Z.to_nat j + 1 + (W-Z.to_nat j-1))%nat by omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
forget (W - Z.to_nat j - 1)%nat as K.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
subst W.

(* Goal: @eq bool (Z.testbit i (Z.of_nat O)) true *)
clear H3.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite <- (Z2Nat.id n) in H by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite <- (Z2Nat.id n) in H0 by omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
rewrite <- two_power_nat_two_p in H.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
assert (Z.to_nat n <= Z.to_nat j)%nat.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
  apply Nat2Z.inj_le; omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
clear H0.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
forget (Z.to_nat n) as n'; clear n; rename n' into n.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (Z.to_nat j))) true *)
forget (Z.to_nat j) as j'; clear j; rename j' into j.
(* Goal: @eq bool (Z.testbit i (Z.of_nat j)) true *)
destruct H as [H _].
(* Goal: forall (n : Z) (i : Int.int) (_ : Z.le (Int.unsigned i) (Z.sub (two_p n) (Zpos xH))), @eq Int.int (Int.zero_ext n i) i *)
revert n i H3 H2 H  H1; induction j; intros.
*
simpl (Z.of_nat) in *.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (n=0)%nat by omega. subst n.
(* Goal: @eq bool (Z.testbit i (Z.of_nat O)) true *)
simpl plus in *. clear H3.
(* Goal: @eq bool (Z.testbit i (Z.of_nat O)) true *)
change (- two_power_nat 0) with (-1) in H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (i = (two_power_nat (S K) - 1)) by omega. subst i.
(* Goal: @eq bool (Z.testbit (Z.sub (two_power_nat (S K)) (Zpos xH)) (Z.of_nat O)) true *)
rewrite two_power_nat_S.
(* Goal: @eq bool (Z.testbit (Z.sub (Z.mul (Zpos (xO xH)) (two_power_nat K)) (Zpos xH)) (Z.of_nat O)) true *)
clear.
(* Goal: @eq bool (Z.testbit (Z.sub (Z.mul (Zpos (xO xH)) (two_power_nat K)) (Zpos xH)) (Z.of_nat O)) true *)
forget (two_power_nat K) as A.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
replace A with ((A-1)+1) by omega.
(* Goal: @eq bool (Z.testbit (Z.sub (Z.mul (Zpos (xO xH)) (Z.add (Z.sub A (Zpos xH)) (Zpos xH))) (Zpos xH)) (Z.of_nat O)) true *)
rewrite Z.mul_add_distr_l.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
replace (2 * (A - 1) + 2 * 1 - 1) with (2 * (A - 1) + 1) by omega.
(* Goal: @eq bool (Z.testbit (Z.add (Z.mul (Zpos (xO xH)) (Z.sub A (Zpos xH))) (Zpos xH)) (Z.of_nat O)) true *)
apply Z.testbit_odd_0.
*
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
destruct n.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
change (- two_power_nat 0)%Z with (-1) in H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (i = two_power_nat (S j + 1 + K) - 1) by omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
clear H H1 H2.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
subst i.
(* Goal: @eq bool (Z.testbit (Z.sub (two_power_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K)) (Zpos xH)) (Z.of_nat (S j))) true *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
replace (two_power_nat (S j + 1 + K) - 1) with (Z.ones (Z.of_nat (S j + 1 + K))).
(* Goal: @eq bool (Z.testbit (Z.ones (Z.of_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K))) (Z.of_nat (S j))) true *)
(* Goal: @eq Z (Z.ones (Z.of_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K))) (Z.sub (two_power_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K)) (Zpos xH)) *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
apply Z.ones_spec_low. split; [omega | ].
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
apply Nat2Z.inj_lt. omega.
(* Goal: @eq Z (Z.ones (Z.of_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K))) (Z.sub (two_power_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K)) (Zpos xH)) *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
rewrite Z.ones_equiv.
(* Goal: @eq Z (Z.pred (Z.pow (Zpos (xO xH)) (Z.of_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K)))) (Z.sub (two_power_nat (Init.Nat.add (Init.Nat.add (S j) (S O)) K)) (Zpos xH)) *)
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
rewrite two_power_nat_equiv.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq bool (Z.testbit i (Z.of_nat (S j))) true *)
rewrite inj_S.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Int.Ztestbit_succ by omega.
(* Goal: @eq bool (Z.testbit (Z.div2 i) (Z.of_nat j)) true *)
apply (IHj n); clear IHj.
+
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
+
(* Goal: Z.ge (Z.div2 i) (Z.div (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K)) (Zpos (xO xH))) *)
rewrite Zdiv2_div.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
apply Z_div_ge; try omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
replace (S j + 1 + K)%nat with (S (j + 1 + K))%nat in H2 by omega.
(* Goal: Z.ge i (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K)) *)
rewrite two_power_nat_S in H2.
(* Goal: Z.ge i (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K)) *)
rewrite Z.mul_comm in H2.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z_div_mult_full in H2 by omega. auto.
+
(* Goal: Z.le (Z.opp (two_power_nat n)) (Z.sub (Z.div2 i) (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K))) *)
rewrite two_power_nat_S in H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
replace (S j + 1 + K)%nat with (S (j + 1 + K))%nat in H by omega.
(* Goal: Z.le (Z.opp (two_power_nat n)) (Z.sub (Z.div2 i) (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K))) *)
rewrite two_power_nat_S in H.
(* Goal: Z.le (Z.opp (two_power_nat n)) (Z.sub (Z.div2 i) (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K))) *)
rewrite (Zdiv2_odd_eqn i) in H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (Z.odd i) eqn:?H; omega.
+
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
replace (S j + 1 + K)%nat with (S (j + 1 + K))%nat in H1 by omega.
(* Goal: and (Z.le Z0 (Z.div2 i)) (Z.lt (Z.div2 i) (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K))) *)
rewrite two_power_nat_S in H1.
(* Goal: and (Z.le Z0 (Z.div2 i)) (Z.lt (Z.div2 i) (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K))) *)
rewrite (Zdiv2_odd_eqn i) in H1.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (Z.odd i) eqn:?H; omega.
Qed.

Lemma sign_ext_inrange:
  forall n i, - two_p (n-1) <= Int.signed i <= two_p (n-1) - 1 ->
       Int.sign_ext n i = i.
Proof.
(* Goal: forall (n : Z) (i : Int.int) (_ : Z.le (Int.unsigned i) (Z.sub (two_p n) (Zpos xH))), @eq Int.int (Int.zero_ext n i) i *)
intros.
destruct (zlt n Int.zwordsize);
  [ | apply Int.sign_ext_above; auto].
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (zlt n 0).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (n-1 < 0) by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
repeat rewrite two_p_neg in H by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (zeq n 0).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
subst n. simpl in H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (Int.signed i = 0) by omega.
(* Goal: @eq Int.int (Int.zero_ext Z0 i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
clear - H0.
(* Goal: @eq Int.int (Int.sign_ext Z0 i) i *)
(* Goal: @eq Int.int (Int.sign_ext n i) i *)
rewrite <- (Int.repr_signed i).
(* Goal: @eq Int.int (Int.zero_ext Z0 (Int.repr Z0)) (Int.repr Z0) *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite H0. reflexivity.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (0 < n < Int.zwordsize) by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
clear - H H0.

(* Goal: @eq Int.int (Int.zero_ext n i) i *)
apply Int.same_bits_eq; intros j ?.
(* Goal: @eq bool (Int.testbit (Int.sign_ext n i) j) (Int.testbit i j) *)
destruct H0.
(* Goal: @eq bool (Int.testbit (Int.sign_ext n i) j) (Int.testbit i j) *)
rewrite (Int.bits_sign_ext n i j H1 H0).
(* Goal: Z.ge i (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K)) *)
if_tac; auto.
(* Goal: @eq bool (Int.testbit i (Z.sub n (Zpos xH))) (Int.testbit i j) *)
destruct H1.
(* Goal: @eq bool (Int.testbit i (Z.sub n (Zpos xH))) (Int.testbit i j) *)
destruct (zlt (Int.signed i) 0).
* (* negative *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (- two_p (n - 1) <= Int.signed i  < 0) by omega.
(* Goal: @eq bool (Int.testbit i (Z.sub n (Zpos xH))) (Int.testbit i j) *)
clear H.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite (testbit_signed_neg i (n-1) (n-1)); auto; try omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite (testbit_signed_neg i j (n-1)%Z); auto; omega.
* (* nonnegative *)
(* Goal: @eq bool (Int.testbit i (Z.sub n (Zpos xH))) (Int.testbit i j) *)
rewrite Int.signed_eq_unsigned in H by (apply Int.signed_positive; auto).
unfold Int.testbit in *.
(* Goal: @eq bool (Z.testbit (Int.unsigned i) (Z.sub n (Zpos xH))) (Z.testbit (Int.unsigned i) j) *)
transitivity false.
(* Goal: @eq bool (Z.testbit (Int.unsigned i) j) false *)
apply (Int.Ztestbit_above (Z.to_nat (n-1))).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.lt (Int.unsigned i) (two_power_nat (Z.to_nat n))) *)
rewrite two_power_nat_two_p.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z2Nat.id by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
pose proof (Int.unsigned_range i).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z2Nat.id by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq bool false (Int.testbit i j) *)
symmetry.
(* Goal: @eq bool (Z.testbit (Int.unsigned i) j) false *)
apply (Int.Ztestbit_above (Z.to_nat (n-1))).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.lt (Int.unsigned i) (two_power_nat (Z.to_nat n))) *)
rewrite two_power_nat_two_p.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z2Nat.id by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
pose proof (Int.unsigned_range i).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z2Nat.id by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
Qed.

Lemma zero_ext_inrange:
  forall n i, Int.unsigned i <= two_p n - 1 ->
       Int.zero_ext n i = i.
Proof.
(* Goal: forall (n : Z) (i : Int.int) (_ : Z.le (Int.unsigned i) (Z.sub (two_p n) (Zpos xH))), @eq Int.int (Int.zero_ext n i) i *)
intros.
destruct (zlt n Int.zwordsize);
  [ | apply Int.zero_ext_above; auto].
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (zlt n 0).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (n-1 < 0) by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
repeat rewrite two_p_neg in H by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
pose proof (Int.unsigned_range i).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
destruct (zeq n 0).
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
subst n. simpl in H.
(* Goal: @eq Int.int (Int.zero_ext Z0 i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (Int.unsigned i = 0) by (pose proof (Int.unsigned_range i); omega).
(* Goal: @eq Int.int (Int.zero_ext Z0 i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
clear - H0.
(* Goal: @eq Int.int (Int.zero_ext Z0 i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite <- (Int.repr_unsigned i).
(* Goal: @eq Int.int (Int.zero_ext Z0 (Int.repr Z0)) (Int.repr Z0) *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite H0. reflexivity.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
assert (0 < n < Int.zwordsize) by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
clear - H H0.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
apply Int.same_bits_eq; intros j ?.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite (Int.bits_zero_ext n i j) by omega.
(* Goal: Z.ge i (two_power_nat (Init.Nat.add (Init.Nat.add j (S O)) K)) *)
if_tac; auto.
(* Goal: @eq bool false (Int.testbit i j) *)
symmetry.
(* Goal: @eq bool (Int.testbit i j) false *)
unfold Int.testbit.
apply (Int.Ztestbit_above (Z.to_nat n));
 [ | rewrite Z2Nat.id by omega; omega].
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.lt (Int.unsigned i) (two_power_nat (Z.to_nat n))) *)
rewrite two_power_nat_two_p.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
rewrite Z2Nat.id by omega.
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
(* Goal: @eq Int.int (Int.zero_ext n i) i *)
pose proof (Int.unsigned_range i); omega.
Qed.
