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 --- _CoqProject | 1 + src/Util/ListUtil/SetoidList.v | 17 +++++++++++++++++ 2 files changed, 18 insertions(+) create mode 100644 src/Util/ListUtil/SetoidList.v diff --git a/_CoqProject b/_CoqProject index 87582fb5b..d5f092a17 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6541,6 +6541,7 @@ src/Util/Decidable/Bool2Prop.v src/Util/Decidable/Decidable2Bool.v src/Util/ListUtil/FoldBool.v src/Util/ListUtil/Forall.v +src/Util/ListUtil/SetoidList.v src/Util/Logic/ImplAnd.v src/Util/Logic/ProdForall.v src/Util/NUtil/WithoutReferenceToZ.v 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