proposition: Lemma int63aif s p q : (Zpos p <= 63)%Z -> (Zpos q <= 63)%Z -> int63i s p = false -> p <> q -> int63i (int63a s p) q = int63i s q.
proof: Proof. intros Hp Hq H Hd. assert (F0: (0 < Zpos p)%Z); try (red; auto; fail). assert (F1: (0 < 2 ^ (Zpos p - 1))%Z). now apply Z.pow_pos_nonneg; auto with zarith. assert (F2: (0 < Zpos q)%Z); try (red; auto; fail). assert (F3: (0 < 2 ^ (Zpos q - 1))%Z). now apply Z.pow_pos_nonneg; auto with zarith. generalize (spec_int63i s p Hp); rewrite H; intros H1. case (phi_toZ s); intros Hs1 Hs2. generalize (spec_int63i s q Hq) (spec_int63i (int63a s p) q Hq). replace ((to_Z s / 2 ^ (Zpos q - 1)) mod 2)%Z with ((to_Z (int63a s p) / 2 ^ (Zpos q - 1)) mod 2)%Z. now intros HH; rewrite HH; case int63i; case int63i; auto; intros; discriminate. 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. assert (F : (to_Z s = 2 ^ (Zpos p) * (to_Z s / 2 ^ (Zpos p)) + (to_Z s mod (2^ (Zpos p - 1))))%Z). 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 H1. rewrite Zmult_0_r; rewrite Zplus_0_l. rewrite Zmod_mod; apply Zmod_small. now case (Z_mod_lt (to_Z s) (2 ^ (Zpos p - 1))%Z); auto with zarith. rewrite <- Zpower_exp; auto with zarith. now apply f_equal2 with (f := Zpower); auto with zarith. rewrite (fun x => Zmod_small x (2 ^ 63)%Z). case (Zle_or_lt (Zpos p) (Zpos q)); intros H2. case (Zle_lt_or_eq _ _ H2); clear H2; intros H2. replace (2 ^ (Zpos q - 1))%Z with (2^(Zpos p + (Zpos q - Zpos p -1)))%Z. rewrite Zpower_exp; try rewrite <- Zdiv_Zdiv; auto with zarith. pattern (to_Z s) at 1; rewrite F. rewrite <- Zplus_assoc; rewrite Z.add_comm; rewrite Zmult_comm. rewrite Z_div_plus_full; auto with zarith. rewrite (Zdiv_small (to_Z s mod 2 ^ (Zpos p - 1) + 2 ^ (Zpos p - 1))%Z); auto with zarith. now rewrite Zplus_0_l; rewrite Zdiv_Zdiv; auto with zarith. case (Z_mod_lt (to_Z s) (2^(Zpos p - 1))%Z); auto with zarith; intros Hm1 Hm2. split; auto with zarith. replace (2 ^ Zpos p)%Z with (2^1 * (2 ^ (Zpos p - 1)))%Z. now rewrite Zpow_facts.Zpower_1_r; auto with zarith. now rewrite <- Zpower_exp; auto with zarith; apply f_equal2 with (f := Zpower); auto with zarith. now apply f_equal2 with (f := Zpower); auto with zarith. now case Hd; injection H2; auto. replace (2 ^ (Zpos p - 1))%Z with (2 ^ (Zpos p - Zpos q) * 2 ^ (Zpos q - 1))%Z. 2: rewrite <- Zpower_exp; auto with zarith. 2: now apply f_equal2 with (f := Zpower); auto with zarith. rewrite Z_div_plus_full; auto with zarith. rewrite Zplus_mod. replace (2 ^ (Zpos p - Zpos q) mod 2)%Z with 0%Z. now rewrite Zplus_0_r; apply Zmod_mod; auto. replace (Zpos p - Zpos q)%Z with (1 + (Zpos p - Zpos q - 1))%Z; try ring. rewrite Zpower_exp; auto with zarith. now rewrite Zpow_facts.Zpower_1_r; rewrite Zmult_comm; rewrite Z_mod_mult; auto. split; auto with zarith. rewrite F. 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. now 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. now rewrite Zpow_facts.Zpower_1_r; auto with zarith. now 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. now 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. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik