Commit e76a300d authored by MARCHE Claude's avatar MARCHE Claude
Browse files

In progress: euler003

parent 2b6fffc3
......@@ -14,37 +14,64 @@ use import number.Divisibility
use import number.Prime
(** returns the smallest divisor of [n] greater or equal to [d] *)
let rec prim_fact (d n:int) : int
let rec smallest_divisor (d n:int) : int
requires { 2 <= n }
requires { 1 <= d <= n }
ensures { d <= result <= n }
ensures { divides result n }
ensures { forall i:int. d <= i < result -> not divides result i }
variant { n - d }
= if d * d > n then n else
if mod n d = 0 then d else
prim_fact (d+1) n
if d >= 2 && mod n d = 0 then d else
smallest_divisor (d+1) n
let test2 () = smallest_divisor 2 13195 (* 5 *)
let test5 () = smallest_divisor 5 13195 (* 5 *)
let test6 () = smallest_divisor 6 13195 (* 7 *)
let test8 () = smallest_divisor 8 13195 (* 13 *)
let test14 () = smallest_divisor 14 13195 (* 29 *)
let test30 () = smallest_divisor 30 13195 (* 35 *)
exception Exit
use import ref.Ref
use import list.List
val factors : ref (list int)
let largest_prime_factor (n:int) : int
requires { 2 <= n }
ensures { prime result }
ensures { divides result n }
ensures { forall i:int. result < i <= n -> not (prime i /\ divides i n) }
= let factor = ref 1 in
try
while True do
invariant { 1 <= !factor < n }
invariant { divides !factor n }
let d = prim_fact (!factor+1) n in
if d = n then raise Exit;
factor := d
done;
absurd
with Exit -> !factor
end
= let d = smallest_divisor 1 n in
let factor = ref d in
let target = ref (div n d) in
factors := Cons d Nil;
while !target >= 2 do
invariant { !target = 1 \/ 2 <= !factor <= !target }
(* invariant { 2 <= !factor <= n } *)
(* invariant { divides !target n } *)
invariant { divides !factor n }
invariant { prime !factor }
variant { !target }
let d = smallest_divisor !factor !target in
factor := d;
factors := Cons d !factors;
target := div !target d
done;
!factor
let test () =
largest_prime_factor 13195 (* should be 29 *)
let solve () =
largest_prime_factor 600851475143 (* should be 6857 *)
end
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment