new example binary_gcd

examples/gcd.mlw

@@ -43,3 +43,42 @@ module EuclideanAlgorithmIterative
     !u
 
 end
+
+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
+
+  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
+  lemma gcd_odd_odd: forall u v: int. 0 <= v -> 0 <= u ->
+    gcd (2 * u + 1) (2 * v + 1) = gcd (u - v) (2 * v + 1)
+  lemma gcd_odd_odd2: forall u v: int. 0 <= v -> 0 <= u ->
+    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