new example: word common factor

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. *)
+
+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 remove_prefix (a b: word) : word
+  requires { length a <= length b && b[0 .. length a] == a }
+  ensures  { b = a ++ result }
+  variant  { length a }
+  = if length a = 0 then b else remove_prefix a[1..] b[1..]
+
+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 /\ 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 = remove_prefix a b 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

examples/word_common_factor/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
+<file proved="true">
+<path name=".."/>
+<path name="word_common_factor.mlw"/>
+<theory name="Top" proved="true">
+ <goal name="VC power" expl="VC for power" proved="true">
+ <proof prover="2"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="VC power_add" expl="VC for power_add" proved="true">
+ <proof prover="1"><result status="valid" time="0.14" steps="270"/></proof>
+ </goal>
+ <goal name="VC remove_prefix" expl="VC for remove_prefix" proved="true">
+ <proof prover="1"><result status="valid" time="0.05" steps="518"/></proof>
+ </goal>
+ <goal name="VC common_factor" expl="VC for common_factor" proved="true">
+ <transf name="split_vc" proved="true" >
+  <goal name="VC common_factor.0" expl="precondition" proved="true">
+  <proof prover="1"><result status="valid" time="0.01" steps="78"/></proof>
+  </goal>
+  <goal name="VC common_factor.1" expl="variant decrease" proved="true">
+  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  </goal>
+  <goal name="VC common_factor.2" expl="precondition" proved="true">
+  <transf name="split_all_full" proved="true" >
+   <goal name="VC common_factor.2.0" expl="precondition" proved="true">
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="VC common_factor.3" expl="variant decrease" proved="true">
+  <transf name="split_all_full" proved="true" >
+   <goal name="VC common_factor.3.0" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
+   </goal>
+   <goal name="VC common_factor.3.1" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.05"/></proof>
+   </goal>
+   <goal name="VC common_factor.3.2" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.04"/></proof>
+   </goal>
+   <goal name="VC common_factor.3.3" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.04"/></proof>
+   </goal>
+   <goal name="VC common_factor.3.4" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.04"/></proof>
+   </goal>
+   <goal name="VC common_factor.3.5" expl="variant decrease" proved="true">
+   <proof prover="2"><result status="valid" time="0.03"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="VC common_factor.4" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  </goal>
+  <goal name="VC common_factor.5" expl="postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.24"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>