Made things cleaner and more concise based on Jason's suggestions.

mit-plv · Nov 13, 2022 · b96724a · b96724a
1 parent adc6939
commit b96724a
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 80 deletions.
diff --git 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
@@ -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 __.