Commit 05bf88b7 authored by Ralf Jung's avatar Ralf Jung

prove list_find_proper

parent 97ab0949
...@@ -916,6 +916,14 @@ Section find. ...@@ -916,6 +916,14 @@ Section find.
change (list_fmap B A f y) with (f <$> y). (* FIXME it simplified too much *) change (list_fmap B A f y) with (f <$> y). (* FIXME it simplified too much *)
rewrite IH. by destruct (list_find (P f) y). rewrite IH. by destruct (list_find (P f) y).
Qed. Qed.
Lemma list_find_proper (Q : A Prop) `{ x, Decision (Q x)} l :
( x, P x Q x)
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x y IH]; [done|]. simpl.
erewrite decide_iff by done. by rewrite IH.
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