From 4a782deda6507c7fe16f2a4a59f15b6386ddad94 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 2 Apr 2019 17:30:11 +0200 Subject: [PATCH] word_common_factor: simplified proof --- examples/word_common_factor.mlw | 21 ++++++----- examples/word_common_factor/why3session.xml | 39 +++++++++++--------- examples/word_common_factor/why3shapes.gz | Bin 1077 -> 1047 bytes 3 files changed, 32 insertions(+), 28 deletions(-) diff --git a/examples/word_common_factor.mlw b/examples/word_common_factor.mlw index a9f7f05bc..0e71e8276 100644 --- a/examples/word_common_factor.mlw +++ b/examples/word_common_factor.mlw @@ -1,7 +1,12 @@ (** {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 diff --git a/examples/word_common_factor/why3session.xml b/examples/word_common_factor/why3session.xml index dcb7294da..c6cc77f9f 100644 --- a/examples/word_common_factor/why3session.xml +++ b/examples/word_common_factor/why3session.xml @@ -14,51 +14,54 @@ - - - - + + + + - + - + - - + + - + - + - + - + - + - + - + - + - - + + + + + diff --git a/examples/word_common_factor/why3shapes.gz b/examples/word_common_factor/why3shapes.gz index 0b9d21306e087a145edf2946925023947017a15a..249e9bfb481a8fdcd6c77bf2509f36dac6c7bd74 100644 GIT binary patch literal 1047 zcmV+y1nB!8iwFP!00000|Ls^!YaBTcz57?pJ#0|vTaXEuC4m8x-1@RCrX-b;A?uki zG3)&Nt=`PE)a~x^ItLF6IoNcmRj=Nws@BKY7)sKzWUWoMI;J29l!+9Q&O)12_xq~s z538^H2Rh((SGM0*Z`U0paecJjbkJ2}okS;Yj@ECTNU-^EwAO5iO~qjA{gsU-1}UYG z1TrRP2qkDmBn@KLb`<{>b3TEs@!z3N90y)84S9Ngb\$Z#s@FX|Ou4>LzRo5yA5_~)f zdfTRf1<8@6+Z5>zMk#_3;-&@MECE8FFD-(SLAb1yv)PnLCJD&a7m-Xf{*nijMJS+UuejmYCS|E2PE z4Q#6Vc(7R?Cm9(P@BJ0#fQXRLWQwIYuYH7AwBx_*Ra|{NP}=YE_I|tHO?k2B@gdG+ zkKZoOpEAan#G^4xGi7CvSdEByrM%&d22?8OBnFSd0V!#c3Lpv!Uh==)Pem|dY%\$Xd zk+lQ}u4oF{dEP6taHV8NviO`sq}AVe*y8Sfl_?zvztN;+ndrHk\$4kpIhJbXjQGs?j z7*V7Kv|31M3(fY^7%){M4J~vjIg0nf#K#IPgC-liQ6wYk7(}L`qx+x95fURg7o)P7 z#poDOcwJ0zSjfAloA3MwAE)biGk?0CGoRC(*|p=t3#EhtCSK@@5~lEfXVE3f#%1q4 zW}}xvvHFylNPQK^AGe%qa&VzDY!p z\$R+8}KBGA=s>4H0&N7d~chq6+- zkTc#qwJ*hCEBb-{QoJ<=k!%cLr1!ylrT93+WijNXa=I)X)\$qs73Lo\$b)|(X@Ni_W`?V7jDwd|y4JZW}{MT9&M}\$yUb{1c5S{g}wG5b7ULK4?I>C+OHgD_8GDeiXCFH4bN@nt8?SrUuE2TQkCHkufultL27 zn4BS\$pcRoch*{fF{CmuK?`)3GOG~j^_`opa{`tdxa|!iHE>4@ODN{9=4ul}V*FB-n zZ5o)697(!OkzT?mMKJQXXdNz2IfOo6\$&yE@oJvs@qbP_NlvN@Y&Yg2&pRWx)tiRL! zLI^}pT51!N7e*^zWUXpiKRm2g_XX2-y{TbqlglBm;|63MQFTjo+Rz}{*rD<3cYZ@-(T@jA z@(qorUW*HMGk6{igugjcqycjihVut4OmWyAeG?3ZEx|P6H\$6z*&{-8G498ZF8IFcU zO!n^4;snL7hpwh)XD~cQ\$ADymRW_E@sXPyGFl@^bbaHyy6FvrK72_>B%qkEw!~sCY%*^xk7O`cz8JQM?3?5R1qbDJdrkB@?Bx4x&xYLNpprmbR_mMHvt` zBA<\$~NaJNrIS}!;R1}F^k`C<~n)9MOJmln@!_4_FeEa2`Oz_2k7C~V-S&6p|&AYMD z;7TgR8Fa+&)ix2SOyHDPQ91XvzPcO_\$)|TNNoH\$p5d2aB++Hbb!-Wb({;Te~9Gj?8 zup)%uNeF2Y8Xg?VO6fw*c=OV=6zfg&)BAhjHb~id\$|(rty)?y%(7)H25UmPX&K}p_ zwiCeP&#w@C!oTA16~aRMt-|4|7PeXpuK74)t7gC7Zk*29_-WeZnZWUM;5Ol*4d&LKy+I2TCmN\$Qg^{UfP2-{IEBogk^>gciXA=Mbm=6*~ -- GitLab