proposition: Lemma eval_omap (b : R -> K -> V' -> R) p a (f : U) z0 : eval b p (omap a f : U') z0 = eval (fun r k v => if a (k, v) is Some v' then b r k v' else r) (fun kv => if a kv is Some v' then p (kv.1, v') else false) f z0.
proof: Proof. elim/um_indf: f z0=>[||k v f IH W /(order_path_min (@trans K)) P] z0. - by rewrite omap_undef !eval_undef. - by rewrite omap0 !eval0. rewrite omapPtUn W evalPtUn //=; case D : (a (k, v))=>[w|]; last by apply: IH. rewrite evalPtUn //; last by move/allP: P=>H; apply/allP=>x /dom_omap_sub /H. rewrite (_ : pts k w \+ omap a f = omap a (pts k v \+ f)) ?valid_omap //. by rewrite omapPtUn W D. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)