diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 5c668adefd..1cdf46ef93 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -206,10 +206,10 @@ Module Associational. Proof. remember (Z_div_exact_full_2 _ _ fw_nz w_fw) as H2. clear HeqH2 fw_nz w_fw. - induction p as [|t p']. + induction p as [|t p' IHp']. - simpl. cbv [Associational.eval]. simpl. lia. - cbv [split_one]. simpl. destruct (fst t =? w) eqn:E. - + simpl in IHp'. remember (partition (fun t0 : Z * Z => fst t0 =? w) p') as thing. + + simpl in IHp'. remember (partition (fun t0 : Z * Z => fst t0 =? w) p') as thing; clear Heqthing. destruct thing as [thing1 thing2]. simpl. simpl in IHp'. repeat rewrite Associational.eval_cons. ring_simplify. simpl. apply Z.eqb_eq in E. rewrite E. rewrite <- H2. rewrite <- IHp'. ring. @@ -532,9 +532,9 @@ Module Associational. Lemma value_at_weight_works a d : d * (value_at_weight a d) = Associational.eval (filter (fun p => d =? fst p) a). Proof. induction a as [| a0 a' IHa']. - - cbv [Associational.eval]. simpl. ring. + - cbv [Associational.eval]. simpl. lia. - simpl. destruct (d =? fst a0) eqn:E. - + rewrite Associational.eval_cons. rewrite <- IHa'. apply Z.eqb_eq in E. rewrite E. ring. + + rewrite Associational.eval_cons. rewrite <- IHa'. apply Z.eqb_eq in E. rewrite E. lia. + apply IHa'. Qed. @@ -567,16 +567,16 @@ Module Associational. Theorem eval_dedup_weights a : Associational.eval (dedup_weights a) = Associational.eval a. Proof. - induction a as [| a0 a']. + induction a as [| a0 a' IHa']. - reflexivity. - cbv [dedup_weights]. simpl. destruct (is_in Z.eqb (fst a0) (just_once Z.eqb (firsts a'))) eqn:E. + apply (is_in_true_iff Z.eqb Z.eqb_eq) in E. rewrite <- (just_once_in_iff Z.eqb Z.eqb_eq) in E. apply (just_once_split Z.eqb Z.eqb_eq) in E. destruct E as [l1 [l2 [H1 [H2 H3] ] ] ]. rewrite H1. repeat rewrite map_app. rewrite <- (map_eq _ _ _ _ H2). rewrite <- (map_eq _ _ _ _ H3). repeat rewrite Associational.eval_app. simpl. rewrite Z.eqb_refl. repeat rewrite Associational.eval_cons. rewrite <- IHa'. simpl. rewrite Associational.eval_nil. cbv [dedup_weights]. rewrite H1. - repeat rewrite map_app. repeat rewrite Associational.eval_app. cbv [Associational.eval]. simpl. ring. + repeat rewrite map_app. repeat rewrite Associational.eval_app. cbv [Associational.eval]. simpl. lia. + simpl. rewrite Z.eqb_refl. apply (is_in_false_iff Z.eqb Z.eqb_eq) in E. rewrite <- (map_eq _ _ _ _ E). repeat rewrite Associational.eval_cons. - simpl. rewrite <- IHa'. cbv [dedup_weights]. f_equal. f_equal. rewrite <- (just_once_in_iff Z.eqb Z.eqb_eq) in E. rewrite (not_in_value_0 _ _ E). ring. + simpl. rewrite <- IHa'. cbv [dedup_weights]. f_equal. f_equal. rewrite <- (just_once_in_iff Z.eqb Z.eqb_eq) in E. rewrite (not_in_value_0 _ _ E). lia. Qed. Section Carries. @@ -627,11 +627,11 @@ Module Associational. Lemma eval_carry_down w fw p (fw_nz:fw<>0) (w_fw:w mod fw = 0): Associational.eval (carry_down w fw p) = Associational.eval p. Proof using Type*. - cbv [carry_down carryterm_down]. induction p. + cbv [carry_down carryterm_down]. induction p as [| a p' IHp']. - trivial. - push. destruct (fst a =? w) eqn:E. + rewrite Z.mul_comm. rewrite <- Z.mul_assoc. rewrite <- Z_div_exact_full_2; lia. - + rewrite IHp. lia. + + rewrite IHp'. lia. Qed. End Carries. diff --git a/src/Arithmetic/DettmanMultiplication.v b/src/Arithmetic/DettmanMultiplication.v index aa7f8cfca6..79991374b0 100644 --- a/src/Arithmetic/DettmanMultiplication.v +++ b/src/Arithmetic/DettmanMultiplication.v @@ -10,7 +10,7 @@ Import ListNotations. Local Open Scope Z_scope. Local Coercion Z.of_nat : nat >-> Z. Local Coercion Z.pos : positive >-> Z. -Section Stuff. +Section __. Context (e : nat) @@ -40,27 +40,20 @@ Lemma weight_0 : weight 0 = 1. Proof. reflexivity. Qed. Lemma weight_nz : forall i, weight i <> 0. -Proof. - intros i. cbv [weight]. apply Z.pow_nonzero. - - apply base_nz. - - lia. -Qed. +Proof. intros i. cbv [weight]. apply Z.pow_nonzero; lia. Qed. Lemma mod_is_zero : forall b (n m : nat), b <> 0 -> le n m -> (b ^ m) mod (b ^ n) = 0. - intros b n m H1 H2. induction H2. + intros b n m H1 H2. induction H2 as [|m' nlem' IHm']. - rewrite Z_mod_same_full. constructor. - - rewrite Nat2Z.inj_succ. cbv [Z.succ]. rewrite <- Pow.Z.pow_mul_base. - + rewrite Z.mul_mod_full. rewrite IHle. rewrite Z.mul_0_r. apply Z.mod_0_l. apply Z.pow_nonzero; lia. - + lia. + - rewrite Nat2Z.inj_succ. cbv [Z.succ]. rewrite <- Pow.Z.pow_mul_base by lia. + rewrite Z.mul_mod_full. rewrite IHm'. rewrite Z.mul_0_r. apply Z.mod_0_l. apply Z.pow_nonzero; lia. Qed. Lemma div_nz a b : b > 0 -> b <= a -> a / b <> 0. Proof. - intros H1 H2. assert (1 <= a / b). + intros H1 H2. assert (H: 1 <= a / b). - replace 1 with (b / b). - + apply Z_div_le. - -- apply H1. - -- apply H2. + + apply Z_div_le; assumption. + apply Z_div_same. apply H1. - symmetry. apply Z.lt_neq. apply Z.lt_le_trans with 1. + reflexivity. @@ -69,27 +62,11 @@ Qed. Lemma limbs_mod_s_0 : (weight limbs) mod s = 0. Proof. - cbv [weight base s]. rewrite <- Z.pow_mul_r. rewrite <- Nat2Z.inj_mul. apply mod_is_zero. - - lia. - - apply e_small. - - lia. - - lia. + cbv [weight base s]. rewrite <- Z.pow_mul_r by lia. rewrite <- Nat2Z.inj_mul. apply mod_is_zero; lia. Qed. Local Open Scope nat_scope. -(* want to start with i = 1 (up to l - 2, excludsive), so want to start with l_minus_2_minus_i = l - 2 - 1 *) -Fixpoint loop l weight s c l_minus_2_minus_i r0 := - match l_minus_2_minus_i with - | O => r0 - | S l_minus_2_minus_i' => - let i := (l - 2) - l_minus_2_minus_i in - let r1 := Associational.carry (weight (i + l)) (weight 1) r0 in - let r2 := reduce_one s (weight (i + l)) (weight l) c r1 in - let r3 := Associational.carry (weight i) (weight 1) r2 in - loop l weight s c l_minus_2_minus_i' r3 - end. - Definition reduce' x1 x2 x3 x4 x5 := dedup_weights (reduce_one x1 x2 x3 x4 x5). Definition carry' x1 x2 x3 := dedup_weights (Associational.carry x1 x2 x3). @@ -99,15 +76,13 @@ Definition loop_body i before := let after := carry' (weight i) (weight 1) middle2 in after. +Hint Rewrite eval_reduce_one Associational.eval_carry eval_dedup_weights: push_eval. + Lemma eval_loop_body i before : (Associational.eval (loop_body i before) mod (s - c) = Associational.eval before mod (s - c))%Z. Proof. - cbv [loop_body carry' reduce']. - repeat (try rewrite eval_reduce_one; - try rewrite Associational.eval_carry; - try rewrite eval_dedup_weights). - reflexivity. + cbv [loop_body carry' reduce']. autorewrite with push_eval. reflexivity. - apply weight_nz. - apply s_nz. - apply weight_nz. @@ -155,21 +130,15 @@ Definition mulmod_general a b := let r13 := carry' (weight (l - 2)) (weight 1) r12 in Positional.from_associational weight l r13. +Hint Rewrite Positional.eval_from_associational Positional.eval_to_associational eval_carry_down eval_loop': push_eval. + Local Open Scope Z_scope. Theorem eval_mulmod_general a b : (Positional.eval weight limbs a * Positional.eval weight limbs b) mod (s - c) = (Positional.eval weight limbs (mulmod_general a b)) mod (s - c). Proof. - cbv [mulmod_general carry' reduce']. - repeat (try rewrite Positional.eval_from_associational; - try rewrite Positional.eval_to_associational; - try rewrite Associational.eval_carry; - try rewrite eval_reduce_one; - try rewrite eval_carry_down; - try rewrite eval_dedup_weights; - try rewrite eval_loop'). - rewrite Associational.eval_mul. repeat rewrite Positional.eval_to_associational. reflexivity. + cbv [mulmod_general carry' reduce']. autorewrite with push_eval. reflexivity. all: cbv [weight s base]; try apply weight_nz; @@ -181,31 +150,12 @@ Proof. try apply mod_is_zero; try (remember limbs_gteq_3 as H; lia); try apply base_nz. - - apply div_nz. - + lia. - + rewrite <- Z.pow_mul_r. rewrite <- Nat2Z.inj_mul. rewrite <- Z.pow_le_mono_r_iff. - -- remember e_small as H. lia. - -- lia. - -- lia. - -- lia. - -- lia. - - apply div_nz. - + lia. - + rewrite <- Z.pow_mul_r. rewrite <- Nat2Z.inj_mul. rewrite <- Z.pow_le_mono_r_iff. - -- remember e_big as H. lia. - -- lia. - -- lia. - -- lia. - -- lia. - - repeat rewrite <- Z.pow_mul_r. rewrite <- Z.pow_sub_r. - + rewrite <- Nat2Z.inj_mul. rewrite <- Nat2Z.inj_sub. apply mod_is_zero. - -- lia. - -- lia. - -- apply e_small. - + lia. - + remember e_small as H. lia. - + lia. - + lia. + - apply div_nz; try lia. rewrite <- Z.pow_mul_r by lia. rewrite <- Nat2Z.inj_mul. + rewrite <- Z.pow_le_mono_r_iff by lia. lia. + - apply div_nz; try lia. rewrite <- Z.pow_mul_r by lia. rewrite <- Nat2Z.inj_mul. + rewrite <- Z.pow_le_mono_r_iff by lia. lia. + - repeat rewrite <- Z.pow_mul_r by lia. rewrite <- Z.pow_sub_r by lia. + rewrite <- Nat2Z.inj_mul. rewrite <- Nat2Z.inj_sub by lia. apply mod_is_zero; lia. Qed. -End Stuff. +End __.