proposition: Lemma wordToZ_ZToWord: forall z sz, (- Z.of_nat (pow2 sz) <= z < Z.of_nat (pow2 sz))%Z -> wordToZ (ZToWord (S sz) z) = z.
proof: Proof. unfold wordToZ, ZToWord; intros. destruct z. - rewrite wmsb_wzero'. rewrite wordToN_wzero'. reflexivity. - rewrite posToWord_nat. remember (wmsb (natToWord (S sz) (Pos.to_nat p)) false) as msb. destruct msb. + exfalso. simpl in H; destruct H. apply eq_sym, wmsb_true_bound in Heqmsb. rewrite <-positive_N_nat, <-NToWord_nat in Heqmsb. rewrite <-positive_nat_Z in H0. apply Nat2Z.inj_lt in H0. rewrite <-positive_N_nat, <-Npow2_nat in H0. apply Nlt_in in H0. pose proof (wordToN_NToWord (S sz) (N.pos p)). destruct H1 as [k [? ?]]. rewrite H1 in Heqmsb. assert (N.pos p - k * Npow2 (S sz) <= N.pos p)%N by apply N.le_sub_l. assert (Npow2 sz <= N.pos p)%N by (etransitivity; eassumption). apply N.le_ngt in H4; auto. + rewrite wordToN_nat, wordToNat_natToWord_2. * rewrite positive_nat_N; reflexivity. * rewrite <-Npow2_nat, <-positive_N_nat. apply Nlt_out. destruct H. rewrite <-N2Z.inj_pos, <-N_nat_Z in H0. apply Nat2Z.inj_lt in H0. rewrite <-Npow2_nat in H0. apply Nlt_in. rewrite Npow2_S, N2Nat.inj_add. lia. - rewrite wneg_idempotent. rewrite posToWord_nat. remember (wmsb (wneg (natToWord (S sz) (Pos.to_nat p))) false) as msb. destruct msb. + rewrite wordToN_nat, wordToNat_natToWord_2. * rewrite positive_nat_N; reflexivity. * rewrite <-Npow2_nat, <-positive_N_nat. apply Nlt_out. destruct H. apply Z.opp_le_mono in H. rewrite Pos2Z.opp_neg, Z.opp_involutive in H. rewrite <-N2Z.inj_pos, <-N_nat_Z in H. apply Nat2Z.inj_le in H. rewrite <-Npow2_nat in H. apply Nlt_in. rewrite Npow2_S, N2Nat.inj_add. assert (N.to_nat (Npow2 sz) > 0)%nat by (rewrite Npow2_nat; apply pow2_zero). lia. + exfalso. simpl in H. apply eq_sym, wmsb_false_bound in Heqmsb. rewrite wneg_wordToN in Heqmsb. * rewrite Npow2_S in Heqmsb. rewrite <-N.add_0_r in Heqmsb. rewrite <-N.add_sub_assoc in Heqmsb. { apply N.add_lt_mono_l in Heqmsb. exfalso; eapply N.nlt_0_r; eauto. } { destruct H. apply Z.opp_le_mono in H. rewrite Pos2Z.opp_neg, Z.opp_involutive in H. rewrite <-N2Z.inj_pos, <-N_nat_Z in H. apply Nat2Z.inj_le in H. rewrite positive_N_nat in H. rewrite <-positive_N_nat, <-NToWord_nat. pose proof (wordToN_NToWord (S sz) (N.pos p)). destruct H1 as [k [? ?]]; rewrite H1. etransitivity; [apply N.le_sub_l|]. rewrite <-Npow2_nat in H. rewrite <-positive_N_nat in H. unfold N.le; rewrite N2Nat.inj_compare. apply nat_compare_le; auto. } * intro Hx. replace 0%N with (wordToN (wzero (S sz))) in Hx by apply wordToN_wzero. apply wordToN_inj in Hx. assert (wordToNat (natToWord (S sz) (Pos.to_nat p)) = 0) by (rewrite Hx; apply wordToNat_wzero). rewrite wordToNat_natToWord_2 in H0. { clear -H0. induction p; simpl in H0; try discriminate. elim IHp; rewrite Pos2Nat.inj_xO in H0; lia. } { destruct H. apply Z.opp_le_mono in H. rewrite Pos2Z.opp_neg, Z.opp_involutive in H. rewrite <-N2Z.inj_pos, <-N_nat_Z in H. apply Nat2Z.inj_le in H. rewrite positive_N_nat in H. simpl. pose proof (pow2_zero sz). lia. } Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Classes.Equivalence Coq.Arith.PeanoNat Coq.ZArith.BinInt  Coq.Arith.Arith Coq.NArith.NArith Coq.Bool.Bool Coq.ZArith.ZArith Coq.Logic.Eqdep_dec Coq.Logic.EqdepFacts Coq.Program.Tactics Coq.Program.Equality Coq.setoid_ring.Ring Coq.setoid_ring.Ring_polynom bbv.Nomega bbv.ZLib bbv.NatLib bbv.NLib bbv.N_Z_nat_conversions bbv.DepEq bbv.DepEqNat bbv.ReservedNotations Coq.micromega.Lia