proposition: Theorem arbFunComplete `{CoArbitrary A, Arbitrary B} (max:A) (f:A-> B) (s:nat) : s = Pos.to_nat (coarbitrary max) -> (semGenSize arbitrary s <--> setT) -> exists seed, forall a, coarbLe a max -> run arbitrary s seed a = f a.
proof: Proof. move=> eqsize semB. have/choice [fseed fseedP]: forall a, exists seed : RandomSeed, run arbitrary s seed = f a. by move => a; case: (semB (f a))=> _ /(_ I) [seed ?]; exists seed. case: (coarbComplete max fseed) => seed Hseed. pose proof (randomSplitAssumption seed seed) as Hyp. move : Hyp => [seed' Hsplit]. exists seed' => a le_a; rewrite -fseedP -Hseed //=. apply (@promoteVariant A B a (fun a => posToPath (coarbitrary a)) arbitrary s seed' seed seed Hsplit). Qed.
imports: PArith List ChoiceFacts Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool) Classes RandomQC Generators Sets