proposition: Lemma bit_add_or x y: (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%uint63= x lor y.
proof: Proof. generalize x y (to_Z_bounded x) (to_Z_bounded y); clear x y. unfold wB; elim size. - replace (2^Z_of_nat 0) with 1%Z; auto with zarith. intros x y Hx Hy; replace x with 0%uint63. + replace y with 0%uint63. { split; auto; intros _ n; rewrite !bit_0; discriminate. } apply to_Z_inj; rewrite to_Z_0; auto with zarith. + apply to_Z_inj; rewrite to_Z_0; auto with zarith. - intros n IH x y; rewrite inj_S. unfold Z.succ; rewrite Zpower_exp, Z.pow_1_r; auto with zarith. intros Hx Hy. split. + intros Hn. assert (F1: ((x >> 1) + (y >> 1))%uint63 = (x >> 1) lor (y >> 1)). { apply IH. - rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. - rewrite lsr_spec, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. - intros m H1 H2. case_eq (digits <=? m)%uint63; [idtac | rewrite <- not_true_iff_false]; intros Heq. + rewrite bit_M in H1; auto; discriminate. + rewrite leb_spec in Heq. apply (Hn (m + 1)%uint63); rewrite <-bit_half; auto; rewrite ltb_spec; auto with zarith. } rewrite (bit_split (x lor y)), lor_lsr, <- F1, lor_spec. replace (b2i (bit x 0 || bit y 0)) with (bit x 0 + bit y 0)%uint63. 2: generalize (Hn 0%uint63); do 2 case bit; auto; intros [ ]; auto. rewrite lsl_add_distr. rewrite (bit_split x) at 1; rewrite (bit_split y) at 1. rewrite <-!add_assoc; apply (f_equal2 add); auto. rewrite add_comm, <-!add_assoc; apply (f_equal2 add); auto. rewrite add_comm; auto. + intros Heq. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. generalize Heq; rewrite (bit_split x) at 1; rewrite (bit_split y )at 1; clear Heq. rewrite (fun y => add_comm y (bit x 0)), <-!add_assoc, add_comm, <-!add_assoc, (add_comm (bit y 0)), add_assoc, <-lsl_add_distr. rewrite (bit_split (x lor y)), lor_spec. intros Heq. assert (F: (bit x 0 + bit y 0)%uint63 = (bit x 0 || bit y 0)). { assert (F1: (2 | wB)) by (apply Zpower_divide; apply refl_equal). assert (F2: 0 < wB) by (apply refl_equal). assert (F3: φ (bit x 0 + bit y 0) mod 2 = φ (bit x 0 || bit y 0) mod 2). { apply trans_equal with ((φ ((x>>1 + y>>1) << 1) + φ (bit x 0 + bit y 0)) mod 2). - rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith. rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. - rewrite (Zmod_div_mod 2 wB), <-add_spec, Heq; auto with zarith. rewrite add_spec, <-Zmod_div_mod; auto with zarith. rewrite lsl_spec, Zplus_mod, <-Zmod_div_mod; auto with zarith. rewrite Z.pow_1_r, Z_mod_mult, Zplus_0_l, Zmod_mod; auto with zarith. } generalize F3; do 2 case bit; try discriminate; auto. } case (IH (x >> 1) (y >> 1)). * rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. * rewrite lsr_spec, to_Z_1, Z.pow_1_r; split; auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. * intros _ HH m; case (to_Z_bounded m); intros H1m H2m. case_eq (digits <=? m)%uint63. -- intros Hlm; rewrite bit_M; auto; discriminate. -- rewrite <- not_true_iff_false, leb_spec; intros Hlm. case (Zle_lt_or_eq 0 φ m); auto; intros Hm. ++ replace m with ((m -1) + 1)%uint63. { rewrite <-(bit_half x), <-(bit_half y); auto with zarith. - apply HH. rewrite <-lor_lsr. assert (0 <= φ (bit (x lor y) 0) <= 1) by (case bit; split; discriminate). rewrite F in Heq; generalize (add_cancel_r _ _ _ Heq). intros Heq1; apply to_Z_inj. generalize (f_equal to_Z Heq1); rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small. + rewrite lsl_spec, to_Z_1, Z.pow_1_r, Zmod_small; auto with zarith. case (to_Z_bounded (x lor y)); intros H1xy H2xy. rewrite lsr_spec, to_Z_1, Z.pow_1_r; auto with zarith. change wB with ((wB/2)*2); split; auto with zarith. assert (φ (x lor y) / 2 < wB / 2); auto with zarith. apply Zdiv_lt_upper_bound; auto with zarith. + split. * case (to_Z_bounded (x >> 1 + y >> 1)); auto with zarith. * rewrite add_spec. apply Z.le_lt_trans with ((φ (x >> 1) + φ (y >> 1)) * 2); auto with zarith. -- case (Z.mod_bound_pos_le (φ (x >> 1) + φ (y >> 1)) wB); auto with zarith. case (to_Z_bounded (x >> 1)); case (to_Z_bounded (y >> 1)); auto with zarith. -- generalize Hb; rewrite (to_Z_split x) at 1; rewrite (to_Z_split y) at 1. case (to_Z_bounded (bit x 0)); case (to_Z_bounded (bit y 0)); auto with zarith. - rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith. - rewrite ltb_spec, sub_spec, to_Z_1, Zmod_small; auto with zarith. } apply to_Z_inj. rewrite add_spec, sub_spec, Zplus_mod_idemp_l, to_Z_1, Zmod_small; auto with zarith. ++ pose proof (to_Z_inj 0 _ Hm); clear Hm; subst m. intros hx hy; revert F; rewrite hx, hy; intros F. generalize (f_equal to_Z F). vm_compute. lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63