Commit 7748d9c5 authored by Ralf Jung's avatar Ralf Jung

use csimpl

parent 09dc9e0d
...@@ -911,9 +911,8 @@ Section find. ...@@ -911,9 +911,8 @@ Section find.
Lemma list_find_fmap {B : Type} (f : B A) (l : list B) : 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. list_find P (f <$> l) = prod_map id f <$> list_find (P f) l.
Proof. Proof.
induction l as [|x l IH]; [done|]. simpl. induction l as [|x l IH]; [done|]. csimpl. (* csimpl re-folds fmap *)
case_decide; [done|]. case_decide; [done|].
change (list_fmap B A f l) with (f <$> l). (* induction didn't re-fold *)
rewrite IH. by destruct (list_find (P f) l). rewrite IH. by destruct (list_find (P f) l).
Qed. Qed.
...@@ -930,8 +929,8 @@ End find. ...@@ -930,8 +929,8 @@ End find.
Lemma list_fmap_omap {B C : Type} (f : A option B) (g : B C) (l : list A) : Lemma list_fmap_omap {B C : Type} (f : A option B) (g : B C) (l : list A) :
g <$> omap f l = omap (λ x, g <$> (f x)) l. g <$> omap f l = omap (λ x, g <$> (f x)) l.
Proof. Proof.
induction l as [|x y IH]; [done|]. simpl. induction l as [|x y IH]; [done|]. csimpl.
destruct (f x); [|done]. simpl. by f_equal. destruct (f x); [|done]. csimpl. by f_equal.
Qed. Qed.
Lemma list_omap_ext {B C : Type} (f : A option C) (g : B option C) Lemma list_omap_ext {B C : Type} (f : A option C) (g : B option C)
(l1 : list A) (l2 : list B) : (l1 : list A) (l2 : list B) :
...@@ -939,7 +938,7 @@ Lemma list_omap_ext {B C : Type} (f : A → option C) (g : B → option C) ...@@ -939,7 +938,7 @@ Lemma list_omap_ext {B C : Type} (f : A → option C) (g : B → option C)
omap f l1 = omap g l2. omap f l1 = omap g l2.
Proof. Proof.
induction 1 as [|x y l l' Hfg ? IH]; [done|]. induction 1 as [|x y l l' Hfg ? IH]; [done|].
simpl. rewrite Hfg. destruct (g y); [|done]. csimpl. rewrite Hfg. destruct (g y); [|done].
by f_equal. by f_equal.
Qed. Qed.
......
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