word_common_factor: simplified proof

parent 79f53fcf
(** {2 Common factor of two words}
If `a ++ b = b ++ a` then `a` and `b` are powers of a common word. *)
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
......@@ -21,21 +26,17 @@ let rec lemma power_add (w: word) (n1 n2: int)
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 }
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 = remove_prefix a b in
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
let w, ka, kb = common_factor b a in
w, kb, ka
......@@ -14,51 +14,54 @@
<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>
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC common_factor.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="VC common_factor.1" expl="variant decrease" proved="true">
<goal name="VC common_factor.2" 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">
<goal name="VC common_factor.3" 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 name="VC common_factor.3.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="VC common_factor.3" expl="variant decrease" proved="true">
<goal name="VC common_factor.4" expl="variant decrease" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC common_factor.3.0" expl="variant decrease" proved="true">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.4.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">
<goal name="VC common_factor.5" 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 name="VC common_factor.6" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC common_factor.7" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.23"/></proof>
</goal>
</transf>
</goal>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment