From 1de1e5111e6056efdb31a86b054862f9f8e52240 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Mon, 13 Aug 2018 15:25:51 -0400
Subject: Add some util lemmas

---
 src/Util/OptionList.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

(limited to 'src/Util/OptionList.v')

diff --git a/src/Util/OptionList.v b/src/Util/OptionList.v
index 2f6d8a2ce..c2157346e 100644
--- a/src/Util/OptionList.v
+++ b/src/Util/OptionList.v
@@ -1,3 +1,4 @@
+Require Import Coq.Lists.List.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Notations.
 
@@ -31,3 +32,35 @@ Module Option.
 End Option.
 
 Export Option.List.Notations.
+
+Lemma fold_right_option_seq A B f init ls v
+  : List.fold_right (fun x y => x <- x; y <- y; Some (f x y))%option (Some init) ls = Some v
+    <-> exists ls', List.map (@Some _) ls' = ls
+                    /\ @List.fold_right A B f init ls' = v.
+Proof.
+  revert v; induction ls as [|x xs IHxs]; cbn; intros;
+    repeat first [ apply conj
+                 | progress intros
+                 | progress subst
+                 | progress cbn in *
+                 | solve [ try (exists nil); cbn; auto ]
+                 | congruence
+                 | match goal with
+                   | [ x : option _ |- _ ] => destruct x
+                   | [ H : ex _ |- _ ] => destruct H
+                   | [ H : and _ _ |- _ ] => destruct H
+                   | [ H : Some _ = Some _ |- _ ] => inversion H; clear H
+                   | [ H : cons _ _ = cons _ _ |- _ ] => inversion H; clear H
+                   | [ H : List.map _ ?x = nil |- _ ] => is_var x; destruct x
+                   | [ H : List.map _ ?x = cons _ _ |- _ ] => is_var x; destruct x
+                   | [ H : forall v, iff _ _ |- _ ]
+                     => pose proof (fun v => proj1 (H v)); pose proof (fun v => proj2 (H v)); clear H
+                   | [ |- iff _ _ ] => split
+                   | [ |- context[Option.bind ?x ?y] ] => destruct x eqn:?
+                   | [ H : context[Option.bind ?x ?y] |- _ ] => destruct x eqn:?
+                   | [ H : forall v, _ = _ -> _ |- _ ] => specialize (H _ ltac:(eassumption || reflexivity))
+                   | [ H : forall v, (exists y, _ = _ /\ _ = _) -> _ |- _ ] => specialize (H _ ltac:(eexists; split; reflexivity))
+                   | [ |- exists ls', List.map ?f ls' = (?f ?x :: List.map ?f ?xs)%list /\ _ ]
+                     => exists (cons x xs)
+                   end ].
+Qed.
-- 
cgit v1.2.3