From ed165980926ae68f03be4843ded944990e171d7a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Dec 2023 09:32:49 -0800 Subject: [PATCH 1/2] Add `Util.Option.{bind2,map2}` To replace `RingMicromega.map_option2` in https://github.com/mit-plv/fiat-crypto/pull/1609 --- src/PushButtonSynthesis/UnsaturatedSolinas.v | 2 +- src/UnsaturatedSolinasHeuristics.v | 6 +++--- src/UnsaturatedSolinasHeuristics/Tests.v | 2 +- src/Util/Notations.v | 7 +++++++ src/Util/Option.v | 18 ++++++++++++++++++ 5 files changed, 30 insertions(+), 5 deletions(-) diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 64d033a31c..5f53f965ed 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/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. diff --git a/src/UnsaturatedSolinasHeuristics.v b/src/UnsaturatedSolinasHeuristics.v index 5ae74e6ecc..6cea791bc0 100644 --- a/src/UnsaturatedSolinasHeuristics.v +++ b/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. diff --git a/src/UnsaturatedSolinasHeuristics/Tests.v b/src/UnsaturatedSolinasHeuristics/Tests.v index fcdd57fadb..4128d6b0b8 100644 --- a/src/UnsaturatedSolinasHeuristics/Tests.v +++ b/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), diff --git a/src/Util/Notations.v b/src/Util/Notations.v index e5cb821cd7..384dad1eed 100644 --- a/src/Util/Notations.v +++ b/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 ']'"). diff --git a/src/Util/Option.v b/src/Util/Option.v index ad296d6c5e..7e0707d1ba 100644 --- a/src/Util/Option.v +++ 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. From 0d06cdf73a99b05961dbe86c3c1164e0e5105de7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Dec 2023 14:13:41 -0800 Subject: [PATCH 2/2] Rename ListUtil.map2 => ListUtil.List.map2 --- src/Util/ListUtil.v | 28 ++++++++++++++-------------- src/Util/Tuple.v | 4 ++-- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 3159a193a6..dc79bac89e 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -337,6 +337,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] @@ -371,19 +384,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 @@ -3481,7 +3481,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. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 925a2be047..8cc4c1e09f 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -315,7 +315,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). @@ -388,7 +388,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.