From 03e72996b86ddfdfd9c6e9f44ecd2cfa6e9aed8a Mon Sep 17 00:00:00 2001 From: Avi Shinnar Date: Tue, 16 Jan 2024 09:58:36 -0500 Subject: [PATCH] finish adjustment to row_sum_rot_pow_is_really_binned Signed-off-by: Avi Shinnar --- coq/FHE/zp_prim_root.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/coq/FHE/zp_prim_root.v b/coq/FHE/zp_prim_root.v index 5d0d13c8..e6e7ba60 100644 --- a/coq/FHE/zp_prim_root.v +++ b/coq/FHE/zp_prim_root.v @@ -3000,17 +3000,19 @@ Section add_self_pow. is_partitioned_in_same_bins_by_m_to (row_sum_rot_pow v) 0. Proof. rewrite /row_sum_rot_pow. - suff {v}: forall n', forall v : 'rV_(2 ^ n), + suff {v}: forall n', n' <= n -> forall v : 'rV_(2 ^ n), is_partitioned_in_same_bins_by_m_to v n' -> is_partitioned_in_same_bins_by_m_to (row_sum_rot_pow_rec v n') 0. { apply. - apply is_partitioned_in_same_bins_by_m_to0. + - apply leqnn. + - apply is_partitioned_in_same_bins_by_m_to0. } - induction n' => //= v. + induction n' => //= n'l v. move/row_sum_rot_pow_rec_step_narrows_bins => HH. apply IHn'. - apply HH. - Admitted. + - by apply ltnW. + - by apply HH. + Qed. Lemma row_sum_rot_pow_is_summed {n} (v:'rV[G]_(2^n)) : \sum_(i < 2^n) v 0 i = (row_sum_rot_pow v) 0 (Ordinal (expn_2_pos n)).