Commit 9aa57786 authored by Felipe Cerqueira's avatar Felipe Cerqueira

Add mapP lemma for non-eqTypes lists

parent a0354880
......@@ -95,6 +95,18 @@ Section UniqList.
by apply filter_idx_lt_take.
Qed.
Lemma mapP2 (T: Type) (T': eqType) (s: seq T) (f: T -> T') y:
reflect (exists2 x, List.In x s & y = f x) (y \in map f s).
Proof.
elim: s => [|x s IHs]; first by right; case.
rewrite /= in_cons eq_sym; case Hxy: (f x == y);
first by left; exists x; [by left | by rewrite (eqP Hxy)].
apply: (iffP IHs) => [[x' Hx' ->]|[x' Hx' Dy]];
first by exists x'; [by right | by done].
exists x'; last by done.
by subst y; move: Hx' => [EQ | IN] //; subst; rewrite eq_refl in Hxy.
Qed.
End UniqList.
(* Additional lemmas about list zip. *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment