blob: 59bae9ac41d1f1a1cfdce49f9d9d62acc859f8bb (
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
26
27
28
29
30
31
32
33
|
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.
Lemma eqlistA_eq_iff {A}
: forall ls1 ls2, eqlistA (@eq A) ls1 ls2 <-> ls1 = ls2.
Proof.
induction ls1 as [|x xs IHxs], ls2 as [|y ys IHys].
all: split; intro H; inversion_clear H; repeat constructor; subst; f_equal; try reflexivity.
apply IHxs; assumption.
Qed.
|
