From ce7bf93b1054c286eae10585a25214ddafe7a97a Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Fri, 19 May 2017 11:20:02 +0200 Subject: [PATCH] updated proof sessions --- examples/TODO | 3 - .../unraveling_a_card_trick/why3session.xml | 245 +-- .../unraveling_a_card_trick/why3shapes.gz | Bin 3608 -> 966 bytes examples/vacid_0_build_maze/why3session.xml | 400 ++++- examples/vacid_0_build_maze/why3shapes.gz | Bin 2423 -> 990 bytes ...0_red_black_trees_RedBlackTree_VC_add_1.v} | 47 +- .../vacid_0_red_black_trees/why3session.xml | 1549 ++--------------- .../vacid_0_red_black_trees/why3shapes.gz | Bin 7578 -> 3416 bytes ...sparse_array_2_SparseArray_permutation_1.v | 108 +- examples/vstte12_bfs/why3session.xml | 295 ++-- examples/vstte12_bfs/why3shapes.gz | Bin 4366 -> 3082 bytes 11 files changed, 657 insertions(+), 1990 deletions(-) rename examples/vacid_0_red_black_trees/{vacid_0_red_black_trees_WP_RedBlackTree_WP_parameter_add_1.v => vacid_0_red_black_trees_RedBlackTree_VC_add_1.v} (82%) diff --git a/examples/TODO b/examples/TODO index c3ef50d46..b17865180 100644 --- a/examples/TODO +++ b/examples/TODO @@ -27,9 +27,6 @@ sum_of_digits.mlw topological_sorting.mlw tortoise_and_hare.mlw tree_height.mlw -unraveling_a_card_trick.mlw -vacid_0_build_maze.mlw -vacid_0_red_black_trees.mlw vacid_0_sparse_array.mlw verifythis_2016_tree_traversal.mlw verifythis_fm2012_LRS.mlw diff --git a/examples/unraveling_a_card_trick/why3session.xml b/examples/unraveling_a_card_trick/why3session.xml index 25010a865..9f6f2315a 100644 --- a/examples/unraveling_a_card_trick/why3session.xml +++ b/examples/unraveling_a_card_trick/why3session.xml @@ -2,257 +2,52 @@ - - - - + + + + - + - + - + - + - + - - + + - - + - - + - + - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + diff --git a/examples/unraveling_a_card_trick/why3shapes.gz b/examples/unraveling_a_card_trick/why3shapes.gz index db52341a3970e7bd720a4595ac70fd99c6abe429..0ed422201763218670fb0a39413608d59c126fcc 100644 GIT binary patch literal 966 zcmV;%13CO3iwFP!00000|GigBj~h1(zWZ1B+@OF+iFyFZVX?pfzND98u7RYH8Y9jw zF!r|n`IX1gyk{F5O%KLM9DXFlkEF&?5;jI_sU1eI6@(B;3+)<0a!uIV^Vhc+Pr-gZ zp2}|*H3i*ph>UE*4H6SFD9J22Z-k^CRYT2cJoHvMrXq1Z4OCKYlG!TVWPB{kAsmSBD>8Ujw zd%Bsn$azYNNVcT(gvOEZfkmK{4X`+vrdrf;fD8Nl`f|P=evr{MEoCE%0!kup6_E1m#3A(+$*49jBuCl>u zCzII<<|hr9nVX!L4>LJ01~!0f18B1U0{b}6yy<(0Z@$t!`jcndT8C*KAQuCOoV)7q z9J>o~s>W*=(weku$Q4uP99PxT=asb2-C=f@siL{N^ri-VQ~IlzUbQ^s4p}ysxBO1- zbcWx_971uw$sNMbHvcVm$ZvT;A)P_tRpA{LK34Q~5LvCQp*wlw0#; za}Z_pox$W5;xpbwm(`h&uL-;Fh3h9mVCnOQxhN!a#%u5*eOiOmEPAIwl;Q4e+kCmS zNB_;9-;S3r=hyZUngs#<^>Y*aVqfg{!}^6Frdz&#A<#-m$Xo0)=~k)=KZpC&7iTKt z{MQ1k(SwJDp6G|dRKLr`7WUnc$^#vVIxWsaBiIu_iI4jrS@8e>O_}G02jYd0k*W?fKlV30CDQ;IeVebVuMqI-g7tUb_ o8poLN&6NIj%!$lnpljdPwh3+N-(}!zY_{6{19B1Igrg4t0P)B1y8r+H literal 3608 zcmV+z4(IV7iwFP!00000|Lt8{ZyPzXexG0A=N%k?RmCb6ft>>c0~pB5JT3IP;C0tH zv&pQJnX^BCt8K|@NiDf$%Z?{*II;Ueve{pKtV{FO2oqs1N{JI-?syRr?!Z{N+ah<89=95TI54l#bax47!aO&&=UjGn$M0HtX z&f;r!p*YYOwRuL#vVH0bEdzZ_H=p{=f3AKSirb#xP?zl~t=#qX57gOHrbe-86KL4F zqQqV)M#o6Ui{32_$4|O1I(JC9Vn&Eg3ahwH6UMo9oI6^!4}4xkqhDTt@A7B5ua+?F#92}C339XPs zg;f}X7Z*BUb-6WPLz1I~Z_C^qoW;bJNTm^#4BXgddtgf5Ud^RiB;ymG`zTFI%`w;N zvu^=v?g)06`pp4v4xY^6BTopM1Kk`voikWet7ffSsh3h(H%tSd>n=fd z@Wj_Vi~X;6)uxiN0$PE5ctGN|{n2i}SnW5tf81U&Z0RtiJ4_kJ5`i`1z^icm@#lVL zgdT2MnGcozX-EU%KKW{;*Vi9@*&@B$Zh+RM;))MTHPaC9@BhCQvtP;#jParvBdu^A z#^^2a`55CGW1PZxD076drNMa^;~Ha}!q_h235<^+Ot@`Z7eko9R2lhM2k#5|I9O`+K`S2Dx`H z0eKw!4!kJj-d=d5Xg%J)yoU+MEv?@Qd`RPI9^`A%l1@RcE6;NvcXyDF?7(pQ-~0Ek zxA_6~a>U&n>-*O?5B~ZVs0V0Q;lu6|KkOFwxL)Iv!aY~7c_YC*3b2VQp0C$egFF50_+>Kee<+7XdlO#X=IKrAwttiqwt9=l$)pb%=FJH z-;Kj?KfK@d$Sv4AzxyI!!FXucYf$GQvW8qzb}E6L=Hj40x%&0<=ijbwKK+qyZ_=l) zc69Ug#VUg-_>xI{k(^^^%-R#?Tsbk7QfF0W8o~1`69uUD*h6ZOC`F;(B6uNbDG8*> z%Irw@{AX%~G{nxmcgj6W5eI0&H3W^3d%XJXww2GH>dn`i&!3JqV~ZV6wvP4v>yIP% z4IgPAc$j71hAs50zu5Upus-i9kw$K;?*QnfDHtk_HM5^#v4qg&JL=E-91th~OAyuB+`2L0m+2VNqE) zTr6O3CDzKV#}u?lYvLRcOA9kawe3HhXo%Ym(?=TOBJfuTgMHK9bGP^?SNq9Gp+PR- zAjSmk*@2R2?{UxiT9boLDgIz8dZhSu=#-kJ_#fdL;=;E#!Z#`{daN-a7RVNj_l9O4 zx=853w}Ve`&x@TFw!Lq*iK{>bq1ECWsw794S*YbyT~wSGP7QAZaiP^htBsdbCHu(Q zHA^S~2!k?+GzjQ5z?l(Nc!>yW;pqG3s7p~Bm)3k3`n!nZFpPZg>lL{$9`WSw$3*9(~63*Ejo-9p8ZAwka+Q_9LEd**^%DQl_+ zLqg7tx-J#vFNFI}2WQZAK z%L=B_Vr`xR77P}6QBgiG@`|Gn?AWc>i@X++ekUYV9;P#QAwsXug__3>p0s2Mtqh}cW=2ixSyDh#4T~N+m8TolBCOeMf?TXn6DIQv zhJVe%A9PAmN%_3*{*MMc>qyt!hY1xte9RrGV0jpg@R$mIgee?}bXw&yH10{(j-gcfpmKRC4l6p+r;toYZBeVf_g~&p2O``4PgxuRkxpzy+1&Qcl^q3LL<^8iyT+ z`Am%N>bK8dzCO5}&zTy%Bb0Z9aOjju%Ggbz4sK@FJ^|vML=pH%a2v zQEm}(h^_$@@C+rMc5`Ob>QXN8>9GTkP-SbM7OFfWdeY!aG>4~9gzjPvg<7u3l`cVZ zzwG$Bg(!boqG+nli!?T8#(S^;I{{V{2&!aeVcyUcXS3ocItc4Ix_C_th z?*QL@NF{RWDqJCV>@C%X!o!ez(z(E2a;1Ysd}kPH#h#n}b}>?O1i5j>lwuHTLgBpG z=HJCq1`B)6SqQ_Y>^ON45hP_78kxg4tcii972exg1q*l1h$V>`DRr5|gnqQ$qx0@Ddt++1sQ+r8iS#4lp++`UTIVdR(^RFu9 z;5+g#St2y=Ent;AcV^3i{JF@tDi%dVA37#wilAzNTxiYp5;V-6r?PE06CIV~NaFNR z#zlT-JA)Q$W2|IWJh*}ZEegyrqiJnohtCcrb_ZcSRqLMa<$i=bTdlj0=d$EU)v@ox z4j)5v=MsyCD6yqlNqvaV9+!2YICP=Uo1~8>NI;AVK6?UW26j1hq3+oJ&K;_CpXB9)b$WzE+MEXn-a=XM{mi|Tdx;QER=hbl*85|^xTI%<(!k$QuGRy zf+Q)W_t~>G-V~P8rrk;Ui-6yXfTj6ilBlD4 zH*GYbV5^ZJx)fb(XRar8!Ce;@w!A^MG)IKKJ5X^RO2FihlBX7gROn%Q&XR8H-@o48 zl>bX#e!uzp_b;DszqUGlg@?UE?=So%eMPX(n;SjKj2ZaM1)Iuj~5ogunF7K!ntYbU4 z+u?Pu6~yrlrb80IP1Eu_8$bEorgbj7L#56Gb;z-K-e2$bl^rP+xZ7*(B+x5&i1X$- zli<2jwHZTt_k63(nD*lxWB0!b93lRAuFfd?pjUUO4?KhWqs^QDcc|S6IUHAGte96g zp3t*a2X`;^`L?!Od#ghT-MFw}uL>ri5Cf-Sp&uLu5Mh>@?1;M#8;F~)F!mAOP~{^y zWpGw??>%Q>Q+X|$!tnI{Nx#Gy6th!LVC15DTNv zn6M0M{d*^N=BH1@4qm;hf#$#%mGaw-sP0 zV6JAW(S=O4cp3Un5>r!jHBH&pc`bDj)(Zp$sdGTKmX<lsju{*~MsrF&(9l et)T%Cxf&n)2z?MsFJgNQvHcfTh+}+wkpKYYss_sd diff --git a/examples/vacid_0_build_maze/why3session.xml b/examples/vacid_0_build_maze/why3session.xml index 2209f87ed..907481788 100644 --- a/examples/vacid_0_build_maze/why3session.xml +++ b/examples/vacid_0_build_maze/why3session.xml @@ -2,10 +2,8 @@ - - - - + + @@ -16,81 +14,339 @@ - - - + + + - + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + diff --git a/examples/vacid_0_build_maze/why3shapes.gz b/examples/vacid_0_build_maze/why3shapes.gz index c32f221694921882dfaf5fe7d814946c06cb8f94..365233f295f4c1847a45556d0b52805e6b9093eb 100644 GIT binary patch literal 990 zcmV<410nn$iwFP!00000|GigDi{m&Dz0a@6d4~m6NwQ>^EQAF^py|Hp8YElZ4Qywo zzhIePzp@?MRcb5Dz)qhMm7b(mPgSLIUj^BtZF{dxtz^|nv_{rlz`oNEaOcmL{`~Lm z%k}s3_4hXiPB>gf!imES-M3;JeVh>vIh;;GHU&pI63r(WgOL>)ZxErXb!+=p^_}Vw zE9iQ?`yd`hw9(7HvoQ(QS2}9!YZE(bd~LC=e?q$dhY-XXtrxA55S12?G%}UwIuETd zqBb8+$OM&wtLm^dp;ZWN?PCZ6E71$#ZTxUT+Jc7wRadnrWv_*fA_Nna3BB*J-?=|` z{nzK6@48d${)#7m=}vE#^Vf_2=3oDIm9wsX@-O}|`j=P#8l4#|D}&mXZg%wKoqXRr}veKz#k<+v64%#FY0b&9I9JmRDQxDvvHc|57 zoe3aQZM2b_gR&$HCvM=xFW0U)+~+badVX;#TTQqTlq{p{jmPjjG-qo#1#gCEODYB?3s=K3kSyun5;K$qz=+zl~6@$-MNs7-n@RHrcLfY56Y zGF3+(LWogdh`~oc=Y4oP|I?iw{r7mD_`OT-xg=qB3d`;ih$OeGmart~7M62CJE+)Q z=*dPju8Joym@dO~vzZ5*EA~s3UK2?tKj=ELJ5bo-7D|VThZsyoQsGsRFoVf5Om6#y z@S~0;Rux}aa4l^)x`xR&>yW<=s3#*KT@E1zD+dwUf^R>3X#*?nT z8;vV%3B_$QptuFxF64`Ytdc{al%vkCk28mqVs=eOoO9{3tA_eG$E!@`Napc68i_Nq z7%74S@fHx5s%Wn4?z3|l=aks?#&!&7ZUN2xszQn!F?9l`=lJdUWexJ_57e7CLt}+mn@( zhWVu?8zEed6b37I4zk+zYg36Wzf!-*))o9B-yzaE$?Jg{ZFa*}A2a_a+u~UHd1bJ2 zLQ2~l`LQZ>nk44aQ1UiZ6ck%=d#2CYoJ=R)Q8G(2uD~gLT0|O$q<>7`^i)}wYUii_ M0L4Iaoy`#d03oB`e*gdg literal 2423 zcmV--35fO|iwFP!00000|Lt2@Ya>Y#e&1i==N$$zBX1Zlm<5AiaKF{7$#YjQZM$vv zu*|RDtSgVIEJ@odHRB$Eu@tV5GBVB*+#2j9lFV9cBoe^52YI9SPhtO` zn_s5apQhKpceq0xBnoxtZf3o;sLj2bIXbA>%SU+e2=7V?-Tw{gATcOTH8z@RqK#GF zDWkm?I+!f-h2;RQ7$Sm8Vr;M=qV}XGfom5qQ}%yR-FXDE&PJ1A%sJ+PdnBcZwv1{* z0L*)R)BW=%Jip#(=N`TLmw(hx?(yr>{`pD2==Xnjypx^!qTlpq---TxUR&w6{U7nK zl>o(a*?KPTXYy7*ef`{tiTZhZ z*Qc3)#S{FgByig2KowfXt*ulXsL6rOu-p5)hrF@0_lSzbTS6m0$F1j4F}S?Edi(t3_V3Ycn%ia_Pn(YK^M-h9&Ek1eBkZ!<^^PhT zcWbaPN>FQ^@mzyQ8DbWg+%=7(qMs(~^u*e& z7lNWy5Ud&0Weo(5Iw4tLR%=bXa6Be#3d$0R09khP^8EImEOd?If08)9`;c+G?K2-T zj%yh>2cwMjN^(H4CIdz=^M*5PjGAj9^L785d;F~b@cU7kmBVaQxV6`8F_rO&CmPFiCUTT%torx;?^1!8`)+n>^^FZwRmq+wc5j-%~^{T--X9VNpOfJgGq3#MzW}A zH=Bf-4R5pIrR2D2mRj^E37@%F!pAQdga_6E??6n_0~yIeEU_(C$;P+Y_)>ak8mX4P zmxRvjEAfHsvi!0GRmk6yg-b z?<>a{Lj-jMXABKw7LnkFB^NBH&4N;#5tA$rX_ZR0=sYdFpqhoXS=d9~VI<|4*B)Q} z%j?^)lBjhV@i)APHL%Cm_@MvrBqgBx`-TvU%*Ech}Cv-|uI+rBoao>!{aT$Qa>jo&kr4Kv%} zRf_LBCT*wzC#|^AZ*Ts!So^kzZ89TE(UOi${$$Wa!@p&ws_WlkV%e0UE6gtz zb`&R>ad(0ahqiIvuIyXegE}-wF^ECaaPOiG0|Uve4_Z5^CFcI-x98`VoBh-8`gO0L z-s8Ld`@B@1lAK#<=k@Ac(tzj(64@Tbdzs8Xyq|?U&=nNM++-5j{Hp3m7UoxHGyl|2 zCzDqhsSN>-Sae*Wzr_D z{tp0_qe^y>C~!Ftj3Cyxa; zE~!;I{^Ajh0{NH_8I?vbqLHL-RZbqU`nq+E7%l3C+_|bKfy%O>Mc*nDqb$2twCpdJ zT`MY){hfVfoLJAkasg0X&R6<)byq>QqFDBo)fjzK-g=h4$wmub;qj;V6kqzvY9#sX zz7p*v3t#EUBff$F0`>q12&L3`<+xB1dqIpaLXeiP95QEPxO52hhg|2xnEaRa&JT7< zQF`Y%?wy^4RldpwmzlkjEgWcDUVfqz7v33_ShVwa+0WziHS}0^xM=AI@`!iRpga$R zU}ZETO8cNN4vs491CNbfvz+Q3v^5_-wIsc|@YRK{E_^N*wubhN5JEKeKr#^K!3%K4 zAge%Nx#7a|8QWqjxIR@Pt5YS?K2;)%QzbH#a`gVbiV4@K@nNFI*cHuD;{xt=xv0@s zrFWI{R#YC~PE?Y2dz@IYZBKD=F~;rBa*I(VUQTlH`9`_W-RxVuK!YlJ-%VO4b09ASGZe=BTH z|4O#@&8Us=a=r*V-1$l|wWn}Jke>dO8tItIKxH?6$aU zCvvbCE2Q+ba*{u)jui64!eY&5C51a}0At6sRe1K2*H4H7g_+JfYUa;ZGAMj}p$ z^3r&7Jnx;*Xl%OH$$i>7v>i`-2_|@r6U=rG*D!kxvwxN_du=a%?Dm34;+QCq{&Zr@{3y5E{tFKCEiffU001o5%9#KF diff --git a/examples/vacid_0_red_black_trees/vacid_0_red_black_trees_WP_RedBlackTree_WP_parameter_add_1.v b/examples/vacid_0_red_black_trees/vacid_0_red_black_trees_RedBlackTree_VC_add_1.v similarity index 82% rename from examples/vacid_0_red_black_trees/vacid_0_red_black_trees_WP_RedBlackTree_WP_parameter_add_1.v rename to examples/vacid_0_red_black_trees/vacid_0_red_black_trees_RedBlackTree_VC_add_1.v index 883f03b00..3215baaa9 100644 --- a/examples/vacid_0_red_black_trees/vacid_0_red_black_trees_WP_RedBlackTree_WP_parameter_add_1.v +++ b/examples/vacid_0_red_black_trees/vacid_0_red_black_trees_RedBlackTree_VC_add_1.v @@ -7,10 +7,6 @@ Require int.Int. (* Why3 assumption *) Definition unit := unit. -Axiom qtmark : Type. -Parameter qtmark_WhyType : WhyType qtmark. -Existing Instance qtmark_WhyType. - (* Why3 assumption *) Definition key := Z. @@ -166,40 +162,31 @@ Axiom almost_rbtree_rbtree_black : forall (x:Z) (v:Z) (l:tree) (r:tree) (n:Z), (almost_rbtree n (Node Black l x v r)) -> (rbtree n (Node Black l x v r)). - - (* Why3 goal *) -Theorem WP_parameter_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\ - exists n:Z, (rbtree n t)) -> (((bst t) /\ exists n:Z, (rbtree n t)) -> - forall (result:tree), ((bst result) /\ ((forall (n:Z), (rbtree n t) -> - (match result with - | Leaf => (n = 0%Z) - | (Node Red l _ _ r) => (rbtree n l) /\ (rbtree n r) - | (Node Black l _ _ r) => (rbtree (n - 1%Z)%Z l) /\ (rbtree (n - 1%Z)%Z r) - end /\ - (match t with - | (Node Red _ _ _ _) => False - | (Leaf|(Node Black _ _ _ _)) => True - end -> (rbtree n result)))) /\ ((memt result k v) /\ forall (k':Z) (v':Z), - ((memt result k' v') \/ (((k' = k) -> (v' = v)) /\ ((~ (k' = k)) -> (memt t - k' v')))) -> ((memt result k' v') /\ (((k' = k) /\ (v' = v)) \/ - ((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (x:color) (x1:tree) (x2:Z) - (x3:Z) (x4:tree), (result = (Node x x1 x2 x3 x4)) -> exists n:Z, (rbtree n - (Node Black x1 x2 x3 x4))). -intros t k v (h1,(n,h2)) _ result (h5,(h6,(h7,h8))) c x1 x2 - x3 x4 h9. +Theorem VC_add : forall (t:tree) (k:Z) (v:Z), ((bst t) /\ exists n:Z, (rbtree + n t)) -> forall (o:tree), ((bst o) /\ ((forall (n:Z), (rbtree n t) -> + ((almost_rbtree n o) /\ ((is_not_red t) -> (rbtree n o)))) /\ ((memt o k + v) /\ forall (k':Z) (v':Z), ((memt o k' v') \/ (((k' = k) -> (v' = v)) /\ + ((~ (k' = k)) -> (memt t k' v')))) -> ((memt o k' v') /\ (((k' = k) /\ + (v' = v)) \/ ((~ (k' = k)) /\ (memt t k' v'))))))) -> forall (result:tree), + (exists x:color, (exists x1:tree, (exists x2:Z, (exists x3:Z, + (exists x4:tree, (o = (Node x x1 x2 x3 x4)) /\ (result = (Node Black x1 x2 + x3 x4))))))) -> exists n:Z, (rbtree n result). +intros t k v (h1,(n,h2)) o (h3,(h4,(h5,h6))) result +(x,(x1,(x2,(x3,(x4,(h7,h8)))))). + subst. intuition. -generalize (h6 n h2); clear h6. +generalize (h4 n h2); clear h4. intros. -destruct c; intuition. +destruct x; intuition. (* c = Red *) exists (n+1)%Z; intuition. simpl rbtree. replace (n+1-1)%Z with n by omega. -intuition. +simpl in H0. intuition. + (* c = Black *) exists n; intuition. -simpl rbtree. -intuition. + Qed. diff --git a/examples/vacid_0_red_black_trees/why3session.xml b/examples/vacid_0_red_black_trees/why3session.xml index 19815cc5f..3a8cc37cd 100644 --- a/examples/vacid_0_red_black_trees/why3session.xml +++ b/examples/vacid_0_red_black_trees/why3session.xml @@ -2,29 +2,27 @@ - - - + + + + - - - - + - + - + - + - + - + @@ -33,1517 +31,184 @@ - + + - + + - + + - + + - + - + - + - + - + - + - + - + - + - + - + - + - - - + - - - + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - + - + - + + + + - + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - + - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - - + + - - + + - - - + + - - + + - - + - - - - - - - - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - - + + - - - - - - - - - - - - - - - - - - - - - - - + + - - - + + - - + - - - - - + + + + - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + - - - + + - - - + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + - - + + - - + + - - - - - - - - + + + + + + - - + + - - - + + - - - + + diff --git a/examples/vacid_0_red_black_trees/why3shapes.gz b/examples/vacid_0_red_black_trees/why3shapes.gz index c8e82ea4313e6eb2c1badaa8e1bdf78f94ec3d98..b4a8f703fb4df946a8deff5eebae7b1e9a142401 100644 GIT binary patch literal 3416 zcmV-e4X5%SiwFP!00000|K(dtZydQ1zUx=aJr`CLpFna@3=c5C!Ulq1t_waLVP(mY z$GiFYDfWx(o{=SMwY$zn0yM)Wn=F3y)r;N2%tMYmG84BqZlhgUjHZP9-I;gY4HBWK=90 zR4EVs=C0iQXZKfbibES#ds>6`S3*E4jEn&a5DmD10SR<+UKf(o3-#C%;s}Q}toD59 zmtcrUI-`M+mKn7RQaM4%69^P_7nfz-tj7}>>2&c5oO8m4;6)-YWlBzC5fXNfNOU%l zb5`f<9AHpdS}2x;C>l)kG6tV^Jw{)X2%QFrplw!47OP#dEE+_S$=gJE_XzT56D4#^ z3FlqT(Gr$Or6j{dO(_bO#IA?*Yg+?E%0iQ{8jA2x5|blFi+t=T=IsI!TLG`b*2 z(jZi1r4{R>B4ve=DKIhK4YpBrcEo+pDqviI72{1})f-lOwxT3KIZB=dp>;OV2CX!Mz7^v`FNX34CF?o`XS{O7UfAfj5_mV0uyPW^&Vn_3r8* z)!-m?H?J9c#)h2-?5_e?BK85cFy*Nz$dJeccBJf5jSsu0rZ_w)1shgIMje?c8l^U@ zb~M?8%mxf4&450Hs`NPe+$(UpO2C9k!T^FXsxX!bWy(_8*p06%`hVm!+*oxmdF{l} zz<^aYdcKW$mM|NiebSXRGS5@6kofj6H}poGZ}(TxWg9IM%%x}~MP#QS$a`j%6eXK( zBKqn?l4;?CP1*6^BG`ll2q%Thj7>ClcYL!e_Yb>rbC=#s237CH{jjB*o9>#~AEuV( zmfc^sE_Y}hjyoz<_4S)FOfuQi-;MxB{l2xtB=9fCUw%0rMYj^*vQ+g-K>b=E4_%j> zR-^OP^pU#N7^!}>&d6n(Teb0gc^qDU#6Y;}4y?AqQcS)mR)*!6R*cIr2`N#P%n60R z{doWR^y8$HAs)5w)l_3(w>VId1BcbYQ2|F)(T)Skb^>-nO~b5MR%$UMVgxoDUNZ~D zo})1BYz~SU*O)qO!Tu4fI1E_6&$h{UEbBCj8G|NIKf3EN%v>19 zys%Yw;;}x*0p)tyAO{oRvDExGb(^eR(=GwVf%8TIRyzg816F&5v&~Lpy4Jj5fVWFr zVR~H>oT)fSE@sKiM9oE3(+jSf;1h=z!PQ!DUQewAH)nE>Lt4wsVym}ZIJ7H%o~vdu zpV4-Xh|@lh0q4v^O%9{>*XD9Js%mLVi~GbvykX?I=Rh5yBNp=Z-PU>VMWiJMm}OzP z7)INcvmL11HG^7(t^;RKam{<=O{|%ZxJ7ju)3tCC2dTlzSV0qxcw0CDMPh6=n6U?n z`#PY8k>@}Wt$-rl6>fpzizK!{v6e_4scDIN-$0#n5aYnbKZq4j#125L&Bkqkn#Qyi z%$XvIo`36rJ7iz`>o;SGb+cqP98<*GDQbwb+)uJI6D|3ZT-S;|`)f5GRXd$0k~lg9Cc;*Y6D1VZeB)RR@A3i#!tJ(M657T zcE&{V67Hy5Owgjo#5GLpIB>zlt|J=MNqbD>nZKOIw3eJ5rm_ta&D@$vBhN{rC0}ir zXeQ=kq>=WF_-%D{oPp;Y07wLnq>yXn_6wN zRPHF7Om-=CHd=yuNYK1LlesmgVERq3L55+PjfwE-z7>YA5&Fjjx!jzRL(U_pQ%E;O%FH~eb zOJ!`1!TH~Yi-V1PJC2!>Pyvo_k_aXHY7yCxBO{za(>Vj}WC}e4ZO=e?SSp)WXW)5FvtgjQ zz`$2h>WYubQ87~JVodare=r$Q(1oB4IMBOKEaU>*A6$h$S%hDA`yWoS`{SCnX>UbQ z8H0{85Jz%ff-Z=~K`xPP?R(#J)u9`X3YK#NTMr6AHj>J|`leQW<2Z1szHv=d<`}Nz zv}a5mhqRWRt8aXJ-Lca(Wtb}T^_H8{(MR3I+m4>P*AzivZ-e!rG?#`ZNbN=93CRSC0((E*Y93ibD=mI0mh0skj7 zhZWR!uMX780~eE|h&~{tkVt#0l3_>0d2tb-eEhC}+K~ADnyNjg`+!MDx5zYedUNsv zYIX86aCLj~GthZ^@?)QS?1-CV$BjAJryZYNS(AO1;~T>Ab9u4KXow63N-DcjpUefD zLg3hJT(Hp*z<0?DT=C*UQ2N!hu+L&eCFpNMiwj|%Wnh9ZBM<(ZRDX+i4w&kLtU zkCf?3?)D5xZg)RO-5%4AC0~7-I6a43T|F$KJ&)qFW;ksL{)8^a5v{RkvmG7wjBHO3 zR>dPZ5u@SXWOZ_sMIx8#J0?lzVhAo4k91*LxhhE$rI>UqC8$8sQgOjJrM1m$13K=$ z+;I^d|K-DNW<$8SJC&Y;70<&TYZ8xCC{Uuz$r)1UQ#86H$@`Q>Lz2ZZQ7>Edt8w)* zRVSj>Y<6SGjm6dJ?K_G-E7zrUs!Q8U_bH01b&R-x?m9VD(x4Ecq*SyZ6__v*BgY*B zv3}|Nz*hm$qt`h@L(M%aCR(>?W-dS|`*!6!X&)Cdwm#%ue_W5xsP+AgOd|C}0l>^pL<9<1ax%PeMXHBy5$01fzohr*pKNm-cvc z-sjM}pF{6{9)W7{A!lH%V|#<^S#L_v`bCKiT=Ge{WDl3T2$x!0l%|rs_AWUa061CK z>~MlN3JuD5MxViNFDHBdZ*UbAgAyqe6Rqc%mmm-qz{nvyf(_wD`I12ee!V1 z%NE&13_JAy{PO8G<8-z(^`%N+F$-D7*@h11WL`yX*7$>c=$*PYhIN}@`YjvjI~a?voHo$$9c-L&TXB&sD( zSl?;u9vaQr)4q4cFkP)LE_6T*|6-u(V?6DZ@|>+=p~CT36)xX&*5H@WdwYNX)0aY<@gb!A7`KXLYg0zlV=ccER_dlPjX>EGl u`yCrK(UNxd^7hiu{Iun97Kle#P^VwB;KKC#>&@=Z(fBX$52rq4H2?r7my9g{ literal 7578 zcmV;L9cAJliwFP!00000|LuKSZyh<3=DUA|-UkbiaUp}i%tLLV1PEw!0gHuR2fX$e z<95}$-CgtZH+XKzyc}E7k>sPY-A0!)PbM??MKI!vNRnxwvK2~{oEOR2`I<0WLPij5 zaufev|Nc4t^|w;*{k^$|d%Cyxc+Ypk4{rS7_FeOV!C)~VXYdt@cd?43428iPdlNr= z{?E^!YP~n{FEzH?cQ%5LnUQ@m7(+B*IWxr=8LDySCjM=42T5vyjfoU}09&GSC{c>d z7W6h6pRtpXRW{qDyo>KYw)g*Y^Y40S?xxH7FVg|uzH?BFHYSZ60#>OIyqH*8DaJ<$ zqfqA_VeakSbXou9Z{s685tg7mX~z0&steXbKN5-teY-g$>*9I0?}CYjQ{n7VkOT^+ z*S}1K0;u5j=8QzEhRA_9OWMUCB_`uJldHf{5nz+*&4|&LBx)i160J=Q6H5W>fCAR8 zDnM1-%^BoZ4cY2iE#f&MVzj6*C268cM;ly9HzTB9>RR=tRRV7X*d@X013J-zU_+=7 zZ_X%c)sQ%if|J@rLOe6_qp#%lNz{E%BZ6`S@kdK3)MHOn^A`| zUf-V>|4%Ku8@mn;UR%AVV2U~tvu$0M>cUG={b>uP<#cR9g@j-3jt6d`&R?`4jVYBX zx`xhh^htCq>Ny=!S#2>64dE9XQfFS9i$u;q_jwR2XN^P{AgLAmoBN+{+Haq3+WU{? z=fi;N_rmS2OYh$g=lt#6;mGNc-2OEE6z--Ug8tA=)&2By+ck0+Pycam?Y;YTIx+`= z|G59-kNbNwJjuf8QQa$99G_+BZup4~Ps8=o+&vCYQ>4bH4TGGfwt2c|bni|N z+FReL{iJI0AT2gv8?Cxr%QpF1Od_e|=WPy>-;JV=&F^fYk8V*U#Y{ohYd;A1RyC9|hTH3{oGc z?o$U<5gTh_#_Y)5{Qjv@2V?Yy<}Q_m zQ8^NEL(U+j0;#P*Vk9*V3l1M-V}3S-dJufpZ#tXBeQ*H+^$ePr^PjRvh9>8k2iYb2JaL?NNY zP`+k1ZZMmRg~`6PLf*CPoG9^#8hTty>adjZl04RK++a5s%VwH}R!<%^z8C#}b{ZQ& zMb&Uz6v3MqKm1)q`p-iw+wu76-|7;Q)vhRA*CY#z2DEI{A;x6YQ+Or2%LbIZO_5Op zVh@H&!@LF2kwwZlv^h|w!0v9@c8{64Uyx&?|)si zb~vqnrv9pV`KiDCXzHRL`|GCu^8Uh&{z~sJPyLmR{>s!}{>#{(LwEi-#(CUdWqum6 z1U)xpEu&40Q@6vmnvb}4h*aI~Vxm=AQE#zqIa6Xuu8fyD1j z>S)a?e{wRz+lTAN>j*5O`A@5wxl%9s>`FjNZYXBS%aQoq0iuzV8}6*%Vh$Ru(NTmd2|-pMp7*Q+P5HhtB~vJb;(QV|#gh5XL>pQ}iO--pbX#gQY0B>`n>MUqF;tGeWCId4LG-AK|;SHegrR7+&wdyL2 zWQVNGTLLMAmQY>&a;Sgv-S008n$pnfl184Wpjr!~d)c(I2x;}Aih^#IJIrr&gP&IL4D;Ao8bJl$w-sM}CP!bg_ct2Q(WF6 z{!a$jCJR4%w`kW%xJuo$bcGvs6n>)%jJpJXGpu4bRSMup(20gIvPutKLE7nElw zaMG74^mk)P6VLJ%DfgOTzn<$d2`Lu{RjNrbh{PI24X{BmXxDEduDm}kyJ%9gRDE9} zle0HuD>!18`ZT|VZ%WLm3z)~~y#Im+vW!;yM`K69*@(j!CW5c@=1A+$cWeAQuMSv#1(d2H<N%dP3|t5P53LM*GjuD12W?Cs#zso16Nt~0 zaxIBmq_>Ff$~n9qoa!{QMN!YG$y%S6%*Od*YH7Jt+s<;zF4qKSKbjC6Ik%n4D2Lu` zpxLV^Q<`iyiYRs}qI{*Iuynl7h*hcNn^m(bNjy?(*=n+@?pFWh)xn;@iti`G(|?~N z8Le(Iy8TLo6-M3QCVSg3x5?VRVr=6Qt_QiZiqTmsks8>XNNt4rVhAry`pV>Ebp7=D ziv-NZA_4r$B7r>~JCw)MyHx{fpr?DTago5fzcTgr%pw7NL_#DW)>B`*g~o;wqVu)3 z;%Z->`|Vyjue#mKtY3NQuN$>US5)jpejdG5zamvGF$^&+3mm7 znkFOZsx@>ib6+pOzfZQP8VwvlaRG|~$0$ZTMvm?*{x4nwUDqf4g#Vce{{_Zag03>oDC+mYSHw_5Bn`f3I<05)-)wp6 z)t8|j_lEHT4Vl=SvLX@4ESWWnMO#wJLN;h*uve|2Ynl6c0sf`+9H5y#_0=@M-2!gs zy~MtMB)!Sp?B!=(T~v9^-X(?_Bp90_CXAc$a0^$l}!#v*Ykh}M`=)@8j%*GAtWDyc9;rKQkp;bN;2 z(%Mo8Ig}$kA3mWJ` z-)XwUpj_KYNR}(4Z?@d;63Tt)9I;Cn97M;x$|4x3`Xx~e*HG!>vLb%n&q#Ct8a)v)pUt9P)8pubSR*hKAlInN^-HB z4MyL3?&~FWS|wnmaqA^QGS#7&A_j9)er6hihn9sfh{2U3cC0 zh339qGF_;K#5O{TDU^_dQHxE|SJ-D3%4f3r>+MhfNDtZ&0gUR%h1~*apR=j#Ol#|K z_%bBu8zKOJ7809Gpq@vGY(Ofh##%(Ze_Q9C&qad1VV`}pQPeXSr=2Fp()TTw+R#Ih zEU!j_z99qxRAbDwl&E>M@hwIs#lfP8b9T*rUx5UDLpU^{!xW4WP3)8&23M5{axWB1 z;bhKjjqt*A`q!>xDh^*br~i`C!@ii@a-`4{n+&mpAlZ?x#UY)mE4;{@{uM$~6#Yuj z!N<<&w}yPv#L&3rt3kC5OIgW8Nw&z8IKBV)kNWBJaYldtXb}(Ho4QJ;uI@giaQpzy zZu6pJw-p<_`?;N{?jQQ+^U$k){OjQxML#Wo=(kSI92Yv^z?*mXbtBznkN!alVF`p(f{7qVH}Vn({}{Cm(u`bng#J z^DCX9MuACX$cL#V>yK&41VvxSGkFYxdzw53jUIz0k3n{S;SmLzdki8y^Hc@yZyuUD zE$_0kSb(as?loxg8szV3@)|UH4Vt_Lx&4JF;pZx(pl6;e{O;zVsgv+0wnco;8at1K zL%Xp%oWhHm*EEFmHBtB=Jd{<3IQiQv4J)71n+Rlm*ZvAdQh9CzN@A;R)rrgJae+4@8+(Fz@dk+dAPqI5<{C9~~U69UN;n2M5P$ z6Wb0BM-S)hy_-7hMmOOmH{lK!9((W1oDra&c`_&1-8?jP?7K6AmK@zXKG+zC{oy1j zk2a>ioovhBP z(@5_9>K7hS*5et!b^0qeb{PsHgH^X5ka(`T~JLL%z29>b( z${$;7*+32WM)v(axxn2PvQwP0W1O;6oRa-@N10_VGvCWY zgVajqe(%uG@e`;r*ok{SE!)}fXyT)F=+$Y9$yLOGjteMMIZ26ep65OQ%LnOS=K7bV z{-2H|j99`ZmiUZV(hN%-yiSZX2sKl2)u^ipwSNE!txUTi903XM~wYm@(xPsQCsARFmtgMveX{{Tt_o$^zyQ-=DR= z`pnPAw}f{8$o}W^!J|Av2M^l5Ku)_CZ0SHQ(1DCPkWC$g=hFeqLKUS3j!+s_OhBoI z49&${x%&Q=eW8QN%m45l+rC3Xe&Ui0S?63Mbs&r`8Xt2e@66J7j3C|3P`aB(*e~M! zprW75Ykmv7=>oiI#G5wp=4Zs)jd4J}|coCR0$ZoU3a&quVmz1G^dD0sR2{ zp@2)X8 zb>k06g8Y~S%~I1z)c!{Fua^owi!&ma*|^NERAXb%%q@7M|4pvHmZCE$(W&tHyt2&_ zq@Y|6TeH=&Z{BN?9k5T0@R%!^GfRBlM1r*Mw@el9*G-UC1(s!kMd|0wlg>XB}loUrCqN$i6D&StGlkJX^@(iy=EFK)FaZI@+6OF8$LH0ZPP> ztIu3AKRtO`gZ`??(;DJ*g&;jQvlmE^g&5|rO-nXs~=wGte24x#931@ z6BV0#)hpS3$tGk({|sr?8vR!#o@?|M#B&RMelhfCG}IzgABrfOi!N4gUDeoGu=-Xb z)g}5*O1gf)e-?fUnrM|&ED&)f1_Ob7L9qf&`O9;sU_VrGRuw5zb1oJ1E=B8`*knvZ zD@mv_ZSS9C_WQ36a8LM!0lu)G#=Kn;7HKOpju;gRD5-wk`X`HTPX|w{`Pifw=0(XHG zxX}vSrWN>SwE~$H&3xZ|R!aZG2bjK0AzCTPM+nulxO@$JQT=97t@(B4N=KJFTM;yv z$QL&84`ctlzy)HKn@VEZB_Dy@(W0@HT%kF9VmviQjy zmN~r}!^L0@U-)LpU=Fll4s@A0JZLqyoECF$nS;N;9Qkkgy3UKY7QYc0Yo2sU(nxtlV_;`{;-WV zX&an{45iAFODYkJ^UcHvAdNt*dyQElPpq?{6@eBhrBY3W5~4A-Qg*S_fYv_KJdvkW z-Jn3~pAH#ul{v{@N#mZl;0idDCDMSW3q+p4I;%b`54 z!8OcEa2z$GegYKgTC+8bS8r%lGy|e~L52(RC#vuQcFY}*Rk;{Er zspjYwiWI-wddBw6H+)D+#0q?=A}6!NYh!x!rHR*C@$1CvQHuXFP7`}#8b-nzLqRjJ zW`uo+RjdJw&7!8@dHJgQq4hbL)#oW}rH73M_@9?6d@5x)d?Cu>JI&JcD zJMy;^z-MO9#^96}Ip4^p3S#>QE?kui23$^MdsZcGG&@@x(AOFDPpJu&q#3(+6~HD) zw(00F&b@5?@F2&0pHE)yV!qzTbCTmh)EVd08JE=g>6+zHvpi^aQ;Fx+*CE9QjaX`J zruvkrebKm!rD^*9AAj7>+1UTuR|u{DY5Tkz5$Uh_zN#JB($0*L zWLCBcCYV|sXeezy#TwZ-_4AaujoO)f>G$mioG7n1l|A?zGqE$86NYS~Sl2gg9x;1x zo#5$^UMt7g^ap1+Mq@*iHU5z2f<7gSzAxn9WId*7rT57UAG1*HJH<5n<|FhygMv>^ z^HU5#nntQBM#8i~);P4EwEFBj#W!{rKq)F$BB>@&f?%6xlc)ssoj3pd_^HPHUom~? z-}!m}@$+np_}wOo*SZVj1ccwfVfLP-Qt>WxOpXP_pTCEh97kjQX;6omNu*aydUU-AGF*8wa=S`Ar)P%4Gmp!-j#{O@ zi~g8+o+cmNj^WQ9cL%?l0i^@-9cInRY*ZcCmK6V71+v3dJxj~+q>K;0{r2Dg{C$a0 z|0u#=kK*sYhOoMV?xqWlGp05K;oO%T_i9)(UdKZM_2{wW(lm|CTqkw?{kMOuwZ*e< w7~nWGX4=Bjw+v1LYoRSX)}qcEgE?yqz4^H@Y&5^H*DW;uKM)PZcuCIy0Envp8~^|S diff --git a/examples/vacid_0_sparse_array/vacid_0_sparse_array_2_SparseArray_permutation_1.v b/examples/vacid_0_sparse_array/vacid_0_sparse_array_2_SparseArray_permutation_1.v index 48502d98f..d3bca14ec 100644 --- a/examples/vacid_0_sparse_array/vacid_0_sparse_array_2_SparseArray_permutation_1.v +++ b/examples/vacid_0_sparse_array/vacid_0_sparse_array_2_SparseArray_permutation_1.v @@ -2,6 +2,7 @@ (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. +Require HighOrd. Require int.Int. Require map.Map. Require map.Occ. @@ -10,84 +11,70 @@ Require map.MapInjection. (* Why3 assumption *) Definition unit := unit. -(* Why3 assumption *) -Inductive array (a:Type) := - | mk_array : Z -> (map.Map.map Z a) -> array a. -Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a). +Axiom array : forall (a:Type), Type. +Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a}, + WhyType (array a). Existing Instance array_WhyType. -Implicit Arguments mk_array [[a]]. -(* Why3 assumption *) -Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) := - match v with - | (mk_array x x1) => x1 - end. +Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a). -(* Why3 assumption *) -Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z := - match v with - | (mk_array x x1) => x - end. +Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z. -(* Why3 assumption *) -Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a := - (map.Map.get (elts a1) i). +Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array + a)), (0%Z <= (length self))%Z. (* Why3 assumption *) -Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array - a) := (mk_array (length a1) (map.Map.set (elts a1) i v)). +Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a := + ((elts a1) i). -(* Why3 assumption *) -Inductive sparse_array - (a:Type) := - | mk_sparse_array : (array a) -> (array Z) -> (array Z) -> Z -> a -> - sparse_array a. -Axiom sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a}, +Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) -> + Z -> a -> (array a). + +Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a}, + forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i + v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i + v)) = (map.Map.set (elts a1) i v)). + +Axiom sparse_array : forall (a:Type), Type. +Parameter sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (sparse_array a). Existing Instance sparse_array_WhyType. -Implicit Arguments mk_sparse_array [[a]]. -(* Why3 assumption *) -Definition def {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): a := - match v with - | (mk_sparse_array x x1 x2 x3 x4) => x4 - end. +Parameter values: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> + (array a). -(* Why3 assumption *) -Definition card {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): Z := - match v with - | (mk_sparse_array x x1 x2 x3 x4) => x3 - end. +Parameter index: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array + Z). -(* Why3 assumption *) -Definition back {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) := - match v with - | (mk_sparse_array x x1 x2 x3 x4) => x2 - end. +Parameter back: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array + Z). -(* Why3 assumption *) -Definition index {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array Z) := - match v with - | (mk_sparse_array x x1 x2 x3 x4) => x1 - end. +Parameter card: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z. -(* Why3 assumption *) -Definition values {a:Type} {a_WT:WhyType a} (v:(sparse_array a)): (array - a) := match v with - | (mk_sparse_array x x1 x2 x3 x4) => x - end. +Parameter def: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> a. + +Axiom sparse_array'invariant : forall {a:Type} {a_WT:WhyType a}, + forall (self:(sparse_array a)), ((0%Z <= (card self))%Z /\ + (((card self) <= (length (values self)))%Z /\ + ((length (values self)) <= 1000%Z)%Z)) /\ + ((((length (values self)) = (length (index self))) /\ + ((length (index self)) = (length (back self)))) /\ forall (i:Z), + ((0%Z <= i)%Z /\ (i < (card self))%Z) -> (((0%Z <= (mixfix_lbrb (back self) + i))%Z /\ ((mixfix_lbrb (back self) i) < (length (values self)))%Z) /\ + ((mixfix_lbrb (index self) (mixfix_lbrb (back self) i)) = i))). (* Why3 assumption *) Definition is_elt {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)) - (i:Z): Prop := ((0%Z <= (get (index a1) i))%Z /\ ((get (index a1) - i) < (card a1))%Z) /\ ((get (back a1) (get (index a1) i)) = i). + (i:Z): Prop := ((0%Z <= (mixfix_lbrb (index a1) i))%Z /\ + ((mixfix_lbrb (index a1) i) < (card a1))%Z) /\ ((mixfix_lbrb (back a1) + (mixfix_lbrb (index a1) i)) = i). Parameter value: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z -> a. Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(sparse_array - a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (get (values a1) i))) /\ - ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))). + a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (mixfix_lbrb (values a1) + i))) /\ ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))). (* Why3 assumption *) Definition length1 {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)): Z := @@ -103,10 +90,11 @@ Theorem permutation : forall {a:Type} {a_WT:WhyType a}, ((length (values a1)) <= 1000%Z)%Z)) /\ ((((length (values a1)) = (length (index a1))) /\ ((length (index a1)) = (length (back a1)))) /\ forall (i:Z), - ((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (get (back a1) i))%Z /\ - ((get (back a1) i) < (length (values a1)))%Z) /\ ((get (index a1) - (get (back a1) i)) = i)))) -> (((card a1) = (length1 a1)) -> forall (i:Z), - ((0%Z <= i)%Z /\ (i < (length1 a1))%Z) -> (is_elt a1 i)). + ((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (mixfix_lbrb (back a1) + i))%Z /\ ((mixfix_lbrb (back a1) i) < (length (values a1)))%Z) /\ + ((mixfix_lbrb (index a1) (mixfix_lbrb (back a1) i)) = i)))) -> + (((card a1) = (length1 a1)) -> forall (i:Z), ((0%Z <= i)%Z /\ + (i < (length1 a1))%Z) -> (is_elt a1 i)). (* Why3 intros a a_WT a1 ((h1,(h2,h3)),((h4,h5),h6)) h7 i (h8,h9). *) intros a _a a1. destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl. diff --git a/examples/vstte12_bfs/why3session.xml b/examples/vstte12_bfs/why3session.xml index c3e7ec139..a2b13ea35 100644 --- a/examples/vstte12_bfs/why3session.xml +++ b/examples/vstte12_bfs/why3session.xml @@ -2,21 +2,16 @@ - - - + + + - - - - - + - - + @@ -26,18 +21,17 @@ - + - + - - + @@ -45,185 +39,170 @@ - - + + - - + + - - + + - - - - - - - - - - - - - - - - + + - - - - - - - - - - - - - - - + + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - - - - - - - - - - - + + + + + - - - - - - - - - - - - - - - - - - - - - + + + + - - + + - - + + - + - - - - - - - - - - + + + + + + + + + + + + + + - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - - + + - - + + + + + + + + + + + - - + + - - - - - - - - - - - - - - - + + - - - + + - - + diff --git a/examples/vstte12_bfs/why3shapes.gz b/examples/vstte12_bfs/why3shapes.gz index 5a18465596582dbcbf3800c9c272560017738645..eae33b659e5481d17246563456f89a96497429e5 100644 GIT binary patch literal 3082 zcmV+l4E6ILiwFP!00000|Lq*hjvG1d?yu-M??u#ulz`0w!6F9wlDYXhpk5dQNjm*V zkp25**=}3qlI?cJJ(*7Wl2oZAlH!{Z-66V&Hc`T&0+-4$)L2rmrbbFsu6X&WF27y< z=gmSVbZH9^o-XBA_}IzqCL*b+wVbpsd=0(J|td%?}qzZN#Z{F*1Us77=>m4+I z5E|{~$+U%?zg@FJ7$Gn7S#r9X0Ez;}nnJP3RU26z6*(W>)e0r7QJS}pd^8LFZpYLu zkvhTki1G88GEN5@iVnp`FfJPtZ8RD@Q?fa(5$H7nyG39Z=H2zVa@f*g609YXgO0Ws z_Kp;n3`IH4U>zB-!C+crcWdml#ZC)su|G{%TkM$NsMtmVP*xQv(dJ+bXCGM9SLJL8 zT;UpV!=Hs(LxF{A0GJJI_xO3U6T2C=3*o{nWMO&r#Zjb?T(a_y7!RUiZLn@+Y(^*^ zHwdl%nD)i4IJ{nhk85#_-|grc@KaSKshSvyb1M22Ba=hqth2KlA>e8JxUh|8Z+Yyt zJhmG>UBCI$5PfTGLFnG7fUs6xHc$b!fHsBz>hY6W?NF4Q3Ry+qoy(DpH-M#LVQr&J zc(wTNRlT{ps>=@_{`geBJuEqWxViswSNQW?8LeRoEirjnYlotJ@;0+aGuErlCH?J&kbiUHyS)6wAI4BS zqkg;QO;X(nJ$ASQGypDuT7J;E{BURU;|ML!!;qa%OE;e$%BP2W!Nr{O0?ckG%zN|P zWS&^d`?a+gdEOY#==*K^c?weVUHN$PwTxEDE;ft&eEwDha{ov9`1#>~3*SCpZ=ai$ zx1$N?*@ACn?@!C#pE3piot7Yor<9um^W6eMOL#ad+HZ=$|i%R=2{%A>q+F8F zdtZ*mG`L($v+G!;PsKDdnKxvBo1mt5K}~mpnm!QJU>nr*G^ptzs6DS5yH?=tXHjEp zcZC;IV^cIja#BD-mNLo~DW(!?QRz%ENrJx@5@h*(x%C4@n$g~+5YU@Rt7ApSQkr97w*08)!uuMg@nzvrO;soFG!*@`}d8Q)e2wXYG zh{_MSOwxr6=8|j7`Y2!4$8i(9*X=po*38r%^3L#v%InF8N5Id{OF_*0T>5=7+S1u$ z{M+}NgT%>~-zOhdtQe~}-^+~6ffDC5oVPsY6QbD7hxGxGOg9Vr?(t-Af^+_Ma~#(Z z)D|vszJ7$}Rt4QYNz`IqBcr{2%sbp&=~+(T#nT&7aQzy~_%X z4XAxEp$4>tRjSCu9^w;-?{j?SU8JCjRl#a0UkZ996^&FgUZXa~J%#d#2J9QPWGBIe z!W46M9%HTOa`xIJ8`(?EL{l_}jD4q^&?u+){P|2uV9E(CI)R@+o`Q>BN2OEoNvh%r zk_J}KfCTEhgKlR&E3Cbzkb-wkqm4yMS zWTGQ42@Tpz8j>F!MJSrte>NPHfuj(flkqaqrIK0y%L~#W*X`u~ftws;L=5s17-)5UV-2 zki4K=#&u-(*5+s(c|}C4tn{FYSTMYefetB^D7rn8_8{)r=bnP7h7%cN>gw;8z#(JZ|~4!y5N0fwP23$?J5Jp3j_+vg0)~2Qs}Jp`>+bOBo7;U1)Do!GX$nL8;ujhY zQ0V&_g0kPTKGuV46aav2we*HotBy5^g8Mr!LdO_A)(; zFVjQ&+!I;29ZxuAbL|epm~*zT&wX|7Yx7~~G;b5})HSzO6R`DF3+?)}^_@Z2`5gqF zdMVGk+d}OIOz(`{?a$I(%d_24(;d}AJClw^g$gul%C}TLud>w-d)aHpCtt6;@2Ed`c)OhppDJ*|w!jJF0_VBKZ+d!_cQXGRc$a0POK{oGn8yT^0#HAsrY49`5X3x}H6A!2hS|nN1jq zM;)|E0X1hpbSR0nfoi;0O@;FdD#I`4bii5flMl)$MsG1jjE-_m991pBw93%)7q1e3 zX%deLU9!XPU`h!L%Am3_d*>z0Bvo}Q@xL5oeggIQ#i9cid{b6-G_-%7b$KUpFb%sZG zpWmi{XC)w+?6cHIiCjp-FKDu|cIX>*+SQ}?BaOC!@2cCVzpd@79)8vl4xFc9|2(aq zvK__X8)Ni`&eLeH=eElXT>m_+9Uj_}dvoA+JmnNm#+`u+t@aPp#s_4lS+EC?ege;Q z=-~Bd^-Lyf$yBVX6bTtPfmgcvnj#SzPbc!$pUWavUgFgv_AEmES{9+4O{J*fps*^$ zUO@p?lDQ|WKJQz^_qU2lEVOBe%F3F`x_F8?I=}>qFov=ht1s6_d9gOCrjK&eV7YAr zgVj&T53~bq`Y1acmQAagZCcgL>L>2|B)Mr9o!i^TU+JU7$M!;;GWxte%47?B5PyrF zAzLn@SCC55wUU$wqZ;81u*Tb5V}!_(Q9-oIX~N8kZ5^79%fVvvWbfqgdkD-{c~4Hc z9Go^O07FnhIEH+b-~(Ng1zjlFN}j4~U`Yd`GQ%HM82*leC7+H{`-FbUN|Z{Kj2EId zzEF~!lU+>09j$b+Ps)G~cS=HqN~O3|FksEdp(J)TlPwC8#j$tTLivs!Nox(SI)?}) zH)aQt(`OJ-WR(r*+F-hLcO*%rfZEy|i#57}6**y*I>OeRSk=pWCfTjBt|%2^3Zk`y z;6#u%)}*onH!57t$>U#Bkk=IC#ibw`H5N`$vhk?M7yxmQ!%xv9C$UPW6Q@Zh3gMS# z60ddYYn?iaF;?Y(wWQ=#nIXR^%8N}zQ^8xl*a=$JnI#!fj4_e1$SO-TtlB7tUgLi3 z`+HB&kUXnY$OJ=DA%HX9M_|cCq;9vN_Og%Ff!Ry5`PVS`8U|-7uyan8>bMkbN$isB z@KZEO%r@~;&x`wfKB|5PTEbQa(iw*H^|95PXR;xDwV~roH=Yh&6)CF5;HOQ4)B$zzHlA(y4vb|Gh5j2bti Yjl1Hnf4H#puO+Pi17q!D(vwsG0N3aTf&c&j literal 4366 zcmV+p5%KOHiwFP!00000|Lt8#ZyY(YzWZ0`J{K~AD=_^4&t#LYYV#FsR`Lkb4>hFzK_&3Rt@}0odIb0Q zdk9B9o32FOmx%RU zJi@2Rq_vI^+Dehx4pk{Al$WD)#ydo2pBtvWn{ zWm-d200|+0mmHH+B3aL=kuvs$%f4_u6fVessxAC7sA}OV@Ux(`=I7iQhRzADyigg? zOKWTp9>5?nJ6NZb+2L>;J2G`+dcVIa$J;|g#BiOeN;W{Hg-eM?BN8gF6{qf~yh_yR zT}Iazfny#pH*V8;u>B#5efu}m_^RrQms7RMkf0%HSc)of%VMzEWDTX1|98|)rJ4KJ!|&;~x%u1jCY8Sc!?evdr<$!B zEc7WT4wF@puF%l2ZRYkw=3^PS=z*(Z`b^dBq7-0FDZu(tez|{mN{>%J4@?I~waSM) z56@X?A4QDJIA)B~G>9U%-p7!Gy!m>6|NVwua}Rg!+Y_bko)(3-z2;P>d2It*h|Cqu z(Sg`og+|>%>>{IjpA0#0mQ3I*Sgy#U zI}=by2nb@sf2@?$Zq=1l6Z(*8o-aZ$-biLbj3(H`lTOO=b&%{7RqV!H8`ngkN$3Ny zfHN!!&18a{QEQMsWjrl;PBm+1+qIP)k3mPB80mQ(gEGXmfH4QqP9&|?R_^R0iUs@B z5I@E$Jg^Hd4M}l31tMP!$MC$QUmI`?cNN{;f}^`>YQ4=+Z(ZxHr+VvJZ#}PfFA%#s zwq|AL2o4Vbn}zOy)jRxXz6^=67(%@-8YuZ?Oqts?iqkTT3MIro>ct~qd#5gH0nnXK zLmi4f9BL;fqnDSvAmR85^-j6fgH&6>kfkCaT6?VNdhhZzUGnZ8*4=W%@USRiwZCr5 zGDx2qjAlkyz#Qe29PCA@c637*!~9(9f5f^v@=r>4apZOs^d^@p5O4qiDfwkg$u$Ug z5(L}^0jWwO2qis$fMQzyDKEDmlzUqs;06e&j&icA?83s!*D46O009plR0_sKa$!m* z&!WoG1QlZ<$L5UJ_@+~t-PNsU_n->*+F&?vZaGB9O!7Jzp@EV&-|ruvYFzy#3vI>f zue01%jQq_kw*|{(B0vD=tBRkhS6R~B^CH+98G)_aBT%jmK7R6C7+d*{P15pm^_cj!7I&- zrwNSZS~417+G^`;vZHBye!TlU?fB4#!EKVSysInv#QLSSH4Mp1yIIkRA17OJ))>w- zOIX9x(B{U~EW0kIS@c_*pKS8uVwU0X{CpLCbfwU3xR?~Q>#~@INU1)D2DByY=C|d| z2ASG=v*2n=w>FyHtb0qkgsXLLy8)_gdq@8otRCXkre&*0vv0(V4%n6rOZ{dOG2a;= zrYfjq^TltAdxzT-J)!JopqjB3H*9li8__*_Xr)A8H7oac_wCFy9C~C(lUk{ni(2QTc!1=R7bx0XhkaL5KJ%?ub!IZOWBj#x zVRnh?P=Z2Edo8k4j0xt!Xb*}05hluc%i2Ce0zG<~Wuj&gBB7_F6^UFrm*9mC(w^FP z(JInc4_ST1h%K?POhOi&j4o+yL{uU%YN~cF1t0My{Tb5tPS1W_=-Um>IbC&U&HRis?H!6^w$`b1f`Uh(NfR1Oc}-U1~a|47GKvh$X7^CvpsJtDw8!7buPdp znsqxJXKb{A`;XaZatK^y9aUy55rdhO6#WAnrIFUd2C<(Q4DY4=S9Wu&xn}4&xiiKv zD5D*@G$@@NFp0eML8Jub5SkidiFI|?cJZ%1rN_O&^0j9AJnjG%hqak%*hU;qnyItW zm(gau$%c5bJQFX*+l_d!tkVj4oE}zP@M;Lxtpa%RV-4Vr(LG&oS$ULct2N96c;sfA zJJYcOGNAobgUGVRcuTvcC~D`a#yJ-273ga21#Jm6FpE=6j@rKQ8rDcM&I5Rox|Smq z=XgfLZDtm2z>qxC%4bxWCjDnuxZ63FXy#a~+nY??T+ZfLZ9nJjzQg*wnC(|MF~`F7 z9IM;D(8dJMOs)B9j>XD^nR>`#idAM*vr3kypn0+9nB_*0AI{~P>pYNhCV7-Oc)^@b zf?4W5Ma8Rx+HOq--V4C;g#a(MkNj`|U#GtT0_jbfpbF15WsBvi6&C1K9K)Z`YY%GwdQSdglo-I`dn9FiDWRrT(4U|7x?UgfsyaxE8c5i6UO zQkUI$L#?IrvW-`HSHQ6B#-VuunyS1>Z~r_p{%o1D_V!_Mj*oN5!Cyjkfza!rA*riR zsMZ5Hy*(VBGSz3=5o5iA7*vIrl6GV5aUL&g*B;HL*91*>KGn6qsfKorFS6EelD1)6 z3tx*9dBgIYov^Z-*dmOM6Z^&4F``=Pb33lX$uZR%46C_uk|$WrO{rFFVL690tv{M0 zPO6}+>cO=BXsRTd zBhJEZ;VkSaoF(7HS<)Xq;9Sx}9VE7;#r)f9C4=9N~W4@wIg*( z62n6XQTh~8pjjaI+Q{T)^WMLffV*8JrwEwqN}+sMc_Cdn%|Yyx)F<6npS*&Ai<=vL ztlc7DezHHnc7N#RAfF~rSP2;B1PpDD=yr^3`PYpeQMQphN5D|K1jrKv40;@RFfMde zbAze_530FA&3L2Vh0+i(n2CV<-62;IFw}twn*$S00)g8=VDVog0Z#)H=K~X47`i

CVnqSv+Ym6SGX&i2GP#<7dxzAg21i^s0->24aoq@nrXgU~5HP=tfT0pF zY!Wb>!dZw-oQqQu1I_{~&c#o(j#f1|7jL4r9IamC-1(Si9IdI2)~pFQK*Ssb(^*6G zGHaV5vFvly*-IDC1s=JqBDo|N2T0zCmDM>`Ui0c~`<|VWy5aF@!(M&cUL%XyB#YUm zEM_NJ8MaxO)18r(dBe)MU}e#=GI4|0Vr99(%JKqMR+W|2DONU>l?QV}H8<#qm8-d7 zP9~t2tZW-rw%5yIR%J2Ul*K23z-=JPKEDx&veR#5Wt_8e3qzR>Y{7sVFra*%l`9IU z-iVd;IaW3=lEpO+ErvKW)<85)k?1mG7|FX~W!|tdT*k^+Ss6E38BemZ+-7B(4akv| z#l*^L&dR!FWpZwMizAw-p3Vm|3;Ng*q}TFjJ-1w=JlK$M+q{R_xhpCjirz4GeCyMu`} zsT(?u4)le+RS+?Z-{Epj{)1n@$i+ZdfXK2V7FC%AB$yscYvp7l4YMY#k z5+2D}PUNiTxQp^v=^ePwzbaI-ZVNIY%=T=^5#1M9GaniJYE;@NG$qnvv*7d#h8mqsfZc5_fXDJUb=gGUm@IA2-Cho zxUUfID}=9GA@sR?{@OdsnG(_@;eF=88KqfJj+?FT94wE@?T4n``=P1sKaLX4g9JxV za91K)kuxb27t-3TBg*YD$^G2pdq4LmAt~leiW;0XXod7i2JNLPpXHbzi))JAPdvW= z!JCX$!Z`pM#4ZSLCBqasN|uz>PF;Ei8a}Q7XurnOeYUW|w}zp$`ODzO7s9>x{@@P> zx4dp7XB}A%zUR|>X@{YE^rUtg%iqWu<*`#e-G!m z;9_*%aqEMQ(TgB?P{Ac)KJOQ^kfzvu6#YG;2(k!*Wp6Mhqon5{a-L0)ky&eXx^a&r zIr@*Z4HN42W1@faC)#|rq>sFD+#?7b1SDpYcF_cg+VlBm*=Aq-y!~tHf1Q^9f5Hu! IKrMLy0BI#_`v3p{ -- GitLab