proposition: Lemma umfoldl_umfilt R (a : R -> K -> V -> R) (p : pred (K * V)) f z0 d: um_foldl a z0 d (um_filter p f) = um_foldl (fun r k v => if p (k, v) then a r k v else r) z0 d f.
proof: Proof. move: f z0; elim/um_indf=>[||k v f IH W P] z0 /=. - by rewrite !umfilt_undef !umfoldl_undef. - by rewrite !umfilt0 !umfoldl0. have V1 : all (ord k) (dom f) by apply/allP=>x; apply: path_mem (@trans K) P. have V2 : all (ord k) (dom (um_filter p f)). - apply/allP=>x /dom_umfilt [w][_] /In_dom. by apply: path_mem (@trans K) P. have : valid (um_filter p (pts k v \+ f)) by rewrite valid_umfilt W. by rewrite !umfiltPtUn W; case: ifP=>E V3; rewrite !umfoldlPtUn // E IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)