From 8a0551767bdf1c6b8f5c05e50f9722912d4eb98b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 14 Sep 2018 23:51:36 -0400 Subject: Add list_elementwise_eqlistA --- src/Util/ListUtil/SetoidList.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 src/Util/ListUtil/SetoidList.v (limited to 'src/Util') 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. -- cgit v1.2.3