Commit 97ab0949 authored by Ralf Jung's avatar Ralf Jung

prove list_find_fmap

parent 5f2a6b77
...@@ -907,6 +907,15 @@ Section find. ...@@ -907,6 +907,15 @@ Section find.
induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto. induction 1 as [|x y l ? IH]; intros; simplify_option_eq; eauto.
by destruct IH as [[i x'] ->]; [|exists (S i, x')]. by destruct IH as [[i x'] ->]; [|exists (S i, x')].
Qed. Qed.
Lemma list_find_fmap {B : Type} (f : B A) (l : list B) :
list_find P (f <$> l) = prod_map id f <$> list_find (P f) l.
Proof.
induction l as [|x y IH]; [done|]. simpl.
case_decide; [done|].
change (list_fmap B A f y) with (f <$> y). (* FIXME it simplified too much *)
rewrite IH. by destruct (list_find (P f) y).
Qed.
End find. End find.
(** ** Properties of the [reverse] function *) (** ** Properties of the [reverse] function *)
......
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