Add some util lemmas

3 files changed, 72 insertions, 0 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 3d43bf509..8211d1ab7 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -2138,3 +2138,30 @@ Proof.
   all: edestruct lt_dec; try (exfalso; lia).
   all: reflexivity.
 Qed.
+
+Lemma nth_error_firstn A ls n i
+  : List.nth_error (@List.firstn A n ls) i = if lt_dec i n then List.nth_error ls i else None.
+Proof.
+  revert ls i; induction n, ls, i; cbn; try reflexivity; destruct lt_dec; try reflexivity; rewrite IHn.
+  all: destruct lt_dec; try reflexivity; omega.
+Qed.
+
+Lemma nth_error_rev A n ls : List.nth_error (@List.rev A ls) n = if lt_dec n (length ls) then List.nth_error ls (length ls - S n) else None.
+Proof.
+  destruct lt_dec; [ | rewrite nth_error_length_error; rewrite ?List.rev_length; try reflexivity; omega ].
+  revert dependent n; induction ls as [|x xs IHxs]; cbn [length List.rev]; try omega; try reflexivity; intros.
+  { destruct n; reflexivity. }
+  { rewrite nth_error_app, List.rev_length, Nat.sub_succ.
+    destruct lt_dec.
+    { rewrite IHxs by omega.
+      rewrite <- (Nat.succ_pred_pos (length xs - n)) by omega.
+      cbn [List.nth_error].
+      f_equal; omega. }
+    { assert (n = length xs) by omega; subst.
+      rewrite Nat.sub_diag.
+      reflexivity. } }
+Qed.
+
+Lemma concat_fold_right_app A ls
+  : @List.concat A ls = List.fold_right (@List.app A) nil ls.
+Proof. induction ls; cbn; eauto. Qed.
diff --git a/src/Util/ListUtil/FoldBool.v b/src/Util/ListUtil/FoldBool.v
index 6cfe6734a..b69081cab 100644
--- a/src/Util/ListUtil/FoldBool.v
+++ b/src/Util/ListUtil/FoldBool.v
@@ -43,3 +43,15 @@ Proof.
   revert ls2; induction ls1, ls2; cbn; try reflexivity.
   apply f_equal2; eauto.
 Qed.
+
+Lemma fold_andb_map_iff A B R ls1 ls2
+  : (@fold_andb_map A B R ls1 ls2 = true)
+    <-> (length ls1 = length ls2
+         /\ (forall v, List.In v (List.combine ls1 ls2) -> R (fst v) (snd v) = true)).
+Proof.
+  revert ls2; induction ls1 as [|x xs IHxs], ls2 as [|y ys]; cbn; try solve [ intuition (congruence || auto) ]; [].
+  rewrite Bool.andb_true_iff, IHxs.
+  split; intros [H0 H1]; split; auto;
+    intuition (congruence || (subst; auto)).
+  apply (H1 (_, _)); auto.
+Qed.
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.