fact: Fixpoint pick_next_aux pick_fuel {A} (gen : G A) (fuzz : A -> G A) fs ds fsq dsq randoms saved := match pick_fuel with | O => (gen, fs, ds, fsq, dsq, randoms, saved) | S pick_fuel => match fs with | ((O, fav)::fs') => pick_next_aux pick_fuel gen fuzz fs' ds fsq dsq randoms saved | ((S n, fav)::fs') => (fuzz fav, (n, fav)::fs', ds, fsq, dsq, randoms, saved) | [] => match fsq with | [] => match ds with | ((O, _)::ds') => (gen, fs, ds', fsq, dsq, randoms, saved) | ((S n, dis)::ds') => (fuzz dis, fs, ((n, dis):: ds'), fsq, dsq, randoms, saved) | [] => match dsq with | [] => match randoms with | O => pick_next_aux pick_fuel gen fuzz saved [] [] [] random_fuel saved | S randoms' => (gen, [], [], [], [], randoms', saved) end | _ => pick_next_aux pick_fuel gen fuzz [] dsq [] [] randoms saved end end | _ => pick_next_aux pick_fuel gen fuzz fsq ds [] dsq randoms saved end end end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrnat ssrbool eqtype div) ExtLib(Structures.Monad) SimpleIO(SimpleIO) QuickChick(RoseTrees RandomQC Generators Producer SemChecker) QuickChick(Show Checker State Classes) Coq.Strings.Ascii Coq.Strings.String List Recdef Arith.EqNat ZArith