ewd650.mlw 692 Bytes
Newer Older
1 2 3

(* EWD 650: A Theorem About Odd Powers of Odd Integers *)

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
4
module EWD650
5

6 7 8 9 10
  use int.Int
  use int.Power
  use number.Parity
  use number.Divisibility
  use ref.Refint
11

12 13 14 15 16 17
  let theorem (p: int) (k: int) (r: int)
    requires { p >= 1 /\ odd p /\ k >= 1 /\ 1 <= r < power 2 k /\ odd r }
    ensures  { 1 <= result < power 2 k }
    ensures  { divides (power 2 k) (power result p - r) }
    ensures  { odd result }
  = let x = ref 1 in
18 19
    let d = ref 2 in
    for i = 1 to k do
20 21
      invariant { !d = power 2 i /\ 1 <= !x < !d }
      invariant { divides !d (power !x p - r) /\ odd !x }
22 23 24 25 26 27
      if not (divides (2 * !d) (power !x p - r)) then x := !x + !d;
      d := 2 * !d
    done;
    !x

end