proposition: Lemma stateset_fold_rec_bis: forall (P : stateset -> A -> Type) p (f : forall i, A -> StateSet.mem i p = true -> A) i, (forall u v a, StateSet.Equal u v -> P u a -> P v a) -> P StateSet.empty i -> (forall x a q (H: StateSet.mem x p = true), ~StateSet.In x q -> P q a -> P (StateSet.add x q) (f x a H)) -> P p (stateset_fold p f i).
proof: Proof. intros P p f i Hc Hi Ha. refine (StateSetProps.Props.fold_rec_bis _ _ _); auto. clear i Hc Hi. intros x a q Hxp Hxq IHa. apply StateSet.mem_1 in Hxp. replace ((if StateSet.mem x p as x0 return (StateSet.mem x p = x0 -> A) then fun H : StateSet.mem x p = true => f x a H else fun _ : StateSet.mem x p = false => a) refl_equal) with (f x a Hxp). auto. remember (f x a) as f'. clear. revert Hxp f'. destruct (StateSet.mem x p); intros. rewrite (eq_proofs_unicity bool_dec' Hxp refl_equal). reflexivity. discriminate. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(Utils_WF) Coq(Relations) Coq(Eqdep_dec)