why3/examples/word_common_factor.mlw

(** {2 Common factor of two words}

    If `a ++ b = b ++ a` then `a` and `b` are powers of a common word.

    Authors: Jean-Christophe Filliâtre (CNRS)
             Andrei Paskevich (Univ Paris-Sud)

*)

use int.Int
use seq.Seq
use seq.FreeMonoid

type char
type word = seq char

let rec function power (w: word) (n: int) : word
  requires { n >= 0 }
  variant  { n }
  = if n = 0 then empty else w ++ power w (n - 1)

let rec lemma power_add (w: word) (n1 n2: int)
  requires { n1 >= 0 && n2 >= 0 }
  variant  { n1 }
  ensures  { power w (n1 + n2) == power w n1 ++ power w n2 }
  = if n1 > 0 then power_add w (n1 - 1) n2

let rec common_factor (a b: word) : (w: word, ka: int, kb: int)
  requires { a ++ b == b ++ a }
  ensures  { ka >= 0 /\ a == power w ka }
  ensures  { kb >= 0 /\ b == power w kb }
  variant  { length a, length b }
  = if length a = 0 then b, 0, 1
    else if length b = 0 then a, 1, 0
    else if length a <= length b then begin
      let c = b[length a ..] ensures { b == a ++ result } in
      let w, ka, kc = common_factor a c in
      w, ka, ka + kc
    end else
      let w, ka, kb = common_factor b a in
      w, kb, ka