(** {1 MPRI lecture 2-36-1 "Proof of Programs"} *) (** {2 Fermat's little theorem for n = 3} *) use int.Int use int.Power let lemma power_3 (x:int) ensures { power x 3 = x*x*x } = assert { power x 3 = power x (1+1+1) } let rec ghost little_fermat_3 (x : int) : int requires { x >= 0 } variant { x } ensures { power x 3 - x = 3 * result } = if x = 0 then 0 else let z = little_fermat_3 (x-1) in (* x^3 - x = ((x-1)+1)^3 - (x-1) - 1 = (x-1)^3 + 3*((x-1)^2+x-1) + 1 - (x-1) - 1 = 3*result + 3 ((x-1)^2+(x-1)) *) assert { power x 3 = power (x-1) 3 + 3 * ((x-1) * (x-1) + (x-1)) + 1 }; z + (x-1) * (x-1) + (x-1) let lemma lem_little_fermat_3 (x : int) requires { x >= 0 } ensures { exists y. power x 3 - x = 3 * y } = let _z = little_fermat_3 x in ()