Small changes suggested by Andres

mit-plv · Nov 21, 2022 · 846c5d4 · 846c5d4
1 parent 7db96f0
commit 846c5d4
Show file tree

Hide file tree

Showing 3 changed files with 123 additions and 130 deletions.
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
@@ -7,6 +7,7 @@ Require Import Crypto.Arithmetic.ModularArithmeticTheorems.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.ListUtil.
+Import Crypto.Util.ListUtil.Reifiable.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Decidable.Bool2Prop.
@@ -527,56 +528,55 @@ Module Associational.
   Qed.
 
   Definition value_at_weight (a : list (Z * Z)) (d : Z) :=
-    fold_right (fun p sum => if (d =? fst p) then (sum + snd p) else sum) 0 a.
+    fold_right Z.add 0 (map snd (filter (fun p => fst p =? d) a)).
 
-  Lemma value_at_weight_works a d : d * (value_at_weight a d) = Associational.eval (filter (fun p => d =? fst p) a).
+  Lemma value_at_weight_works a d : d * (value_at_weight a d) = Associational.eval (filter (fun p => fst p =? d) a).
   Proof.
     induction a as [| a0 a' IHa'].
-    - 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. lia.
+    - cbv [Associational.eval value_at_weight]. simpl. lia.
+    - cbv [value_at_weight]. simpl. destruct (fst a0 =? d) eqn:E.
+      + rewrite Associational.eval_cons. simpl. rewrite <- IHa'. cbv [value_at_weight]. lia.
       + apply IHa'.
   Qed.
 
-  Definition firsts (a : list (Z*Z)) :=
-    map (fun p => fst p) a.
-
-  Lemma not_in_value_0 a d : ~ In d (firsts a) -> value_at_weight a d = 0.
+  Lemma not_in_value_0 a d : ~ In d (map fst a) -> value_at_weight a d = 0.
   Proof.
     intros H. induction a as [| x a' IHa'].
     - reflexivity.
-    - simpl. destruct (d =? fst x) eqn:E.
-      + exfalso. apply H. simpl. left. apply Z.eqb_eq in E. symmetry. apply E.
+    - cbv [value_at_weight]. simpl. destruct (fst x =? d) eqn:E.
+      + exfalso. apply H. simpl. lia.
       + apply IHa'. intros H'. apply H. simpl. right. apply H'.
   Qed.
 
   Definition dedup_weights a :=
-    map (fun d => (d, value_at_weight a d)) (just_once Z.eqb (firsts a)).
+    map (fun d => (d, value_at_weight a d)) (nodupb Z.eqb (map fst a)).
 
-  Lemma map_eq (x y : Z) l a : ~ In x l ->
-    map (fun d : Z => (d, value_at_weight a d)) l = map (fun d : Z => (d, if d =? x then (value_at_weight a d + y) else value_at_weight a d)) l.
+  Lemma funs_same (l : list Z) (a0 : Z*Z) (a' : list (Z*Z)) :
+  ~ In (fst a0) l ->
+  forall d, In d l ->
+  (fun d : Z => (d, value_at_weight (a0 :: a') d)) d = (fun d => (d, value_at_weight a' d)) d.
   Proof.
-    intros H. induction l as [|x' l' IHl'].
+    intros H d H'. simpl. f_equal. cbv [value_at_weight]. simpl. destruct (fst a0 =? d) eqn:E.
+    - exfalso. rewrite Z.eqb_eq in E. subst. apply (H H').
     - reflexivity.
-    - simpl. destruct (x' =? x) eqn:E.
-      + exfalso. apply H. apply Z.eqb_eq in E. rewrite E. simpl. left. reflexivity.
-      + rewrite IHl'.
-        -- reflexivity.
-        -- intros H'. apply H. simpl. right. apply H'.
   Qed.
 
-  Theorem eval_dedup_weights a : Associational.eval (dedup_weights a) = Associational.eval a.
+  Lemma eval_dedup_weights a : Associational.eval (dedup_weights a) = Associational.eval a.
   Proof.
     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. 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). lia.
+    - cbv [dedup_weights]. simpl. destruct (existsb (Z.eqb (fst a0)) (nodupb Z.eqb (map fst a'))) eqn:E.
+      + apply (existsb_eqb_true_iff Z.eqb Z.eqb_eq) in E. rewrite <- (nodupb_in_iff Z.eqb Z.eqb_eq) in E.
+        apply (nodupb_split Z.eqb Z.eqb_eq) in E. destruct E as [l1 [l2 [H1 [H2 H3] ] ] ]. rewrite H1.
+        repeat rewrite map_app. rewrite (map_ext_in _ _ l1 (funs_same l1 a0 a' H2)).
+        rewrite (map_ext_in _ _ l2 (funs_same l2 a0 a' H3)). repeat rewrite Associational.eval_app. simpl.
+        repeat rewrite Associational.eval_cons. simpl. rewrite <- IHa'. simpl. rewrite Associational.eval_nil. 
+        cbv [dedup_weights]. rewrite H1. repeat rewrite map_app. repeat rewrite Associational.eval_app.
+        cbv [value_at_weight]. simpl. rewrite Z.eqb_refl. simpl. cbv [Associational.eval]. simpl. lia.
+      + simpl. apply (existsb_eqb_false_iff Z.eqb Z.eqb_eq) in E. rewrite (map_ext_in _ _ _ (funs_same _ _ _ E)).
+        repeat rewrite Associational.eval_cons. simpl. rewrite <- IHa'. cbv [dedup_weights]. f_equal. f_equal.
+        rewrite <- (nodupb_in_iff Z.eqb Z.eqb_eq) in E. cbv [value_at_weight]. simpl. rewrite Z.eqb_refl.
+        apply not_in_value_0 in E. cbv [value_at_weight] in E. simpl. rewrite E. lia.
   Qed.
 
   Section Carries.
@@ -605,29 +605,28 @@ Module Associational.
     Proof using Type*. cbv [carry]; induction p; push; nsatz. Qed.
     Hint Rewrite eval_carry using auto : push_eval.
 
-  (* 'carrying down', aka borrowing *)
-  Definition carryterm_down (w fw:Z) (t:Z * Z) :=
+  Definition borrowterm (w fw:Z) (t:Z * Z) :=
       let quot := w / fw in
       if (Z.eqb (fst t) w)
         then [(quot, snd t * fw)]
         else [t].
 
-  Lemma eval_carryterm_down w fw (t:Z * Z) (fw_nz:fw<>0) (w_fw:w mod fw = 0) :
-        Associational.eval (carryterm_down w fw t) = Associational.eval [t].
+  Lemma eval_borrowterm w fw (t:Z * Z) (fw_nz:fw<>0) (w_fw:w mod fw = 0) :
+        Associational.eval (borrowterm w fw t) = Associational.eval [t].
   Proof using Type*.
-    cbv [carryterm_down Let_In]; break_match; push; [|trivial].
+    cbv [borrowterm Let_In]; break_match; push; [|trivial].
     pose proof (Z.div_mod (snd t) fw fw_nz).
     rewrite Z.eqb_eq in *.
     ring_simplify. rewrite Z.mul_comm. rewrite Z.mul_assoc. rewrite <- Z_div_exact_full_2; lia.
   Qed.
 
-  Definition carry_down (w fw:Z) (p:list (Z*Z)) :=
-    flat_map (carryterm_down w fw) p.
+  Definition borrow (w fw:Z) (p:list (Z*Z)) :=
+    flat_map (borrowterm w fw) p.
 
-  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.
+  Lemma eval_borrow w fw p (fw_nz:fw<>0) (w_fw:w mod fw = 0):
+        Associational.eval (borrow w fw p) = Associational.eval p.
   Proof using Type*.
-    cbv [carry_down carryterm_down]. induction p as [| a p' IHp'].
+    cbv [borrow borrowterm]. 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.

diff --git a/src/Arithmetic/DettmanMultiplication.v b/src/Arithmetic/DettmanMultiplication.v
@@ -8,7 +8,6 @@ Import Associational Positional.
 Import ListNotations. Local Open Scope Z_scope.
 
 Local Coercion Z.of_nat : nat >-> Z.
-Local Coercion Z.pos : positive >-> Z.
 
 Section __.
 
@@ -94,21 +93,18 @@ Proof.
   - apply weight_nz.
 Qed.
 
-Definition from_n_to_one n :=
-  fold_right (fun (x :nat) l' => (length l' + 1) :: l') [] (repeat 0 n).
+Definition loop start :=
+  fold_right loop_body start (rev (seq 1 (limbs - 2 - 1))).
 
-Definition loop' start :=
-  fold_right loop_body start (from_n_to_one (limbs - 2 - 1)).
-
-Lemma eval_loop' start :
-  ((Associational.eval (loop' start)) mod (s - c) = (Associational.eval start) mod (s - c))%Z.
+Lemma eval_loop start :
+  ((Associational.eval (loop start)) mod (s - c) = (Associational.eval start) mod (s - c))%Z.
 Proof.
-  cbv [loop']. induction (from_n_to_one (limbs - 2 - 1)) as [| i l' IHl'].
+  cbv [loop]. induction (rev (seq 1 (limbs - 2 - 1))) as [| i l' IHl'].
   - reflexivity.
   - simpl. rewrite eval_loop_body. apply IHl'.
 Qed.
 
-Definition mulmod_general a b :=
+Definition mulmod a b :=
   let l := limbs in
   let a_assoc := Positional.to_associational weight limbs a in
   let b_assoc := Positional.to_associational weight limbs b in
@@ -121,24 +117,24 @@ Definition mulmod_general a b :=
   let r5 := carry' (weight (l - 1)) (weight 1) r4 in
   let r6 := carry' (weight (l - 1)) (Z.div s (weight (l - 1))) r5 in
   let r7 := carry' (weight l) (weight 1) r6 in
-  let r8 := carry_down (weight l) (weight l / s) r7 in
+  let r8 := borrow (weight l) (weight l / s) r7 in
   let r8' := dedup_weights r8 in
   let r9 := reduce' s s s c r8' in
   let r10 := carry' (weight 0) (weight 1) r9 in
-  let r11 := loop' r10 in
+  let r11 := loop r10 in
   let r12 := reduce' s (weight (2 * l - 2)) (weight l) c r11 in
   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.
+Hint Rewrite Positional.eval_from_associational Positional.eval_to_associational eval_borrow eval_loop: push_eval.
 
 Local Open Scope Z_scope.
 
-Theorem eval_mulmod_general a b :
+Theorem eval_mulmod 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).
+  (Positional.eval weight limbs (mulmod a b)) mod (s - c).
 Proof.
-  cbv [mulmod_general carry' reduce']. autorewrite with push_eval. reflexivity.
+  cbv [mulmod carry' reduce']. autorewrite with push_eval. reflexivity.
   all:
       cbv [weight s base];
       try apply weight_nz;

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
@@ -3421,86 +3421,84 @@ Lemma fold_left_rev_higher_order A B f a ls
     = fold_left (fun acc x a => acc (f a x)) ls id a.
 Proof. symmetry; apply fold_left_higher_order. Qed.
 
-(* This section is here because the equivalent standard library functions fail to be "reified by unfolding". *)
+(* This module is here because the equivalent standard library functions fail to be "reified by unfolding". *)
 
-Section Reifiable.
+Module Reifiable.
+  Section __.
+    Context {X : Type}
+            (eqb : X -> X -> bool)
+            (eqb_eq : forall x1 x2, eqb x1 x2 = true <-> x1 = x2).
 
-Context {X : Type}
-        (eqb : X -> X -> bool)
-        (eqb_eq : forall x1 x2, eqb x1 x2 = true <-> x1 = x2).
+    Definition existsb (f : X -> bool) (l : list X) : bool :=
+      fold_right (fun x found => orb (f x)found) false l.
 
-Definition is_in (x : X) (l : list X) :=
-  fold_right (fun x' found => orb (eqb x' x) found) false l.
-
-Lemma is_in_true_iff : forall x l, is_in x l = true <-> In x l.
-  intros. induction l as [ | x' l'].
-  - split; intros H.
-    + discriminate H.
-    + destruct H.
-  - split; intros H.
-    + simpl in *. destruct (eqb x' x) eqn:E.
-      -- apply eqb_eq in E. left. apply E.
-      -- simpl in H. right. rewrite <- IHl'. apply H.
-    + destruct H as [H | H].
-      -- simpl. apply eqb_eq in H. rewrite H. reflexivity.
-      -- simpl. rewrite <- IHl' in H. rewrite H. destruct (eqb x' x); reflexivity.
-Qed.
+    Lemma reifiable_existsb_is_existsb : forall (f : X -> bool) (l : list X),
+      existsb f l = List.existsb f l.
+    Proof. reflexivity. Qed.
 
-Lemma is_in_false_iff : forall x l, is_in x l = false <-> ~ In x l.
-Proof.
-  intros. rewrite <- is_in_true_iff. split.
-  - intros H. rewrite H. auto.
-  - intros H. destruct (is_in x l).
-    + exfalso. apply H. reflexivity.
-    + reflexivity.
-Qed.
+    Lemma existsb_eqb_true_iff : forall x l, existsb (eqb x) l = true <-> In x l.
+      intros x l. rewrite reifiable_existsb_is_existsb. rewrite existsb_exists. split.
+      - intros [x0 [H1 H2]]. rewrite eqb_eq in H2. subst. assumption.
+      - intros H. exists x. split.
+        + assumption.
+        + apply eqb_eq. reflexivity.
+    Qed.
 
-Definition just_once (l : list X) :=
-  fold_right (fun x l' => if (is_in x l') then l' else (x :: l')) [] l.
+    Lemma existsb_eqb_false_iff : forall x l, existsb (eqb x) l = false <-> ~In x l.
+    Proof.
+      intros. rewrite <- existsb_eqb_true_iff. split.
+      - intros H. rewrite H. auto.
+      - intros H. destruct (existsb (eqb x) l).
+        + exfalso. apply H. reflexivity.
+        + reflexivity.
+    Qed.
 
-Lemma just_once_in_iff (x : X) (l : list X) : In x l <-> In x (just_once l).
-Proof.
-  induction l as [|x' l' IHl'].
-  - reflexivity.
-  - simpl. destruct (is_in x' (just_once l')) eqn:E.
-    + rewrite is_in_true_iff in E. split.
-      -- intros [H|H].
-        ++ rewrite <- H. apply E.
-        ++ rewrite <- IHl'. apply H.
-      -- intros H. right. rewrite IHl'. apply H.
-    + rewrite is_in_false_iff in E. split.
-      -- intros [H|H].
-        ++ rewrite H. simpl. left. reflexivity.
-        ++ simpl. right. rewrite <- IHl'. apply H.
-      -- simpl. intros [H|H].
-        ++ left. apply H.
-        ++ right. rewrite IHl'. apply H.
-Qed.
-
-Lemma just_once_split (x : X) (l : list X) : In x l ->
-  exists l1 l2, just_once l = l1 ++ [x] ++ l2 /\ ~ In x l1 /\ ~ In x l2.
-Proof.
-  intros H. induction l as [| x' l'].
-  - simpl in H. destruct H.
-  - simpl in H. destruct H as [H|H].
-    + rewrite H. clear H. simpl. destruct (is_in x (just_once l')) eqn:E.
-      -- rewrite is_in_true_iff in E. rewrite <- just_once_in_iff in E.
-         apply IHl' in E. apply E.
-      -- exists []. exists (just_once l'). split.
-        ++ rewrite app_nil_l. reflexivity.
-        ++ split.
-          --- auto.
-          --- rewrite <- is_in_false_iff. apply E.
-    + apply IHl' in H. clear IHl'. simpl. destruct (is_in x' (just_once l')) eqn:E.
-      -- apply H.
-      -- destruct H as [l1 [l2 [H1 [H2 H3] ] ] ]. exists (x' :: l1). exists l2. split.
-        ++ rewrite H1. reflexivity.
-        ++ split.
-          --- simpl. intros [H|H].
-            +++ rewrite H in *. rewrite H1 in E. apply is_in_false_iff in E. apply E.
-                repeat rewrite in_app_iff. right. left. simpl. left. reflexivity.
-            +++ apply H2. apply H.
-          --- apply H3.
-Qed.
+    Definition nodupb (l : list X) :=
+      fold_right (fun x l' => if (existsb (eqb x) l') then l' else (x :: l')) [] l.
+
+    Lemma nodupb_in_iff (x : X) (l : list X) : In x l <-> In x (nodupb l).
+    Proof.
+      induction l as [|x' l' IHl'].
+      - reflexivity.
+      - simpl. destruct (existsb (eqb x') (nodupb l')) eqn:E.
+        + rewrite existsb_eqb_true_iff in E. split.
+          -- intros [H|H].
+            ++ rewrite <- H. apply E.
+            ++ rewrite <- IHl'. apply H.
+          -- intros H. right. rewrite IHl'. apply H.
+        + rewrite existsb_eqb_false_iff in E. split.
+          -- intros [H|H].
+            ++ rewrite H. simpl. left. reflexivity.
+            ++ simpl. right. rewrite <- IHl'. apply H.
+          -- simpl. intros [H|H].
+            ++ left. apply H.
+            ++ right. rewrite IHl'. apply H.
+    Qed.
 
+    Lemma nodupb_split (x : X) (l : list X) : In x l ->
+      exists l1 l2, nodupb l = l1 ++ [x] ++ l2 /\ ~ In x l1 /\ ~ In x l2.
+    Proof.
+      intros H. induction l as [| x' l'].
+      - simpl in H. destruct H.
+      - simpl in H. destruct H as [H|H].
+        + rewrite H. clear H. simpl. destruct (existsb (eqb x) (nodupb l')) eqn:E. 
+          -- rewrite existsb_eqb_true_iff in E. rewrite <- nodupb_in_iff in E.
+             apply IHl' in E. apply E.
+          -- exists []. exists (nodupb l'). split.
+            ++ rewrite app_nil_l. reflexivity.
+            ++ split.
+              --- auto.
+              --- rewrite <- existsb_eqb_false_iff. apply E.
+        + apply IHl' in H. clear IHl'. simpl. destruct (existsb (eqb x') (nodupb l')) eqn:E.
+          -- apply H.
+          -- destruct H as [l1 [l2 [H1 [H2 H3] ] ] ]. exists (x' :: l1). exists l2. split.
+            ++ rewrite H1. reflexivity.
+            ++ split.
+              --- simpl. intros [H|H].
+                +++ rewrite H in *. rewrite H1 in E. apply existsb_eqb_false_iff in E. apply E.
+                    repeat rewrite in_app_iff. right. left. simpl. left. reflexivity.
+                +++ apply H2. apply H.
+              --- apply H3.
+    Qed.
+  End __.
 End Reifiable.