proposition: Lemma bit_lsl x i j : bit (x << i) j = (if (j <? i) || (digits <=? j) then false else bit x (j - i))%uint63.
proof: Proof. assert (F1: 1 >= 0) by discriminate. case_eq (digits <=? j)%uint63; intros H. - rewrite orb_true_r, bit_M; auto. - set (d := φ digits). case (Zle_or_lt d (φ j)); intros H1. 1:case (leb_spec digits j); rewrite H; auto with zarith. 1:intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl. + change 62%uint63 with (digits - 1)%uint63. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. apply sym_equal; rewrite is_zero_spec; apply to_Z_inj. rewrite lsl_spec, lsr_spec, lsl_spec. replace wB with (2^d); auto. pattern d at 1; replace d with ((d - (φ j + 1)) + (φ j + 1))%Z by ring. rewrite Zpower_exp; auto with zarith. replace φ i with ((φ i - (φ j + 1)) + (φ j + 1))%Z by ring. rewrite -> Zpower_exp, Zmult_assoc; auto with zarith. rewrite Zmult_mod_distr_r. rewrite -> Zplus_comm, Zpower_exp, !Zmult_assoc; auto with zarith. rewrite -> Z_div_mult_full; auto with zarith. rewrite <-Zmult_assoc, <-Zpower_exp; auto with zarith. replace (1 + φ digits - 1)%Z with d; auto with zarith. rewrite Z_mod_mult; auto. + case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2. 2: generalize (H3 F2); discriminate. clear H2 H3. apply (f_equal negb). apply (f_equal is_zero). apply to_Z_inj. rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto. rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. rewrite !Zmult_mod_distr_r. apply (f_equal2 Zmult); auto. replace wB with (2^ d); auto with zarith. replace d with ((d - φ i) + φ i)%Z by ring. case (to_Z_bounded i); intros H1i H2i. rewrite Zpower_exp; auto with zarith. rewrite Zmult_mod_distr_r. case (to_Z_bounded j); intros H1j H2j. replace φ (j - i) with (φ j - φ i)%Z. 2: rewrite sub_spec, Zmod_small; auto with zarith. set (d1 := (d - φ i)%Z). set (d2 := (φ j - φ i)%Z). pattern φ j at 1; replace φ j with (d2 + φ i)%Z. 2: unfold d2; ring. rewrite -> Zpower_exp; auto with zarith. rewrite -> Zdiv_mult_cancel_r. 2: generalize (Zpower2_lt_lin φ i H1i); auto with zarith. rewrite -> (Z_div_mod_eq_full φ x (2^d1)) at 2. pattern d1 at 2; replace d1 with (d2 + (1+ (d - φ j - 1)))%Z by (unfold d1, d2; ring). rewrite Zpower_exp; auto with zarith. rewrite <-Zmult_assoc, Zmult_comm. rewrite Zdiv.Z_div_plus_full_l; auto with zarith. rewrite Zpower_exp, Z.pow_1_r; auto with zarith. rewrite <-Zplus_mod_idemp_l. rewrite <-!Zmult_assoc, Zmult_comm, Z_mod_mult, Zplus_0_l; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63