Add list_elementwise_eqlistA

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Util/ListUtil/SetoidList.v b/src/Util/ListUtil/SetoidList.v
new file mode 100644
index 000000000..dd89b65a9
--- /dev/null
+++ b/src/Util/ListUtil/SetoidList.v
@@ -0,0 +1,17 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Setoids.Setoid.
+Require Import Coq.Lists.SetoidList.
+Require Import Crypto.Util.Option.
+
+Import ListNotations.
+
+Lemma list_elementwise_eqlistA : forall {T R} (l1 l2 : list T),
+  (forall i, option_eq R (nth_error l1 i) (nth_error l2 i)) -> eqlistA R l1 l2.
+Proof.
+  induction l1, l2; intros H; try solve [ constructor ];
+    pose proof (H 0%nat) as Hfirst; cbn in Hfirst; try solve [ inversion Hfirst ].
+  constructor; [ assumption | ].
+  apply IHl1.
+  intros i; specialize (H (S i)).
+  assumption.
+Qed.