fact: Definition sieve' (fuel : nat) (max : Z) := List.rev (fst (@nat_rect (fun _ => list Z * PositiveSet.t * positive -> list Z * PositiveSet.t ) (fun '(primes, composites, next_prime) => (primes, composites)) (fun _ rec '(primes, composites, next_prime) => rec (if (PositiveSet.mem next_prime composites || (Z.pos next_prime >? max))%bool%Z then (primes, composites, Pos.succ next_prime) else (Z.pos next_prime :: primes, List.fold_right PositiveSet.add composites (List.map (fun n => Pos.mul (Pos.of_nat (S n)) next_prime) (List.seq 0 (Z.to_nat (max / Z.pos next_prime)))), Pos.succ next_prime))) fuel (nil, PositiveSet.empty, 2%positive))).
imports: Coq.QArith.QArith Coq.MSets.MSetPositive Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.ZArith.ZArith Coq.Lists.List PerformanceExperiments.Harness