diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/ListUtil/SetoidList.v | 17 |
2 files changed, 18 insertions, 0 deletions
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. |