From b4b79ae26ee03954aaa7180fcf11741faa484760 Mon Sep 17 00:00:00 2001 From: Quentin Garchery Date: Mon, 25 Feb 2019 11:23:35 +0100 Subject: [PATCH] ThreeIdem is only in the logic --- examples/three_idem_ring.mlw | 21 ++++++++------------- examples/three_idem_ring/why3session.xml | 18 ++++++++---------- examples/three_idem_ring/why3shapes.gz | Bin 2492 -> 2499 bytes 3 files changed, 16 insertions(+), 23 deletions(-) diff --git a/examples/three_idem_ring.mlw b/examples/three_idem_ring.mlw index 387cf3eaf..60a2aa047 100644 --- a/examples/three_idem_ring.mlw +++ b/examples/three_idem_ring.mlw @@ -6,29 +6,24 @@ module ThreeIdempotentRing use int.Int - type t - val constant zero : t - val function (+) t t : t - val function ( *) t t : t - clone import algebra.Ring as R with - type t = t, constant zero = zero, function (+) = (+), function ( *) = ( *), - axiom . + clone export algebra.Ring with + axiom . (** Define multiplication by an integer recursively *) - let rec function mul (x : t) (n : int) : t + let rec ghost function mul (x : t) (n : int) : t requires { n >= 0 } variant { n } = - if n = 0 then zero else x + mul x (n-1) + if n = 0 then pure{zero} else let r = mul x (n-1) in pure {x + r} (** We get lemmas from the why3 library *) - clone import int.Exponentiation as Mul with - type t = t, constant one = zero, - function ( *) = (+), function power = mul, lemma . + clone int.Exponentiation with type t = t, + constant one = zero, function ( * ) = (+), function power = mul, + lemma . -(** {2 General results about unitary rings} *) +(** {2 General results about rings} *) (** First results : *) diff --git a/examples/three_idem_ring/why3session.xml b/examples/three_idem_ring/why3session.xml index 9698c7783..b03606168 100644 --- a/examples/three_idem_ring/why3session.xml +++ b/examples/three_idem_ring/why3session.xml @@ -13,19 +13,19 @@ - + - + - + - + - + @@ -67,11 +67,9 @@ - - @@ -143,14 +141,14 @@ - + - + @@ -171,7 +169,7 @@ - + diff --git a/examples/three_idem_ring/why3shapes.gz b/examples/three_idem_ring/why3shapes.gz index c6226f92be8414ca69fd52506a8bac8924cff8cf..d4cc58263ce13f4cad084a748846772197439f43 100644 GIT binary patch literal 2499 zcmV;!2|V^6iwFP!00000|Lt4dYaBTefA?SEXNQAQl~j`8vJj3n7{cA#ye_Je1Pi&{ zBex6A{qQ#nY{iQmH)yu^zJa_ zT2hEL`^=su+c9wt64=hXzwuDBxJ(4#c;MMsSLztC_oB5tn|Ii(x(OHCzKwf0(\$oD7 z4HAabSrIt7(x_x4L>FoZfpkxNkln*?|C-6>KOftu&Z+cIcjLocOdB^HVA6tGTP&\$c zDijHnTMA@6`3@=YdBzSphXpS7-FVbJXUt7F\$3czIYc1lEgW5#{yT&2NUXP7%BKhT10yyUYfq& zp4&ejdd(zOg?Bem%QHet1DA*!\$7pH;ti52>*dmGA4p3NoVWCwoev!pF`P54CwkAQS ztvDdxFgxreijQ9+uGi!@M#utLlb{fH3l(M{#j#3`G4L!l-A!!w>(qNp=yHz9!l5EV z>q&CcASH7Qy``K}mo\$%vFS&TqKq*;zhz-1iYBjgsa;|e{xY!9CUZfJC0ZL??I{\$wDWF-qe44wlu)>J*T8qAnWFyoLQsauA)Ex-K!VV8@?JovC} zn>4;)\$L8!UXFo;KVS^M!J{rbA~C@jc)%F@jaMp\$XSCO5TMran2QllZ z-r|K*oNfH\$`Hhd+)=l%=>c;nj>5tvG1Vqan8kNy(u\$9=QT4o{@RLd_%mUMSyNelJ^ zy>~W~G@J&Z_hyL=jj)#xi*H&^P;+x?fsq49@V*uUoY2IV-a4^QkaB#ElqUJv?Tl{E z>H+agrSQWO`iZUk5PeFeg+>Xu`);X8g)Lk4(r-s9\$`(Z@ar6nGrRQK`Z0EsO-<=)2 zLzRb-J6|~d9o!gJpC^Vj5iblY8eDB92NFi7!5PF5gY%}|ngL2M06CA3FSc~xE}2*o z)!H#=j1?_H8A\$HU0^khouFL0nM1DagwHh\$7j9aLipa%Q}&Z>>%g2Cbfbe_qH#\$S=o zS{Pew)V(o^l\$kAi2#az~)\$Da*r{ABATA61UP0&gYbz&Mp^\$j!@5rb|r?#+VIyD?zs zKI*+auI+vtu+Daj-;bu{(X{dJw|pJ)tK\$1n4rGbeD%~OCBnH-;VhZZj@Ju%39;*wt z%N(4f*{Esd6b+=rY>CDfFf?G9JS7TssAqTkJ4vQ?PGrFqa!_U~BBf}tqR5HVY~br4 zu#;p`%}H%gvywD>*VNd9o~^cyN!aUW\$^C_-4nAV7IYcu7mtsqniluZ8R_i2)ek%3B zGG6%A`!{-=)Dz@Uf7&y0rYSEcL?!wu)Jq~J8Zk`1>SHp=W|+5 z(Z8I+R2*FlZ(5Wv*Xq&tW;L{{)xv)!\$kDGRfj8xG-}1PBe%`vRO}EMYQSl~Q2<_;+ zK#E#w41;~E)MjOvSOz\$oa4uT&1Sc=I6|3z-%!Ypvd@5{+Ff^;xrLxs%q%bdRE@tOX zxLX!)Ah>}6AtL9q)#jaIMni?sL!X~3Y-v3HrDPB+?71EqJLgebFNR&6hs@pTf}H2Y z_ff^~#t1TxAF~qi%|hRd*oh!;bXK-Xd?8c}gjW}Q*oXOP^q@q;fkai{gsCS=3WZH3 zMT+lkp~OCj`qSd`3Y!x(-P!0*llD)O_QxlEeX{VrR~&U@mR_3KFIoolIZ3vx+O5J7 zQMcr(>-;>PSo_=W)v0)&VK{jX(E@r3xmt3wP-_vk\$?Q1o+#bGXS!7FO4V(eu;2=uq ztlYD~nclK`zYwCIuRU>#gOg01Vshp)aT{yhX4xmiuzvWwhMMQQb**m+ zAzZQ|o>+0Y?`cJRTJgj#&uRF}rTqLDZ5q=~cTbP~7ng*c3cq\$+O9#eF8\$Irv9S={K zU#7SugGn_^ zVXVjAVVwzbTS_*cFTighl&j%g}xc6Jcm9>&<)YpmbBU^tx4PKq_>Vz-pgb5N_ZCSl!\$&HmM3iRZLi=~Yq zuRGzwiOZ8pmQQ1z6tmK|RnK@*bM^YGt-p?~S1L{OaK_qN%(>M{)zA_Y7Od1)@A{px z^~JN!(bkvyo^0Kp7Vp)\$uFmy+IoCFA04L=T3Uc;XVu~Sa%&4`UtrEXR9bf25SKqz* z?\$vkAca;RY>prC|ui0YgUUkM}=PC?gPiI5vsUH^vb\$YfTQ9*uWye8*{1mSHjzAh>(iyA8hL&l;rzeo{{k{\$aJko_Arg_#02Ey6Rb;qr6Bh5}oxNLg zxA7ZVzA-mkHC*Wl8(itZO&EK&1{@~W8Fx>9xY#&ejGSC?JY2}}o3M2A5jXVX{Y}eF zlLZ76gVEJcG^PZI8MBH>#^1iy!bu\$uFkSp`ZJ1nf02Q?KftkRwqoRW>9\$tl|`}-S> zF}RQf8yh3\$FcK<+QXGqKb>Sk*UU9F+k_9R1)siAm z%-YbizkVa@nbnzDRnzYFc\$T6Mm8nN46wfb|>Yz1MAmQTGqjnT&-Nlp(a!J12t^a=4 zfBkg#uirn)&%gAapYFbYzxLIA*u8zX_Uq%z`|8&2\$KBiC)~@=;f9&4g+nakl(y+IO zl@sWVp~n>L\$9V9}-eGg#v`E&w{p8*6yZ!Il*}8CiJ3LwI!zyXhZp;&S*E80XRa5O= zQ+F&WP09YZefrgC8cTrDCU>n+8pfO?l50|9E3IfOQ?H^C{^svG} zAh`\$j7-J}%dsSOVAVqAQ+kyBXyT{-DIg!o3Kee4Y\$I?IF4UbbXt^Ig_F_x80FD9RW z-hoLCx}\$0mEC}NGB4bCLyBRJH-Eh)9Wz3H_he3@6xFsz;#?qlMILEOfMlP*Uit)J# z-0uuvr_I=lDN)(T7#*y_)Y&#`W=>)@Ihnqjxtoq8*jjJ}dWmc{0@{V6sjM@bVa-iH zY|kGakG*CRi^97fspT1=xq)-U2adhVA^R4zsN|X=WKShm\${~81akp1oyq63dEmWB? z#aO\$!jW>zevtl*(dx^N-lHVfWAf<*S#3mMf6QYyaav2n!>eRT7w)@A_drIhfjuS}r zj-*!C86XLI\$;IMhbgs83SE=`RRE`JE8Uqn6b!Kxp^W~&6H7Hbg_*R{ZIe-O+Nkf@xbXZ_urr7-TPh2 zfw4@V55{MMaqW))0jfWkuDzTBiEzXiVGSo;a6)2)G2nGKV9DVF5CKXo?G1bVKDx=80xG#+Nd!q9aTD|16HB^3v7{OM zX%?+G6|GF-Rg}8fPBQ~%fsji+L(NaA874twCu)pwPmPUg5\$S5sL}T?!h{sHAZ*&J% zkBDb1h3~iMCs-!Wq2-WBYhcs6w#}N(erhatJ1R9=6dlFUEkMi9!NjgT4!-)~;@~~1 zJdWJ^!s+ke#%}R>WLP8dx?x4zU(5n6S>m%8ZJR;`wh&3(Fl34xrt\$IBmbM_pAqMK` zeeMRi&EBl3JM*j7Ge1YW%kp_1kzbKXDw4=?D9te3;QBsLG+D8wFX;FjTA\$bW8}iw\$ zS}_=4=2>#^\$tTRw9M&qAfKm4DwXxH0&PH2qB\$;~j3gpOHJ~Lp87MvpbjJ(^MRY@Oq z0izzG-uu(q?uP;EY{rDcXq+F7>+s`-uVa3#@Z(Mn_^_%BnLGr;=E0f0x?F3rbckjz zIl~cIoN{oMX7h0XE6#`(Z)v|pg8;<}FIz~w4|j+Coh4&csuhi5;K9t)QnpVyR4_bi zh=L>bqrlFSv3Q@l+PmKi4l8-5Ut=g1X6ng zI+6Ndn)@hU@\$h8nqoQL1mr^J>)?heVK`>dJo|J=3AnDE+Hz9rsmJjT2hHaL;!W&NJ zd`as\$`qxt!i(@!0U^VUsmx=HR&6;?yZ zF6Oi?LA5%jduSS1nuSy!q+L!pSFL%5lh@mdRB2YiWG5Dys@40BIaP0fA+<_SriIPb z?ED3H%K4Up!! z!-7%8?{^Vo8b2l_;=7r?39&Ol;N+}qk@!rg7zi&e_;?8OPdU5;m\$W83v6 z^mGyh\$I2u zb7\$-GeOp@(=f!(-uA6gxTh7&pdXd_xcIJYu0~UvU_#{awz~l?;YpUagu5|O=oA2Iy zcL0HngDAz|Br#DbNwU;JB&c?p3r8*9VSw zvG8Gq>~mG^+GFS?rq*\$|a2%y_l#G)LK~sItnbE27PL1!>jF-+H?=Q@~j`oZ-q?DB@ zl)_v\$cjz(1>MW\$E7Bsdm|3v@o%Y+@9IEMe{W9mMFCg)Sf9D>tO8@}jn&HXy8asI~K zaMf_3ht{yr18ds#Yz&x2*BSRuVYt}1yBImT;&{A}6V^0\$^AXng!^5hRWQ{IyugwST zE;kAdF=Xx32g`V)g|!f7j4js~fT(FQ+}=Y=T%AdO=D*JNvUq\$GmL48f95SbF(Sa;( z=3a;Y>tpj3W-|?k(~B\$z#l0CzrD4~o;7u+#{0l(Sp1GkEIG?#*!wJkxQ{ez?2{Xg9j)kt&)>olkC2AH~t??pEw&A GJpcet)A?Ee -- 2.22.0