proposition: Lemma int63ai s p : (Zpos p <= 63)%Z -> int63i s p = false -> int63i (int63a s p) p = true.
proof: Proof. intros H H1. assert (F0: (0 < Zpos p)%Z); try (red; auto; fail). assert (F1: (0 < 2 ^ (Zpos p - 1))%Z); auto with zarith. case (phi_toZ s); intros Hs1 Hs2. generalize (spec_int63i s p H); rewrite H1; intros H2. generalize (spec_int63i (int63a s p) p H). case int63i; auto. unfold int63a. rewrite phi_add; rewrite phi_shiftl63; rewrite phi_p2t63; try (rewrite phi1; rewrite Zmult_1_l); auto with zarith. 2: apply Zpow_facts.Zpower_lt_monotone; auto with zarith. rewrite (fun x => Zmod_small x (2^63)%Z). - generalize (Z_div_plus_full (to_Z s) 1%Z (2 ^ (Zpos p - 1))%Z). rewrite Zmult_1_l; intros HH; rewrite HH; clear HH; auto with zarith. rewrite Zplus_mod; rewrite H2; rewrite Zplus_0_l; repeat rewrite Zmod_small; auto with zarith. - split; auto with zarith. replace (to_Z s) with (2^(Zpos p) * (to_Z s / 2 ^ (Zpos p)) + (to_Z s mod (2^ (Zpos p - 1))))%Z. + apply Z.lt_le_trans with (2 ^ Zpos p * (to_Z s / 2 ^ Zpos p) + 2 ^ Zpos p)%Z. rewrite <- Zplus_assoc; apply Zplus_lt_compat_l. apply Z.le_lt_trans with (2 ^ (Zpos p - 1) - 1 + 2 ^ (Zpos p - 1))%Z. * apply Zplus_le_compat_r. case (Z_mod_lt (to_Z s) (2 ^ (Zpos p - 1))); auto with zarith. * replace (2 ^Zpos p)%Z with (2^(Zpos p -1) * 2 ^1)%Z. -- rewrite Zpow_facts.Zpower_1_r; auto with zarith. -- rewrite <- Zpower_exp; auto with zarith; apply f_equal2 with (f := Zpower); auto with zarith. * replace (2 ^ Zpos p * (to_Z s / 2 ^ Zpos p) + 2 ^ Zpos p)%Z with (2 ^ Zpos p * (to_Z s / 2 ^ Zpos p + 1))%Z; try ring. replace (2 ^ 63)%Z with (2 ^ (Zpos p) * (2^ (63 - Zpos p)))%Z. -- apply Zmult_le_compat_l; auto with zarith. assert (to_Z s / 2 ^ Zpos p < 2 ^ (63 - Zpos p))%Z; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. rewrite <- Zpower_exp; auto with zarith. replace (63 - Zpos p + Zpos p)%Z with 63%Z; auto; ring. -- rewrite <- Zpower_exp; auto with zarith. apply f_equal2 with (f := Zpower); auto; ring. + apply sym_equal. pattern (to_Z s) at 1; rewrite (Z_div_mod_eq_full (to_Z s) (2 ^ Zpos p)%Z). * apply f_equal2 with (f := Zplus); auto. pattern (to_Z s) at 1; rewrite (Z_div_mod_eq_full (to_Z s) (2 ^ (Zpos p - 1))%Z). -- rewrite Zplus_mod. replace (2 ^(Zpos p))%Z with (2^(Zpos p - 1) * (2 ^ 1))%Z. ++ rewrite Zmult_mod_distr_l; rewrite Zpow_facts.Zpower_1_r; rewrite H2. rewrite Zmult_0_r; rewrite Zplus_0_l. rewrite Zmod_mod; apply Zmod_small. case (Z_mod_lt (to_Z s) (2 ^ (Zpos p - 1))%Z); auto with zarith. ++ rewrite <- Zpower_exp; auto with zarith. apply f_equal2 with (f := Zpower); auto with zarith. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik