Add Option.{lift,map,combine}, List.Option.lift

These will be useful for extending the AST with `option` types.

13 files changed, 36 insertions, 11 deletions

diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index a6a2d8d6b..3d9f03f79 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -23,6 +23,7 @@ Require Import Crypto.LanguageInversion.
 Require Import Crypto.LanguageWf.
 Require Import Crypto.UnderLetsProofs.
 Require Import Crypto.AbstractInterpretation.
+Import Coq.Lists.List.
 
 Module Compilers.
   Import Language.Compilers.
diff --git a/src/Arithmetic.v b/src/Arithmetic.v
index dc4c5031b..5f4b6de50 100644
--- a/src/Arithmetic.v
+++ b/src/Arithmetic.v
@@ -54,7 +54,7 @@ Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.Tactics.SetEvars.
-Import ListNotations. Local Open Scope Z_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope Z_scope.
 
 Module Associational.
   Definition eval (p:list (Z*Z)) : Z :=
diff --git a/src/CStringification.v b/src/CStringification.v
index b50957dcd..0cdf55c99 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -18,7 +18,7 @@ Require Import Crypto.Language.
 Require Import Crypto.AbstractInterpretation.
 Require Import Crypto.Util.Bool.Equality.
 Require Import Crypto.Util.Notations.
-Import ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope.
 
 Module Compilers.
   Local Set Boolean Equality Schemes.
diff --git a/src/Language.v b/src/Language.v
index 6eac36949..efcc16b63 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -1237,7 +1237,7 @@ Module Compilers.
         | @repeat ?A
           => let rA := base.reify A in
              then_tac (@ident.List_repeat rA)
-        | @combine ?A ?B
+        | @List.combine ?A ?B
           => let rA := base.reify A in
              let rB := base.reify B in
              then_tac (@ident.List_combine rA rB)
diff --git a/src/LanguageWf.v b/src/LanguageWf.v
index 1aa0a775a..7f6bd5e18 100644
--- a/src/LanguageWf.v
+++ b/src/LanguageWf.v
@@ -31,7 +31,7 @@ Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Notations.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 
 Import EqNotations.
 Module Compilers.
diff --git a/src/Primitives/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
index d867a62df..b7f4acd9b 100644
--- a/src/Primitives/EdDSARepChange.v
+++ b/src/Primitives/EdDSARepChange.v
@@ -56,7 +56,7 @@ Section EdDSA.
   Context {Edec:word b-> option E}   {eq_enc_E_iff: forall P_ P, Eenc P = P_ <-> option_eq Eeq (Edec P_) (Some P)}.
   Context {Sdec:word b-> option (F l)} {eq_enc_S_iff: forall n_ n, Senc n = n_ <-> Sdec n_ = Some n}.
 
-  Local Infix "++" := combine.
+  Local Infix "++" := Word.combine.
   Definition verify'_sig : { verify | forall mlen (message:word mlen) (pk:word b) (sig:word (b+b)),
       verify mlen message pk sig = true <-> valid message pk sig }.
   Proof.
@@ -231,7 +231,7 @@ Section EdDSA.
       dlet r := SRepDecModL (H _ (p ++ msg)) in
       dlet R := SRepERepMul r ErepB in
       dlet S := SRepAdd r (SRepMul (SRepDecModL (H _ (ERepEnc R ++ pk ++ msg))) s) in
-      ERepEnc R ++ SRepEnc S. 
+      ERepEnc R ++ SRepEnc S.
 
     Lemma Z_l_nonzero : Z.pos l <> 0%Z. discriminate. Qed.
 
diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v
index e4ac4afda..0587aec51 100644
--- a/src/RewriterProofs.v
+++ b/src/RewriterProofs.v
@@ -27,7 +27,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Decidable.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v
index 9deb2ec6d..585ba2387 100644
--- a/src/RewriterRulesGood.v
+++ b/src/RewriterRulesGood.v
@@ -24,7 +24,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Decidable.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index 2b18d01d0..f425a769b 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -34,7 +34,7 @@ Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Decidable.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/RewriterWf2.v b/src/RewriterWf2.v
index 13238361b..96911abe5 100644
--- a/src/RewriterWf2.v
+++ b/src/RewriterWf2.v
@@ -25,7 +25,7 @@ Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.Decidable.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 Local Open Scope Z_scope.
 
 Import EqNotations.
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v
index 787fdb7c4..884b6687a 100644
--- a/src/UnderLetsProofs.v
+++ b/src/UnderLetsProofs.v
@@ -12,7 +12,7 @@ Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Tactics.SpecializeBy.
-Import ListNotations. Local Open Scope list_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope list_scope.
 
 Import EqNotations.
 Module Compilers.
diff --git a/src/Util/Option.v b/src/Util/Option.v
index 2c6549cb6..2eae8d0e5 100644
--- a/src/Util/Option.v
+++ b/src/Util/Option.v
@@ -16,6 +16,19 @@ Definition option_beq_hetero {A B} (AB_beq : A -> B -> bool) (x : option A) (y :
        => false
      end.
 
+(** In general, [lift : M (option A) -> option (M A)].  This is a bit
+    confusing for [option] because [M = option].  We want to return
+    [None] if the thing contained in the [M (option A)] is [None], and
+    say [Some] otherwise. *)
+Definition lift {A} (x : option (option A)) : option (option A)
+  := match x with
+     | Some None => None (* the contained thing is bad/not present *)
+     | Some (Some x) => Some (Some x)
+     | None => Some None
+     end.
+
+Notation map := option_map (only parsing). (* so we have [Option.map] *)
+
 Definition bind {A B} (v : option A) (f : A -> option B) : option B
   := match v with
      | Some v => f v
@@ -45,6 +58,12 @@ Module Export Notations.
 End Notations.
 Local Open Scope option_scope.
 
+Definition combine {A B} (x : option A) (y : option B) : option (A * B)
+  := match x, y with
+     | Some x, Some y => Some (x, y)
+     | _, _ => None
+     end.
+
 Section Relations.
   Definition option_eq {A B} eq (x : option A) (y : option B) :=
     match x with
diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
index c2157346e..4b88dd9a3 100644
--- a/src/Util/OptionList.v
+++ b/src/Util/OptionList.v
@@ -25,6 +25,11 @@ Module Option.
          | x :: xs => (x <- x; @bind_list A B xs (fun xs => f (x :: xs)))
          end%option%list.
 
+    Definition lift {A} (ls : list (option A)) : option (list A)
+      := fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))%option
+                    (Some nil)
+                    ls.
+
     Module Export Notations.
       Notation "A <-- X ; B" := (bind_list X (fun A => B%option)) : option_scope.
     End Notations.