proposition: Lemma bit_not_int : forall x n (SN : (n <? digits = true)%uint63), bit (not_int x) n = negb (bit x n).
proof: Proof. unfold not_int. intros. rewrite! bitE. unfold Uint63.opp. rewrite sub_spec. assert (x = 0 \/ x <> 0)%uint63 by lia. destruct H. - subst. change (to_Z (0 - 0)%uint63) with 0%Z. rewrite Z.bits_0. simpl. change ( - to_Z 1%uint63 mod wB)%Z with (wB - 1)%Z. assert (nat_of_int n <= 62). { unfold nat_of_int, digits in * ; lia. } replace (to_Z n) with (Z.of_nat (nat_of_int n)) by (unfold nat_of_int in * ; lia). set (P := fun n => Z.testbit (wB - 1) (Z.of_nat n)). change (P (nat_of_int n) = true). eapply (forall_n_correct _ 62); auto. - rewrite sub_spec. rewrite Z.sub_0_l. unfold digits in SN. rewrite Z.mod_opp_l_nz. rewrite (Z.mod_small (to_Z x)%Z). rewrite Z.mod_small. rewrite <- (Z.opp_involutive (wB - φ (x)%uint63 - φ (1)%uint63)). rewrite Z.bits_opp. f_equal. replace ((Z.pred (- (wB - φ (x)%uint63 - φ (1)%uint63))))%Z with (to_Z x + (-1) * wB)%Z by lia. rewrite! testbit_0 by lia. replace (-1 * wB)%Z with ((2 * (-1 * 2^(62 - to_Z n))) * 2^(to_Z n))%Z. rewrite Z_div_plus. rewrite Z.mul_comm. rewrite Z_mod_plus_full. reflexivity. apply pow2_pos. lia. unfold wB. change (Z.of_nat size) with 63%Z. replace 63%Z with (1 + (62 - to_Z n) + to_Z n)%Z by lia. rewrite! Z.pow_add_r. all: try (change wB with (2^63)%Z ; lia). Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR