proposition: Lemma positive_to_Z p : [positive_to_num p] = Zpos p.
proof: Proof. assert (Hi0: (forall i n, to_Z i = Zpower_nat 2 n -> match 2 * i ?= 0 with | Eq => n = 62%nat | Lt => False | Gt => to_Z (2 * i) = Zpower_nat 2 (S n) end)). intros i n Hi. assert (n < 63)%nat. case (to_Z_bounded i); nrom; rewrite Hi; intros Hi1 Hi2. apply Zpower_nat_lt_reg with 2%Z; auto with zarith. assert (HH1: (0 < 2)%Z); auto with zarith. assert (HH2 := Zpower_nat_pos _ (S n) HH1). rewrite compare_spec; case Z.compare_spec. rewrite mul_spec; nrom. rewrite Hi, <- Zpower_nat_S; auto with zarith. assert (H30 : (n <= 62)%nat) by auto with zarith. apply Nat.lt_eq_cases in H30; case H30; auto with zarith; intros HH3. rewrite Zmod_small; auto with zarith. split; auto with zarith. change Uint63.wB with (Zpower_nat 2 63); apply Zpower_nat_lt_compat; auto with zarith. intros HH; contradict HH. case (to_Z_bounded (2 * i)); nrom; auto with zarith. rewrite mul_spec; nrom; rewrite Hi, <- Zpower_nat_S; auto with zarith. assert (H62 : (n <= 62)%nat) by auto with arith. apply Nat.lt_eq_cases in H62; case H62; auto with zarith; intros HH3'. rewrite Zmod_small; nrom; auto with zarith. split; auto with zarith. change Uint63.wB with (Zpower_nat 2 63); apply Zpower_nat_lt_compat; auto with zarith. rewrite HH3', Z_mod_same; auto with zarith. apply Z.lt_gt; auto with zarith. assert (Hij: (forall i j n, to_Z i = Zpower_nat 2 n -> to_Z j < to_Z i -> to_Z (i + j) = to_Z i + to_Z j)%Z). intros i j n Hi Hj. rewrite add_spec, Zmod_small; auto; nrom. case (to_Z_bounded i); case (to_Z_bounded j); nrom; intros H1j H2j H1i H2i; split; auto with zarith. assert (n < 63)%nat. apply Zpower_nat_lt_reg with 2%Z; auto with zarith. rewrite <- Hi; auto with zarith. apply Z.lt_le_trans with (Zpower_nat 2 (S n)). rewrite Zpower_nat_S, <-Hi; auto with zarith. change Uint63.wB with (Zpower_nat 2 63). apply Zpower_nat_le_compat; auto with zarith. assert (H: forall p1 i j n, to_Z i = Zpower_nat 2 n -> (to_Z j < to_Z i -> m_to_Z (positive_aux_to_num p1 i j) = Zpos p1 * to_Z i + to_Z j)%Z). induction p1 as [p1 Hrec| p1 Hrec| ]; simpl positive_aux_to_num; intros i j n Hi Hj. generalize (Hi0 i n Hi); rewrite compare_spec; case Z.compare_spec; nrom. intros Hto_Z Hn; rewrite (Hij i j n), Hi, Hn; auto with zarith. rewrite (Hrec 1 0 0%nat); nrom; auto with zarith. rewrite Zpos_xI; change wB with (2 * Zpower_nat 2 62)%Z; ring. generalize (to_Z_bounded (2 * i)); auto with zarith. intros HH H2i; rewrite (Hrec _ _ (S n)); auto with zarith. rewrite Zpos_xI, H2i, (Hij i j n), Hi, Zpower_nat_S by auto with zarith. ring. rewrite (Hij i j n), H2i, Zpower_nat_S, <- Hi; auto with zarith. generalize (Hi0 i n Hi); rewrite compare_spec; case Z.compare_spec; nrom. intros HH Hn; rewrite Hi, Hn; auto with zarith. rewrite (Hrec 1 0 0%nat); nrom; auto with zarith. rewrite Zpos_xO; change wB with (2 * Zpower_nat 2 62)%Z; ring. generalize (to_Z_bounded (2 * i)); auto with zarith. intros HH H2i; rewrite (Hrec _ _ (S n)); auto with zarith. rewrite Zpos_xO, H2i, Hi, Zpower_nat_S by auto with zarith. ring. case (to_Z_bounded i); intros Hi1 H2. rewrite H2i, Zpower_nat_S, <- Hi; auto with zarith. rewrite to_Z_cons, (Hij i j n); nrom; auto with zarith. unfold positive_to_num. rewrite (H _ _ _ 0%nat); [|auto with zarith|]. nrom; ring. nrom; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63