proposition: Lemma spec_int63i s p : (Zpos p <= 63)%Z -> (to_Z s / 2 ^ (Zpos p - 1) mod 2 = if int63i s p then 1 else 0)%Z.
proof: Proof. intro H; unfold int63i. case (phi_toZ s); intros Hs1 Hs2. assert (F1: (to_Z 1 <= 63)%Z). rewrite phi1; intros HH; discriminate. assert (F2: (to_Z (shiftr63 (shiftr63 s (p2t63 p)) 1) = to_Z s / 2 ^ (Zpos p))%Z). repeat (rewrite phi_shiftr63; auto); rewrite phi_p2t63; auto with zarith. rewrite Zdiv_Zdiv; auto with zarith. rewrite <- Zpower_exp; try rewrite phi1; auto with zarith. replace (Zpos p - 1 + 1)%Z with (Zpos p); auto with zarith. assert (F3: (to_Z (shiftr63 (shiftr63 s (p2t63 p)) 1) * 2 ^ to_Z 1 < 2 ^ 63)%Z). rewrite phi1; rewrite F2; rewrite Zpow_facts.Zpower_1_r. change (2^63)%Z with (2^62 * 2)%Z. apply Zmult_lt_compat_r; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. apply Z.lt_le_trans with (1 := Hs2). change (2 ^ 63)%Z with (2 ^ 62 * 2 ^ 1)%Z. apply Zmult_le_compat_l; auto with zarith. apply Zpow_facts.Zpower_le_monotone; auto with zarith. assert (F4: (to_Z (p2t63 p) < 63)%Z). rewrite phi_p2t63; auto with zarith. assert (F5: (2 ^ Zpos p = 2 ^ (Zpos p - 1) * 2)%Z). assert (FF: (0 < Zpos p)%Z); try (red; auto; fail). replace (2 ^ (Zpos p))%Z with (2 ^ (Zpos p -1 + 1))%Z. rewrite Zpower_exp; auto with zarith. apply f_equal2 with (f := Zpower); auto with zarith. match goal with |- context[?X ?= ?Y] => generalize (phi_compare63 X Y); case compare end; rewrite phi_shiftl63; auto; rewrite F2; rewrite phi_shiftr63; auto with zarith; rewrite phi1; rewrite Zpow_facts.Zpower_1_r; rewrite phi_p2t63; auto; set (u := (to_Z s/ (2 ^ (Zpos p - 1)))%Z); pattern u at 1; rewrite (Z_div_mod_eq_full u 2%Z); auto with zarith; unfold u; rewrite Zdiv_Zdiv; auto with zarith; replace (2 ^ (Zpos p - 1) * 2)%Z with (2 ^(Zpos p))%Z; auto with zarith; rewrite Zmult_comm; fold u; case (Z_mod_lt u 2); auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik