proposition: Lemma iter_int63_aux_S : forall n i A f a, (0 < to_Z i < 2 ^ Z.of_nat n)%Z -> iter_int63_aux n i A f a = f (iter_int63_aux n (i - 1) A f a).
proof: Proof. intros n i A f; revert i; induction n; intros i a Hi. { change (0 < φ (i) < 1)%Z in Hi. lia. } simpl. replace (i =? 0) with false. { rewrite bit_sub1_0, sub1_lsr. { case_eq (bit i 0); simpl. { intros _. case_eq (i =? 1). { rewrite eqb_spec; intro H; rewrite H in *; clear i H. case n; reflexivity. } rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. replace (i - 1 =? 0) with false. { reflexivity. } symmetry. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. } intro Hibit. case_eq (i =? 1). { rewrite eqb_spec; intro H; rewrite H in *; clear i H; discriminate. } rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_1; intro Hi1. replace (i - 1 =? 0) with false. { case_eq (i =? 2). { rewrite eqb_spec; intro H; rewrite H in *; clear i H. destruct n. - change (0 < φ (2) < 2 ^ Z.of_nat 1)%Z with (0 < φ (2) < 2)%Z in Hi. lia. - case n; reflexivity. } rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq. change (to_Z 2) with 2%Z; intro Hi2. rewrite (IHn (i >> 1)). { rewrite (IHn (i >> 1)). { f_equal. apply iter_int63_aux_comm. replace (i >> 1 - 1) with ((i - 1) >> 1). { apply pow2_lsr. rewrite to_Z_sub_1_0; lia. } rewrite sub1_lsr, Hibit; [ reflexivity | ]. rewrite <- to_Z_eq, to_Z_0; lia. } split. { rewrite lsr_spec, to_Z_1. change (2 ^ 1)%Z with 2%Z. apply Z.div_str_pos; lia. } apply pow2_lsr; lia. } split. { rewrite lsr_spec, to_Z_1. change (2 ^ 1)%Z with 2%Z. apply Z.div_str_pos; lia. } apply pow2_lsr; lia. } symmetry. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_sub_1_0, to_Z_0; lia. } rewrite <- to_Z_eq, to_Z_0; lia. } symmetry. rewrite <- not_true_iff_false, eqb_spec, <- to_Z_eq, to_Z_0; lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz