gcd.mlw 2.39 KB
Newer Older
1 2 3 4

(* Greatest common divisor, using the Euclidean algorithm *)

module EuclideanAlgorithm
5

6
  use import int.Int
7
  use import number.Gcd
8 9
  use import int.ComputerDivision

10
  let rec euclid (u v: int) : int
11
    variant  { v }
12
    requires { u >= 0 /\ v >= 0 }
13 14 15
    ensures  { result = gcd u v }
  =
    if v = 0 then
16 17
      u
    else
18
      euclid v (mod u v)
19

20
end
21 22 23 24 25 26 27 28

module EuclideanAlgorithmIterative

  use import int.Int
  use import ref.Ref
  use import number.Gcd
  use import int.ComputerDivision

29
  let euclid (u0 v0: int) : int
30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45
    requires { u0 >= 0 /\ v0 >= 0 }
    ensures  { result = gcd u0 v0 }
  =
    let u = ref u0 in
    let v = ref v0 in
    while !v <> 0 do
      invariant { !u >= 0 /\ !v >= 0 }
      invariant { gcd !u !v = gcd u0 v0 }
      variant   { !v }
      let tmp = !v in
      v := mod !u !v;
      u := tmp
    done;
    !u

end
46 47 48 49 50 51 52 53 54 55 56 57 58

module BinaryGcd

  use import int.Int
  use import int.Lex2
  use import number.Parity
  use import number.Gcd
  use import int.ComputerDivision

  lemma even1: forall n: int. 0 <= n -> even n <-> n = 2 * div n 2
  lemma odd1: forall n: int. 0 <= n -> not (even n) <-> n = 2 * div n 2 + 1
  lemma div_nonneg: forall n: int. 0 <= n -> 0 <= div n 2

59 60
  use number.Coprime

61 62 63 64 65 66 67 68
  lemma gcd_even_even: forall u v: int. 0 <= v -> 0 <= u ->
    gcd (2 * u) (2 * v) = 2 * gcd u v
  lemma gcd_even_odd: forall u v: int. 0 <= v -> 0 <= u ->
    gcd (2 * u) (2 * v + 1) = gcd u (2 * v + 1)
  lemma gcd_even_odd2: forall u v: int. 0 <= v -> 0 <= u ->
    even u -> odd v -> gcd u v = gcd (div u 2) v
  lemma odd_odd_div2: forall u v: int. 0 <= v -> 0 <= u ->
    div ((2*u+1) - (2*v+1)) 2 = u - v
69 70 71
  lemma gcd_odd_odd_aux: forall u v: int. 0 <= v <= u ->
    gcd (2 * u + 1) (2 * v + 1) = gcd ((2*u+1) - 1*(2*v+1)) (2 * v + 1)
  lemma gcd_odd_odd: forall u v: int. 0 <= v <= u ->
72
    gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1)
73
  lemma gcd_odd_odd2: forall u v: int. 0 <= v <= u ->
74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
    odd u -> odd v -> gcd u v = gcd (div (u - v) 2) v

  let rec binary_gcd (u v: int) : int
    variant  { (v, u) with lex }
    requires { u >= 0 /\ v >= 0 }
    ensures  { result = gcd u v }
  =
    if v > u then binary_gcd v u else
    if v = 0 then u else
    if even u then if even v then 2 * binary_gcd (div u 2) (div v 2)
                             else binary_gcd (div u 2) v
              else if even v then binary_gcd u (div v 2)
                             else binary_gcd (div (u - v) 2) v

end