blob: f620ccc96f809a2253512b4adfb20a39ec4b47b7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
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.
Lemma nth_error_Proper_eqlistA {T R}
: Proper (eqlistA R ==> eq ==> option_eq R) (@nth_error T).
Proof.
intros ls1 ls2 Hls n n' ?; subst n'.
revert ls1 ls2 Hls.
induction n; intros ls1 ls2 Hls; destruct Hls; cbn; auto.
Qed.
|
