Add Util.Option.bind2 (mit-plv#1768)

* Add `Util.Option.{bind2,map2}`

To replace `RingMicromega.map_option2` in
mit-plv#1609

* Rename ListUtil.map2 => ListUtil.List.map2

src/PushButtonSynthesis/UnsaturatedSolinas.v

@@ -139,7 +139,7 @@ Section __.
   Definition m_enc_min : list Z :=
     let wt := weight (Qnum limbwidth) (Qden limbwidth) in
     let fw := List.map (fun i => wt (S i) / wt i) (seq 0 n) in
-    let m_enc_min := map2 Z.sub tight_upperbounds fw in
+    let m_enc_min := List.map2 Z.sub tight_upperbounds fw in
     if List.forallb (Z.eqb 0) m_enc_min
     then set_nth (n-1) 1 m_enc_min
     else m_enc_min.

src/UnsaturatedSolinasHeuristics.v

@@ -60,7 +60,7 @@ Section encode_distributed.
   Hint Rewrite length_encode_distributed : distr_length.
   Lemma nth_default_encode_distributed_bounded_eq'
         (** We add an extra hypothesis that is too bulky to prove *)
-        (Hadd : forall x y, length x = n -> length y = n -> add weight n x y = map2 Z.add x y)
+        (Hadd : forall x y, length x = n -> length y = n -> add weight n x y = List.map2 Z.add x y)
         minvalues x i d
     : nth_default d (encode_distributed minvalues x) i
       = if Decidable.dec (i < n)%nat
@@ -80,7 +80,7 @@ Section encode_distributed.
   Qed.
   Lemma nth_default_encode_distributed_bounded'
         (** We add an extra hypothesis that is too bulky to prove *)
-        (Hadd : forall x y, length x = n -> length y = n -> add weight n x y = map2 Z.add x y)
+        (Hadd : forall x y, length x = n -> length y = n -> add weight n x y = List.map2 Z.add x y)
         minvalues x i d' d
         (Hmin : (i < length minvalues)%nat)
         (Hn : (i < n)%nat)
@@ -345,7 +345,7 @@ else:
   (*
   Lemma nth_default_balance_bounded' i d' d
         (** We add an extra hypothesis that is too bulky to prove *)
-        (Hadd : forall x y, length x = n -> length y = n -> Positional.add weight n x y = map2 Z.add x y)
+        (Hadd : forall x y, length x = n -> length y = n -> Positional.add weight n x y = List.map2 Z.add x y)
     : (i < n)%nat ->
       coef * nth_default d' tight_upperbounds i <= nth_default d balance i.
   Proof using wprops.

src/UnsaturatedSolinasHeuristics/Tests.v

@@ -168,7 +168,7 @@ Time Definition balances
                                    (fun n
                                     => let bal := @balance default_tight_upperbound_fraction n s c in
                                        let tub := @tight_upperbounds default_tight_upperbound_fraction n s c in
-                                       let dif := map2 Z.sub bal tub in
+                                       let dif := List.map2 Z.sub bal tub in
                                        ((bw, n),
                                         ("balance:                                        ",
                                          (let show_lvl_Z := PowersOfTwo.show_lvl_Z in show bal),

src/Util/ListUtil.v

@@ -338,6 +338,19 @@ Module Export List.
   (** new operations *)
   Definition enumerate {A} (ls : list A) : list (nat * A)
     := combine (seq 0 (length ls)) ls.
+
+  Section map2.
+    Context {A B C}
+      (f : A -> B -> C).
+
+    Fixpoint map2 (la : list A) (lb : list B) : list C :=
+      match la, lb with
+      | nil, _ => nil
+      | _, nil => nil
+      | a :: la', b :: lb'
+        => f a b :: map2 la' lb'
+      end.
+  End map2.
 End List.
 
 #[global]
@@ -372,19 +385,6 @@ Definition sum_firstn l n := fold_right Z.add 0%Z (firstn n l).
 
 Definition sum xs := sum_firstn xs (length xs).
 
-Section map2.
-  Context {A B C}
-          (f : A -> B -> C).
-
-  Fixpoint map2 (la : list A) (lb : list B) : list C :=
-    match la, lb with
-    | nil, _ => nil
-    | _, nil => nil
-    | a :: la', b :: lb'
-      => f a b :: map2 la' lb'
-    end.
-End map2.
-
 (* xs[n] := f xs[n] *)
 Fixpoint update_nth {T} n f (xs:list T) {struct n} :=
         match n with
@@ -3482,7 +3482,7 @@ Module Reifiable.
       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 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.

src/Util/Notations.v

@@ -124,6 +124,13 @@ Reserved Notation "A <-- X ; B" (at level 70, X at next level, right associativi
 Reserved Notation "A <--- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <---  X ; '/' B ']'").
 Reserved Notation "A <---- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <----  X ; '/' B ']'").
 Reserved Notation "A <----- X ; B" (at level 70, X at next level, right associativity, format "'[v' A  <-----  X ; '/' B ']'").
+(*
+Reserved Notation "A , A' <- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <-  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <-- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <--  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <--- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <---  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <---- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <----  X ,  X' ; '/' B ']'").
+Reserved Notation "A , A' <----- X , X' ; B" (at level 70, A' at next level, X at next level, X' at next level, right associativity, format "'[v' A ,  A'  <-----  X ,  X' ; '/' B ']'").
+*)
 Reserved Notation "A ;; B" (at level 70, right associativity, format "'[v' A ;; '/' B ']'").
 Reserved Notation "A ';;L' B" (at level 70, right associativity, format "'[v' A ';;L' '/' B ']'").
 Reserved Notation "A ';;R' B" (at level 70, right associativity, format "'[v' A ';;R' '/' B ']'").

src/Util/Option.v

@@ -29,12 +29,29 @@ Definition lift {A} (x : option (option A)) : option (option A)
 
 Notation map := option_map (only parsing). (* so we have [Option.map] *)
 
+Definition map2 {A B C} (f : A -> B -> C) (v1 : option A) (v2 : option B) : option C
+  := match v1, v2 with
+     | None, _
+     | _, None
+       => None
+     | Some v1, Some v2 => Some (f v1 v2)
+     end.
+
 Definition bind {A B} (v : option A) (f : A -> option B) : option B
   := match v with
      | Some v => f v
      | None => None
      end.
 
+Definition bind2 {A B C} (v1 : option A) (v2 : option B) (f : A -> B -> option C) : option C
+  := match v1, v2 with
+     | None, _
+     | _, None
+       => None
+     | Some x1, Some x2 => f x1 x2
+     end.
+Global Arguments bind2 {A B C} !v1 !v2 / f.
+
 Definition sequence {A} (v1 v2 : option A) : option A
   := match v1 with
      | Some v => Some v
@@ -59,6 +76,7 @@ Module Export Notations.
 
   Notation "'olet' x .. y <- X ; B" := (bind X (fun x => .. (fun y => B%option) .. )) : option_scope.
   Notation "A <- X ; B" := (bind X (fun A => B%option)) : option_scope.
+  (*Notation "A , A' <- X , X' ; B" := (bind2 X X' (fun A A' => B%option)) : option_scope.*)
   Infix ";;" := sequence : option_scope.
   Infix ";;;" := sequence_return : option_scope.
 End Notations.

src/Util/Tuple.v

@@ -314,7 +314,7 @@ Proof using Type.
 Qed.
 
 Lemma to_list_map2 {A B C n xs ys} (f : A -> B -> C)
-  : ListUtil.map2 f (@to_list A n xs) (@to_list B n ys) = @to_list C n (map2 f xs ys).
+  : List.map2 f (@to_list A n xs) (@to_list B n ys) = @to_list C n (map2 f xs ys).
 Proof using Type.
   tuples_from_lists; unfold map2, on_tuple2.
   repeat (rewrite to_list_from_list || rewrite from_list_to_list).
@@ -387,7 +387,7 @@ Proof using Type.
   destruct lxs as [|x' lxs']; [simpl in *; discriminate|].
   let lys := match goal with lxs : list B |- _ => lxs end in
   destruct lys as [|y' lys']; [simpl in *; discriminate|].
-  change ( f x y ::  ListUtil.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1))
+  change ( f x y ::  List.map2 f (to_list (S n) (from_list (S n) (x' :: lxs') x1))
     (to_list (S n) (from_list (S n) (y' :: lys') x0)) = f x y :: to_list (S n) (map2 f (from_list (S n) (x' :: lxs') x1) (from_list (S n) (y' :: lys') x0)) ).
   tuple_maps_to_list_maps.
   reflexivity.