From 13410bfc8fc37eb09a1a98f94de61530b4605483 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Mon, 24 Nov 2025 11:22:11 +0100 Subject: [PATCH] cleaning --- examples/numeric/log-sum-exp.mlw | 13 +- examples/numeric/log-sum-exp/why3session.xml | 463 ++++++++++--------- examples/numeric/log-sum-exp/why3shapes.gz | Bin 10763 -> 10810 bytes stdlib/ufloat.mlw | 71 +-- 4 files changed, 269 insertions(+), 278 deletions(-) diff --git a/examples/numeric/log-sum-exp.mlw b/examples/numeric/log-sum-exp.mlw index 1af5e160b..3a839853a 100644 --- a/examples/numeric/log-sum-exp.mlw +++ b/examples/numeric/log-sum-exp.mlw @@ -423,7 +423,7 @@ module SLSE begin ensures { abs (to_real u_a -. a) <=. 2. *. eps *. a' } - UFloatLemmas.usub_double_error_propagation (uadd x rho) y u_a + UFloatLemmas.usub_error_propagation (uadd x rho) y u_a (to_real x +. to_real rho) (abs (to_real x +. to_real rho)) eps 0.0 (to_real y) (abs (to_real y)) 0.0 0.0; end; @@ -434,7 +434,7 @@ module SLSE begin ensures { abs (to_real u_b -. b) <=. 2.0 *. a_eps *. b' +. eta } - UFloatLemmas.umul_double_error_propagation u_a u_a u_b + UFloatLemmas.umul_error_propagation u_a u_a u_b a a' (2. *. eps) 0.0 a a' (2. *. eps) 0.0 end; let c = b /. 2.0 in @@ -444,7 +444,7 @@ module SLSE begin ensures { abs (to_real u_c -. c) <=. a_eps *. c' +. 1.5 *. eta } - UFloatLemmas.udiv_exact_double_error_propagation u_b utwo u_c b b' (2.0 *. a_eps) eta + UFloatLemmas.udiv_exact_error_propagation u_b utwo u_c b b' (2.0 *. a_eps) eta end; let d = -. c in let u_d = uminus u_c in @@ -458,10 +458,11 @@ module SLSE begin ensures { d' <=. sqr (2.0 *. a_max +. abs (to_real rho)) } sqr_ge a' (2.0 *. a_max +. abs (to_real rho)) end; + assert { (0.5 +. a_eps) *. d' <=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) }; assert { abs (to_real u_d) <=. abs d +. a_eps *. d' +. 1.5 *. eta <=. (0.5 +. a_eps) *. d' +. 1.5 *. eta - <=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) +. 1.5 *. eta + <=. (0.5 +. a_eps) *. sqr (2.0 *. a_max +. abs (to_real rho)) +. 1.5 *. eta <=. exp_max_value }; () @@ -473,7 +474,7 @@ module SLSE begin ensures { abs (to_real u_e -. e) <=. error *. e } - UFloatLemmas.exp_double_error_propagation u_e u_d d d' exp_error 0.0 a_eps (1.5 *. eta); + UFloatLemmas.exp_error_propagation u_e u_d d d' exp_error 0.0 a_eps (1.5 *. eta); end; assert { u_g x y rho = u_e }; assert { g x y rho = e } @@ -635,7 +636,7 @@ let ghost slse_accuracy (a:int -> u) (n:int) (rho:u) (a_max:real) by slse_hypothesis rho a_max n } end end; - UFloatLemmas.log2_double_error_propagation_simple + UFloatLemmas.log2_error_propagation_simple (u_log2 (u_sum (u_gi a rho i) n)) (u_sum (u_gi a rho i) n) (sum (gi a rho i) 0 n) diff --git a/examples/numeric/log-sum-exp/why3session.xml b/examples/numeric/log-sum-exp/why3session.xml index 6072aef2c..a5f8f857b 100644 --- a/examples/numeric/log-sum-exp/why3session.xml +++ b/examples/numeric/log-sum-exp/why3session.xml @@ -7,7 +7,9 @@ - + + + @@ -44,114 +46,113 @@ - + - + - - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + @@ -160,516 +161,544 @@ - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + + + + + + + - - + + - - + + - - + + - - + + - - - - - + + - + - + - + - - + + - - + + - + - - + + + + + - + - + - + - + - - + + - + - - + + + + + - + - + - - + + + + + - - + + + + + - + - + - + - + - + - + - - + + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + + + + - - + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - - + + + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + diff --git a/examples/numeric/log-sum-exp/why3shapes.gz b/examples/numeric/log-sum-exp/why3shapes.gz index c467f2a6ea2b09f4588b1b60b0c7e0732259f809..bbf5420dc2e9efa480b9430c40c07e517edfb8ed 100644 GIT binary patch literal 10810 zcmb2|=3oGW|7U9>^JCmMJ+rQ7y>FxJSoH4ngH?%142>)u`}CWuREwrw-Jlw)Yy0WX zub)ci>t0=P+H|9qciJnRnSv81P85uP67)}g{kr{s<@Qa; z-$zaR535%?{OFwhVe|T%hA;CEt^QD4Q!IS%;lHmRUOf+a^?cQ#&>!E{*8Jr=D81F* zuHGU-@cpx%l`r-rR2zuy|MltT?eAZH2LIckV0Wb;dyd@j;rQEdE{iuuSHOB_@WZRO1NPVb`~2|n^7jd=KCI#V zT=tlC_NuR3lJYY`3yVAYA}<)$Mu!F~yeJE;Q#Rc&??B(z@4nIjnc0#jHh=#+_4SmO zWt)UcLe$p1FJG5laJ?`>d$N?V;ZyBpvEm>643bWq0PZrhLCO)|T@iUYJ-ON`vs~=jKQzohh53rwq(O%k#7wmW&T{=ZprVf_5NSHSU1b3Jlg1I zpjy3y+J5!P@@>WbueY1k{VKc~D5wQWMXZKZGitzbC3y8p$cGFKrf6@KA71|c`c9QAKfP7*?GO0*@Y(i_6GJlNo;WQzw*35p>-4u{%1rIlIIoa7fyQgsP zq%-r5)dim`#A2<>y8L@@aPFU6wfc)h@QObf4Ayz(N0tN?b$v^}zT@@=(LHiGsjF8- z7|)h6+%8yk#M(^ZQfOw{#^8>XMcljQAOHUDW6gYptnOKR*StPpX>;s)ZTz2k@6;a_ zo_^oCiN*Mir$WcZ{Fic!)dElF**%W-oEUx2e2s$OdDV*x`F6X%loZ^xyIdn??eUyO-ae}DU&0u`nE z{VP%~yKZhgHO*c6(nH-XTNW9az1eR1VTPxTn#J!_InA#+?YCXhjZc1$lbiG}zvO4i z3y;2hQQ7A;cDlR&O+2!)Icf%#A&OUN)f@1Gw@7cUJg|{kizu)A` zw!S}jzslO#r_DaU`(0o6|NQhfn-72dlXUId{oswS50-fb-&$;bhEr*#crvezl~b?U z^}M)-TTeA|uUOv`&UGs4|6eGaFQiwvsHOVelwU1;^6pjM-)1(x7diXqFK_=%F$K%+ z!(G43Uge4YT5#q3N}*Ky3y}hee^Y+`>;5@qvAoBnHNEo7f23`$uQPS`7S{XoSHX3* zbd;y1=Q4TCNPFYu&z&-7X}r>UP+ET9U%vNK$4r}T5B)BtHNA>j!Fpj~q}I;Y9Va^@ z#NV;=maOUg^4s;moX2y1arf}^mvx_9SN4DFpN|3i>T*}g?=v^Ny5RM`H;*FY-+QcC zxBt!0XTMG-r%&7^_4mvL_gSvLBS7# zztGV3tZ2+GuJ^|{7kzvGVXykXO$TFze`&35>+$zDPmk}eUL>D$qw?%+wtn07ec$Yk zAN+iyMn?7JaoWt?y`}v2bqsJHE1P?H%&rCBiQ|Om6GWIBk)v$vr<}V;x9|)qlpil>+D+e zr{$0uD|5-{_6dOpXS>ta+TUnjqi+`A969Qe`DG0?;p1bO8zL>H+A2)^2{&# z;kyG)NU!_0u!ry0S+>LT4_`L-URH0dao6o&bIbP3^C9JZHYPWBUbq!fe*E_SoYg`; z->z@pviMP++T%TkcJWC*dhFGA)G7MQ+`ao}YyMdNQ0rSG9fH zr!RlLQRwT}n6`3VpNE;t*Kg}>{Bk{i+lzVk4$LWcW-^lRx4!qnl*?pQ=Jmr41zF8A za@!)_>c48g%b=3MT2j4jU2nY754S13bLKCzH#Cv|#Tj7MRBHC1zRFel(u>~@=RfS1 zPwiW*(e(GvrRlSJ9jCNs%-?^m@x101$G1_2H$TT6>6!M|&TQM~)&u>`>+jSXdKJ&n z_*E5Jew<(6ZC9DgYbw@a4 z_n!BOJMJy$TAsbiee!|S>tFo0ABj|avT&yJuZ!=tUHtUvZpzH`1`**zhaZBWUnV#q=X0LO% z<`;C_KlQEaJln^~G5otWEx*3UQt`40{|}j5nHlePSFo4*eU#*V_uYAI?6aJPxfl6Q zE0`5m_pjggJV;OO*0foFw)K>JmhDfTxSE-tf3jluXVKh+t*`T@zIe;Syq>LE`o`z< z;`(BV$~=oz7w?vBKT>!&UZ5@NgzfWf{IQ%9{_j$Ke_7+)^SZe0(`y@~j3!T3iO)U! zNjFR44Da*2Jy99Y;uXD*zx?`nM(@_B!cSXsjRT}L^Y6{m`uNHxFrO_jeA%~B)w`J! z(gg%mO3Q8ZRh{%*W3A1D>b@a>2THj`t$N(@K1-^4_>Os zY=2z7``_2MeXsxJ$ei8qWxB2Hl#98(Q%+a^D!KF_Z_{^P)6i`@<6a!Q^sUPJ?WW{h z(b79}uYJ4Hf6T(`$HMGa?e8K^n|wLO_BDSQ*I_$_Ti5c>nuxe(vqaOE13Eg{-=r@}}cg%I3>g zk9>D%?0i4pzQDih|Hr@o>-OEBx81GvX73y+y8_D(-!8BnZ+?zQ1&IauvEZ!haY zLFN80Vw0Dg7TO%dK3mAjFy>B=led7Lmws+C&>+_^GToqYW zT(@(o@0v9ae<$i5u?=l!UnN|hdG(vZ{i{5iOhgLroV&!sZCdwv)$ESU{a50IgY@4@ z3vD-FTzhv*nT~tS{RLlBG-t%L_TS&dvT{M~{!;hJg43jflpAgydF8e5^{ub3*XO76 z^KY-)d^Wo@cxU`H$L0Dx=1c8oZoP8qpr3C*!1|jDwGaAz`<3-IE%wKR@U7|3ADeyI zb6#)p9nP|3onNVz+jjlD=WEg6)6{kO`p(ctkGuN2z4OJw_J93hm@<9yT}z+k3qN_v z&J8d7q#%7LU&wa#mxWEwP5&9LneS4V9sB3$i~E0mhm?O7TDD>9@&AR}cCOofQTF%i z#BSB~^B%AMx#q#Eze+QnTzu|x`p)K)+ux?Xb#{6Z7<$_Br1{-bmjl_&d_TVNuQ9u& zJ}uWdv-jPp@{i4CLVvGX$-jSj@ymk=M$3gRUwz0{D}H>5+9Tzu&VPOhSk%Zr*}8do zWvR)xbK>Tu_+ExIQ4 zhL*`mqg9E!-sD?{@^ne8)>HXayEm&q?~m;Br?XF%=GB?L-SO?o@{1Sawry#*mGdpJ z=8nE_*TM1ZdE04MS@h*j=gH5qk-TXa*%Y?U_FB=-lMfBI%vv0{=YQm(~bwo9_uEIx5|=DO@}T@UWBeD(MI#JMXf{yeRZK70R<_nG(aHYGoMw&}?` zw|=M9o0;W`jq|tekX*1W+kPg;o=gs*8Ex@bCly-X*dX+Fp3n;BVpjjJ$IYev{=Hjs zVYAny8>vm_&hDT1Jy!l<`JvKkgR47i=4<}YYj!n9cl|eOC;Kz?T;-qm z<=1`7OHY0NZ(H^Kuc3mU7b{4sum8Sk#==wCO7(HByI$@+-NSZu{%QB+O1IuK);)QA z@?HIfzxL1C!`U4!m05ju*1r1XoBZ*xrJUL2BD)sdWjS$g@!`$F={_xMR?5y3>i1R{rBg1-O{->ftmle|1s-Wq06yD=VIN@swIo$K6f`%TUBpQEtNKTHtW`k z4gYi}8C&J-KjW#i**Mn3)$(D{t^c($G4@?|e&*g-ReojCcC9zPudlkiUG?ka!b=rr zw*8*JYO{y_vQz%TdCs1X1-oolZd8j?pKw1|Jzw>&%deZCzP6s9{{GD3 z=l^rRRKC;vCeOcr`(*FAGxoRsyeq?hX8!q>TGKhNDoW(#1s2V%o_{}=tMR$N=%W{s zKbM=Q+p4J7mL}Hhx!+<}oj-l8b!)>nule^ojx#NLtH%HQX;hNg{z~IFyKV@7d=YY_ z$U^7keyKFaFx{Mr!pHRz8%!@2I#jmzNxl!ZUexihUd}jn-r^Qndw0&uaXrjhH%|7( zN8eZWUD~IWaGYN=L7{B_jO}8#)%Dw+y8V(rexWtPdqei?`Eu`{G|tzHmJxa5_4bM8 zhWlB*x>7OUlWsT1yla|pI$7FS-nDnam*T*ti{H;^m-+{Y9+6TBQPy91@BaBK)%`-b z+roFu75M(+RbAkvlH*Fs`ck;_5?lnAm|M#2J2@maEf8RFp-HbAy zw(IxDxkqR1x{_I#^2woQ*7UoZJvizwa0*{`^#Ap@ael~+Dc5p5v*i@mR&Lo+y{WhT zh1mX%LeX3fS60>p!K4pylCiA;R&J|n_g>rnD(qg@Y7S#_H+9WQE!9dn@3S{Q$~bI| z=xkc1e`?1QGdEEduaI|3R~>x%YHmtb_Ox|(*UEC=elus<%4aKLdHjwZSXChNc9LWC zv2{ClJpHq3$&6K{sv2>@9X=89bIx32pWAaLqj%TSPhG7EUM6>{B4avdoqiLmv(ZCv zY5BKVv!mCopJF&oI)3Vhb59R-Ke@mlCE8@N?N|1@yq$X=X*seM001xn_Oqe$f?4zdwoAG&5={=B`w`xhB`NNpt?%fQ2#Mb=o&W?rof4`TWA7 zzM~TFck&vE%og5~G57UpZ^KZ|OV^TGo%6GA^yn{)TIVB{;U%iMh*jvXzWCHBPqtoB z@zr}_p{l#8C|pGUnkx71i`y^V_X^p%{n8z;yBTLVHY}K76wtDw&2_TU`MBQ?e4p@? ztvxa0Ca08@ar=Q*y-gdIILwWo*<(A zxv3_#!Ao#y^Q;Xw(-K|NY%UqJ1$Iho(Ne9-bbhzygGH~*s;2CRnpTg6r|&x8tIF%V z^@H20nC$ZGU15tia>hR0BF-jvpquBrT96a_EhQewnV+_E^~#&hZS9ESdbxFDW})-AtsmHpU>6jWIOEpm1l0-#n%V!AC3-kopR;JWa+Dpw<;rM zoD!|lvO+`afQeInNr z+vWnrsHp}bGYeELk68W?Z4|irYxZ1Mty5Y)EgL6n%@Xbk*lO`(%PN7uMasITqm}zE zP7s}TjN6ix@&26DY1hJYd2`gbEDEk?%u!;#KXvAVt1U7n#vFEg6uwl(#kQU^5W2DU z>ss$Ax>}Mus***Lq>@bBc>UL;oUSz6oBHs)0?VxE%YSOm#jH%q?X;}8@I@?1TwXwU z@%aMDSl!3pw8Y{K+}1QjUzqA_BAIYXZt9M}ZIx-=_GQ_B%vxu7Znn}qqPKwQrNkkJ zP{V_J4`)|o+&mSnZMI6uKyx)$vg!t&Wy2ic9Z|2A*UC2oU((`6ZV%~ZD$K-tn<7R=ACi)&aK058xobujOSlq z`f>cg7F`B*zJ+F?^G-gFzMYYCbzRs2=R?d2JEUFQTWXHTO2)R@3%Lfq?K_b6_QaO- znUTCa$Chm8*}AzU{jw^T$dM8m5kUru!$YTTW}we-Lu&v3uHR+X=h ztbH85>QIDngX_{C%LNYgd}FXSlahS+2WjDoPik3k5%Tm^Z%JHSLjK#gUSw9ILCE!=5fOS#dyG$}RTk zpS8u+Uv&c1HJEoCc~0tm8be^HAtR zzMTh5)!%5|4P|p%b3o$if$EChP1hK%9%5S>a&BVsc*&skoE;n@Ny(ZW)3uClOlG~mWNN>F`_)E<^hXAQ z3xZps1S6&wWgO9Mkm)+OsAvhVtYB8#tyOXt)fo-0WltCF-VncRfqFiZOfid3_SLh7 zLIqWfyVgmlXiRO4nad_&u*fR0D{b$4OGnlle2b?mdY_U}5LG((a*_3eZWRUgY}-bk zhMT#%2YeG&yy)6-h*vdyPnxvhtOpJ@tl|gGC5t4nmYncn?@r`;9m4Z?f7bK_mnp#} zt_r@&Mz2?0RB{P9@SEqH-NKJ2taL8;w`jWF3zd!e&!`kIB~)^u+yS|5EZL%ttP%PR z%EnuRxGi!TgEsuV_2ezXE}jjmTEZR0nRZ6@f8nyPxNeF=-o*_D4r-+x2V@hH z8A}=)6CQnN34ZB0}2}gy5muzzO&684uoF^*^v(0Kg z-{T?0oG{P5N^262t!lNLX@&OL3Es?$9&zn6jeaa6jbo9%WJC#>@yd^eUCSI`I zaynCYVw2bo6$Tb#C2l{>mu9RLT;~L*GL$q<5;gECV3;do8Mf&_-`SKSnp$RIoh(ev zvW?=L)~Dwk3}t%udqPeA=A;ri^_QMKwk{^I0tUTLBs2Ac<|YXoSmWFFNIhTViJ_Lr zZKH$ln^ZJCPlYnh7g1_Zw7>a=!;_Q!gtOFUSH;2#!A76+ic*Ft4NMO;H@=bB5}f;) z_0Zf!OxF{qxW$CH9%hKtb#=%!rf-zlr?U^+P=J5(iIOwnz=X%LIp`@QNJ2v5tVRD7gsh<%h zMVfw{TD!#L3&l+536!~}x}JKnXn}~}0ohE&@JZ~aI(CG}9=&`;LdLia0y|Fa3|w5X=KRtXjSm^C1@0w$mN+r1c?)ZmGgI4ybxlUGI^RGuWsrs0#v zCZ|zQ(xdpF+xJIypUZsjde#u00#@HC2@30y`r%HW@{da_5?9t(6g9;#3hdne z;jKY}UXjzJ6BPj;+!roV*s_8_OFQVO&I9Y*C-YPltnyi{^x64rrUwcnX}545Ry`)N zsjOLtZ=aH9AcJ^gKLc}t>j8 z9#Fh!6Xb9&yJ0PZUw4~nquXoQlrEV{rRyfi?%yX!-IR29J3nzz;ggJ*pQ~jSc60n? zTxiJiqo;)beX}29()R?Wo3A(htK4Gi(7VcGlXhwe566TvD~fv0_{@AFox5bS|I+x1 zOF@U78Q(wUQ8*j)Q7i4B))lQF_y3hP6V9pklrm&El%*I;B%fH`xNFVAOvURT15G>LCYv+PT-jr> zIwSPhA>mS~&;E;ee{_U!_AS3u(y7+Y9Wr@h(xrPE4E8e%_J6-70jU8GE_mr(FW}MR(?ig(~gQ{IGG# ztO-5q4KXMT~@lY~ETDDLh!aW*ER;->dD(Ww(|OE7L(WS~=A zIO%d%O4Gtub$y5T@#H5PIn3C4f-y(a;W*Q~6O4Mwj64iGo;2#Liu`D@`Qt98^KSWj zn&&cv{ESe(ZnCre;T=}b)mC!;l1wXI7OeAlcj8$`L!(qd#RfrUmn*ZE)*1ax&{Fvp zIWuA_$E`~yE-N$IgjhQ|Y*w&JX3sn0)cS&}VKLVh2k*5bZoC~=#~ z{Y^ydc;hW(GOOtE z%Ns|38XY*$wPr4NWTc)Z$9zed>5puR@^&jejcYRxXyH(FWqzu3cnhQG)|1;LB7`=r z>f2sn_^;!V!~Ut8yG&FaIXWFz#)OzKw=L=3Gu1h?oH0yjW~|UTp+o&l8jJx4wO!xw zRJJUg_}<~r%f6?^Hx;WL@`6+X6xcG|{;B7mo*B_u13v&Y%LO9!uSjqmM(G+e6D})R_5%6FxDW+ zmo3+%9=maOUeS7Jf0tq7bKBpiH=Vn8;MDfwZ4#Uu?ah}-aPHz zxZPp((jfWSJx?q(H|5Wo%;vRxYtON`y%N<6Zdf2RbRi`3VB-Vh^J*@aZ|tA* zvXIZE@nEWeoUU*5rz9^q* zbm4e3>G77W6Vw$}9E;n#g5#d?5|4cs{&=;Xl09AEb55E?jbGrd)q|%;7pSWBn@mm; ztl6+dP+|Ei6`Pjim^kid2k*rGOxjx{VR@^~BYT@#=n=nz1`}3yJ(9ZkIIN&7m3yrb zSH6W%*^q}C@ z$y2*a1Kx?3s+>Jt@K8kg?8cNy3!nBqiRRPDSm<@ZX=y@tR?{>287F2bJAXfuwpONv zD^N3IbHE&-EnBCrI=8CwKw^eeU0B4IM$R)Y57_wlJnxCixcVe5bk?ObGX?W6CzKZX z-eW6qpCtC8r&L;-<*mGRfc#6H_L7XGG^zV{SeKl=P`BuA=e})iQZ;mTbY?|kUKL!7Y;Nw=eetfZINz-Z1%4FM#i)7EctXm&6 z@r{7OF^!ZdOO$OVT--Ism)EtZT(^PW&~AMMpXT9!BwwEmj}m@tF=u~gea++cuG?SK zo-AZ_tT`WcsrL-WQN!I*6HmMh@@4tQwS~85sh@@^*Vgd)B8d~!B`ZWCy4RR_u`4Fd zo!NaYSffL+wg29FJ+BQWtb)ZNsxzYk=BsHIIjj=gEC0mKjhT--LGr4{a>13lkF*?G zS_BVCM;_YfbZaB0`_aI#=#;fDlAj4(@VL08omc+G{)?L?7Nt)tjqa1rI{dO~KQU?R zrb|<#qI{c=Z$6T`eY^jKoeZwO-4gF}l`UW9JNFGo=Hl36Cl<#3~CmhhY{AA`uH}{opr|a3emvk@eEi9>X@tRfiU|QR(Al5d& z%2@$R%72Tz>S#Qfs#?=KuT1x&Lv}pt&xTTy;}>5Zw{Lg#^$VR9=AtH_TeeamCrHH2 zA#u-b7k+^YcIO{7CG@V)M8Rw9=8Nf>7OK-VLVABYOZsbll{bRSvS4fH#9Z+7V_ImO77{nq#SvR{lCQ}4q2z@ zqe9KUm+5B9EIur`r0C>i?aU=Bl{P$|sbcH4f~C!OXTls$7S@R>8&(LKT+hF=;nru5 zO1$LJ^P>C zTDyY#u$y!R6L)w+8h84Os+8*+Ex+?TSjLrLvTK3t)rHD@e>P4jcG2N7nJ*K#{&*`pl{7qCarxRL7FpgZsZuuI+dk5s zt;TK&j9MHgBx-LOoV>JS>o-Xq6WJM!*Ik2>Cp?yrOt{07p>ervc9hxguaa-}oIg~Q z`tnWEM^EYG7s{%oo~L}{cfEeRym;Z^Sv}|CqFNlD=t+9Uxr9wha^!mzy{hHNH>Nom zp5lj1rBtS}#x-tZR!F@v^J-McJDtAv_-HFevLe~^^Zu_hudnbkY zd{Xn4Z6ZJBvj_w(Y2YskJe;b~nABytIhXx>k|(!M2^YUy=

b#t#28Ldr@e9o-^w zTS)vuX1m|788@olM9vYOlo%IWSh6o%QZ&`=N8y&8p&~rDuSIyPGyGJ&aZyWnHB*D= zPFGEilMcrl8dxpsJGZJzOtZ^aFm?JPuFK^@2{$XO>QiG3k1FlDkiy11C#(6utmzNt zm@ZbHzc5T-yM)w>Gp9bTQ8L~f8?brX<9{`IRzFzSg(|x^imlXMvu;`zuypOgS?lI5 zNW8n$f+-<9b9ylS2J!xb;i>{u+R?DyJB=$-I~9Z{~? zv0CK;ogTusmv3fV#k}i!Nt4rW1;H*}_J3uT+L=My6+L!zZ&>6Szf`k3H1brL!d|I~ zOaLoIDekMP71w@>tx-zjqAju36`Bn z!u%$lQn6pQ1uxrS5^eQmxp&LsWs5s4KOfL>Xqh^vFFWFTPw=<-&r1`xE}Z-9Jd>q{ z8?$?x^XdgL7jvSgS6CTOD01+%!AkvH7n9NDHphA)zmpfAeQKOj@GEB0vM}Gh z(HV#IPASYSW=VxXD5`dtvT(fw^0E2KWDZ$Mg1Y NJem1O literal 10763 zcmb2|=3oGW|7U9>^JOhJJ=XF!FE;{MyHJZuNnyOWmfv)xK@J z?&sIfti|Uir(e8Q%X`{trsuI^2}i_zKK-cQv-8il>K{@2V*hQnsoDMi)6e?YS*Oka ze^&Z)y#0gTl=<=HI(t0-{0)!0(RYzO>;~_=KJoA!9&2jvZ0r}`{l7MHzfH`d=dpi2 zJucq&SUkA-gRuC+^!uBWFU7Z*KYaelueTpwJiqel`Ox<64{xI@fAAfY-fF+E z#_ERP`DZ;VU+ziVZD_jx$FHZizkhjJyf0orzUqL^X}R5L9a9;uWc{+>EZBOb=6Kq* zKLs29Z(?S9ctoP%zU=l^ zx9py^{TFYp%*JwSXZ{NZYTwvj;4Lw+_PblYXY!igHM@;%FV60J^|tnh#J?Y5hyGXo z2;3EIp6xd8)-OLMlMl?whO0OizBh>QJ-Dp##>u%{`S;p?eRz6)_wV!f4~9I96Mpvh z7_(XFYhI&!2CJVv6Oi4!Ah{|w)L7v~S!|uM@rHQ^`o3O2D`k**ndiyPFoZrfF>WRD0Q7fe(HLNvGJCWhLG)Yp=fD_9OR`%rB8wvhQ?l zGB0|pmCD_9mD}>{Jnsh0BX$oyRc}9gWcfvvX#GD0rapV*)js`AoMN`Locra|eP1Lz zEw@H~l5xv42r>7nURC$|U%~u+|36+g;mr`aR~pwNc=zQ!!|XyVs4|-F7f2T>6Mc&^|w#>x9dlpbY06F#rgZ*I_a}5DK98` zXJ%mYaPq!fIcp2!cX$8n{h5=bz47+miFf<04fgCfK4F``N=mY2Oxc!>vj3SEKm4EC zuCILbTuJPze{+5$Db@Th`W|pdKK8!Aq33lI+J84zP1-BwIQK-$r?0o42%hE>ub*G> zb*+6oZ_*!Qn>+32@9P(PzWBKI%crer;_>pQn4)Dwwk+PIpHp7%|Df#miVN?jZL@T# ze6#0k$*Z`!wl8~yMQbuNwoj?lxPL;n{q*`Pbvu6KhD@?LJA047%8&1iUwjpQS>k+S zuchmCyPAKSzb?IaV>5s2hIOoVd*?D;zO>AF|HOMo?Y=RjZ%o>JF~Re}l8T*wKHBp5 zTYog;{M`BBZ?Ws{s&$3?<}bf}lkwr(J7TrxJ-77A?d9DzLqIR4%<+`_kvp@GSXX8+ zmCLS^JHP01^70=`j`;nUdnJ19@i|U!-Pvyx?p9RWIw^RY{qEyu+txq$_&_^4_UNpe zOOD)ee>RTpTmUvT%H^k zoSM^?VHR++E5q4xPwTX>5Vxas(ailbk0dv4zW;1u(D|$#z9nXpYu-OpeEHu^em;+^ z=7+VL9?v=d{OJYzNfx{pdakJLUizIesm}TG`);ke$v3QvmK0WI22ZpNv@ZHBm19&< zJ?EGArCn8#ruqB+KmY!}=B%Ohob&N#ZvU&6Dzm*AcWLUk7rfa`8qbd2VBX#ru=wcK z)!_@i6-_bwB`e>#O=0Kp|2w+PIj36$D%s?F)gEf=SKh1o`^>@euCRaq+HU7?PndHw z(Y02(bUR;d(5veqotxxe=yYtT+gS7eV9m*k{3@AOkM(=kY`$v0KWgz(R`Gv@6Be!I zUAttC%H{qkYvN~KE?#J&D^e=^VaM)w)BD{jkNC*lE?AzS?O3XNh3Ulwt*LiPk34Z% z=L-G)vYu;~-hDJFe0QBj{hg`p?P0$jepg#2m2-D{?48%YWlvuH zI(_ernEJ{$T0z$r$4l;79=hcBho2q$Dte@UlrPj@7yfIVc;olh9P@T5@g;0bn@i_A z&Ybs*OE0#C|1neG@A4me)&B)O^lROB+H2y+cbTQ%*6vXM<#_a5aK5z7w>?(3e#^8U zur7#w_PEuGz4(XYGWO~{4JPU}e^y*7{?*QMMIO=81uHN z`<{Q^`D>5F&b{C5_kCU9KgVB1e7)Ik_Op^=*AiEoJ9u0d+W*3Kbt>*8se^LqGN-cRqIH_TOs}`+^}Jf)DQg;h z{G4Kg9n-mAn%4QY#V4m)f72|fZe-p1ZvMxA#WVMRTKedDZHLRN=R6|qt~@_0#rM_K z{`e&9Yh_x0$?N^m`-z|C+bVjM+D?t{jEfJs7}meB{Py>c`vfI_lx&<@_xAmz7xL@M z76zEaymgjj{<535&Axs2`)NM^%K~=wwy|^OU!FJfolIrM#^S`SE8q8RufG|lzT?gM z_nGcT&-xszY%i5BI&yrg%{K?d-fi>juLg(rhex+}i0u4vFK*tv z<6c*`7faf0F=^dBckeATwoUQ-Z!X$h&02nsm-R%A-Mfm#*EKGzSr*IBe9)8K@HWrJ zTk%)?cQblikiPKt>MpbT&Ii_kW?6Mn|BhVQ^IF{DCdaj#4gX&X=6Wo?U;dw`{*Okn zjH~3E=hydL&EZ>Q>+<`P0lVGu3v4g9CT$Ym+abC4+wT0F=lV?V+aq@VPnhz|BCzM{ zs`q{J3b#z(c5Lggxz$@=BYHA_m(dhN^h?^Zp>rO2Pf_tbs&Ew|IB(E{g9XM70#9$v1S~ z*zWrs=TZ6b%C;>}wx=$e{k}qGc8tu9${9SZv)Era>95)TKVPAKc4gE>a5^3xw9K@`BZ-Y7t(E>-c@DVv8!ln`_z)qHX{8UwJdHU%3B^&CfOqKXZ7zO+j(FkJXKp@y!BhcWT~WT$f+6)q%D5mD9b>8@d`j z(N}(noB#jnApP^>`<&u1=ZeE--~U(b_#HB>ebI{Ziw-{5pa0%&y8jm5d47iqt^eiC zudm(zc$dAjySC2XK+GzExSj-IV-R_tg&T zwQpC-&n=wtA$a+#FvMUKYaK-y|mr3Z-KI=ee~j+iVgFHw=B9>{7m18^}7GE&E{3BpFdUD z!_6LX_KmrI)NwX_r+4esgKy4mxP4Zv>hXDf|7{;`3vQ7${<1N2_5QT^Qd@6+oBZ;k zT{!!gF^ke3}BJuQ@OH1d~-}ADs?)@cVa26ap{i5b|0r-%jN$Rdq%)$ue9=?_T zYLA)u*59c!OMV@z2>LZS(tEXx%oP^quhV4Pgx;j&ufLXW)>2-1wYtnM@9??bZ;Wou zO)!79D1KV;>ge}(TbNg3?XG;V zc`ASSm#4_~xP<+3e^=Mff4MI1u;@0k$M)yUuh*KlCI3Hq_0ips^B>RF{LK4WBlz{R zgv_$<7dMA)di(u+d&`N%E2nk0zuy(^;;wvli`eGU}47VM(Z9`q&HXQi;a#wKPgZ%LC&+lAwnIe5v zl6C*w{!;0ux68^+a}2IrYAic;?~=dqqI;6Rj?K<{c;Q5x>z#>rFD?GI{Yuj1gD(^% z!*9>Mwj)c$+Ed}7?%g}WZl@C&0|L40ZqKfIe}hdjOL_a8yu!4gn9^#XCGVFqUzZXnuevmYSN@jk?Nw)Xt&dauR=a&B%YJ>9 z1qIasFP|QE%`DK{i}!9yTo1*4a>#XLCvzd0+ z&ZN?4Q|%^}wXwU`J}ojol$^2EVR6O(zm5K{&riF3V7^7u`*|6?A6LuF*ZaFe`fsKX z&w8!dn$N2P=6M%ttD5Ou@>jN7()H2tlgjZoypOqn-ScM7&Z@{F^JJHW*HrYix>z><=_2d^8ef|O}m<1H+Ik2I`{bPca`R0u4m5Y zW^{d&eySL*fTW#cpA@06cEu6*PFg4gwD{AcntEXnnJ)*h#M z`EtEXb*)dt?!^~O--v`sLSWzY4p&6h407*_QGm#{_l$fMd-QKm4jb)+h5JYQ@K$@oOaWa^`)$ zRd4fb?c&+9qgSWPy_r%2?04TXXFqQjesb^3 z{)aCFrh2Y-y}kCaPPET8_r7gMD}HkrJ`2tklmC{dFK{Jk$3H{Hjc-5xIbOGXuFb{F z|K8utI#%d%?8v#eZ&B5fMRK37)>fPS-te?k+T_`^TQ4^JyEMU=Eoc8(Po>R=!?(Ct zJ}kPmqE;rxzU$6UtDLXauTDnGetY&cYhl^dzfVFkZPI>!^8Xq+MLhWVa?b6EOFphS zJTK&S+(kLv!{;7F92b7F_{rY$llGndlk@Y}vFE4DpGkiFZ}!dR`;MReyYJr?T?oPaZbY6%1bfsyR6FvW*-N3c!(uRjed-K2D zk9uK|u*dm%gw7zpf+ zT@&5?R$1uqYqwwWaW9%P)+b!QXMgwJN#^^8+bk|#-+Jq0aKiqtvrMF%z9-#oj(OKK z;q+(G%@VF&9>3z$55D-Wqg7gdLG*}}N{F)lO1pdK&Qy1cI(<@4B;kIY*fvy7XG9$8Gt3?UGEvF;}@IJD$9`6>qWb!HcWedL;p# z73+J}Icdl)zPc~&Rd%WF`lGHbv!xeLo?wD1E2Ss1~jEo#=jGP;yG- z!Y9-4Wm^&?q(wIiiCs5XU~ru&SJZU9rAs1f3$N&zkI9=wH;Kh}`TN9k)$3k3`t9vx z-9s*k3XYG0G?uj#>O{(}ny~MN_sR9Dvu_>F)5{E(P4>CHYI2)!NW9JWjjLAt{ubmD zTM{Nw&u5wSMReX%5eo}x@1n?d4qlaG@p@K2h4v=zGmh5{Jf@Yi%0?wSWrdWU+TX1% z;nlilw_fQz*3+P=RJ?AB@5KXtH#bW0&QTOyEb*s*&dj+B1cOh;Bxza1CQ3eikj}c< z*Pz|W3zuVi8X|p;q)|{X+Ev{K6eGS@R{D%}@tKB$n-5hx2%5@)$_ugx7hMbLg_$X+1_GN3;Hc4Z9g$qXx@oGn< zOj~jM zFB8*j=jaf4yE%M@=Q0+T-%RBO2UDI%`-M%r?k2NXP%zVb6sIaT&2#XgJe2Y@)(gE4sp}*8&J>=u+%(7K#6-`GT%KghZ+m;9%U!raIK(z(wFk6b zm^*>1a@`5rC!CE|QGZgeACq73Ah%r2xAW<1JjiDhJ(^F*-3z%U|co3GPqwVV7GKMKCo z+`;r$GW=-d661MO%{it`6%2lj*Rv6IHsgLB|}(m@2+oG zcn2hz<=wbL0xG4AR*+uP>4%FP?mgipjIf1iIqd~PnQax9F zLhSb>o{N$Ty)Ila^jh6>@=JbnBFe7VR0kFW9D9>?%~5 zpT73>n&3lo+QnUz8#dI4SXMrHEt2;>uKvU7T>bX!*6S^QEHBL7(($(`TvB(FtJ{SMix{qK{c&jK8|&g@*IAg- zMHBiK$gN;u44iRDL&_m{-D+8m0yRG2iQAs|)G`PNJXrkwgSK)(Yvcigr&5AJ&bg)K zp`w`&wJksC=(e#vTr}anNOaAI*z)2YmSq`J4CJ{_)K8H4p`~fD(P@RdN^tEPOGnm+ zdo)<$y7u?j$O_(Go#Mb|x2i~*Glc0(-q&qXT;c1vR;@cB%lnSO1%oo2vC})4USX2vBho;RbKLrI{&bq_> zf;9#LDYoz2IiHB}iqy(2RIrki>~cP}#;CYgThriSWmrtBb$>e$?qdQq+J%fbS z;w>3#7pdG=le2H1UfKCzFJu4!l>TJ z6tJHwLXYptoysc)*2>I!W-I|Z81vQL2%9u=dgh=^m z73;YvyR=TIF@JkRQ|pAcL&zn?hlgI<9-qL>`a{b*gi~_iVk5Tx$zK?5HGbh@TIkim zDkRL*!NR%F;>u6g3H)YUpCqQfX!xJVDUv7Wy4Bh70n6X|E;&cXj8g(KuAJ;A4nKW% zBRNCG$@o;*TEPgxs7Y=Yl|&{;EGt|5z%P*VqW8nb1p*P4Q`JOMgPW|C&M6yxJZJS! zCuoJW@dAknmTzQ>r<@QGd)cyKl2e6ZkjC!wD(xj247nykdR@(H5;bQ>oMKX)DX>%e z@9~K`2a_%^JGdo9DZ6v8W9sSa(h!N%JiO@Cp?-^YDI-P!zRDFY7Ttyi*=M*b`koFl z-BO?w>i*Hhw4LF>iWjUO)_bfmVw92&nSWqq>+1_E0`0D)2kYFC>a%Dt@~(&y?zpug zWNDDhO#}1Xw~JR+Ij~$2WXRb0gJnWmqtO(`70zBOeok6^f!${R2M&d(7bkKZW_64F z)0A;oAjOrHYSJ=ObpM79%WWUt^a?grcbaHQh;JznUpdX)IU;ajSZ7;MXv&^fZ?Z2k zxXox$O<_*=6y#Oh=Jev=ktJJIm)my92~Yg-pzn-AVpsO;SyaNv>TvYI-nL8wPHCYBE8?dAJ->J^v)AiIbBv7& z@)MptVBF@^)xziEF8%aP@XPEYMOT)17;9{O=&a$V+ZChh^R%&)J6qyW`bUSa(ps-9 zA7p!ab93BW)}i9F>cn@&a+@QYe=cz1>#-DOm>0-#anh!RL0mt$JT0yXUfIi_-@fT~ z)D)wG6=!%GYFartm#R2_oSM$?DfLI-)2FIkUJ^#L&z#isVO!0>AnnRNtG6a_UPtIg zwYh;x-03bn>!SKA54$)_k)5!wvT)y|#9OB#y!<{Knb4Ka#~iJ+`H=B7M(@ROt>vrw z;*2B?sCB=1pt|<|fp;410e2Nx8+sJOvW3$9TD$hlY26+veYVA9*@YluC#${JJ9yto zCnZ{&rB8BA5aD^U#BodMn-f+T1UNi$ z>3^r%lNw6^`=)7df3b&`|JOr&#bZNJ)mF zJuq&!>y%o@eGWATKH4qRa&w&7babWj~Z-Q$BWtejn9hlRt9R;s6^_cpnJ=FRx zCOX^QbUNdM0NcY>C$<_Yug$o&QepntcIBCF{YO@D2v?rYT6HslEBl$?Un{#~dpY!3 zg4*^ZuhAEqsk7jmh>6DzVb)WN{nWoF{Ym23(j&CC{dAb*oX``leqKA+w!GQU{8j&y zurQ0LTK5VArM&^cM^CHN6y7`W#6`STwz_bitC#u<-UZiJ2s69!o9byXg*D2>^oQSh z{o$L0%a!Mxp{WT$LAEV3R;I9NnQG4N+g@S%kM(KpCWll;j$;O^Bidvaamcy0`hS@= z*Se(ie0uAePv2r(pn0%o z(}KJhy^tX0l4Xyy(t-{@nzx@Td*LGYsOOqTef0NDIvu(!sJX`~`hKQvTzlz6u3%$# z3+Z%@GfJ0Oo;kUsXI2YsoVNau)ncx6HO)|J?PFNZAmDmd_<^MRmFYivH+TyN7+iFz;QiLRY@S0R|C7Fx3>)N1 zIYSj$k_5Kozj?a4D?#@A#ege!|hR!cjDJMQMv2Ryuv7nSCuo>y_3qPUFp zsNnT(ofWY=Ii+|r*){e*2vk-QXfQckWqX<=$)UW#l=( zcg3{yD~^p9yQ4}qUzE;I5jSLgqSN4g$KY7zx||Dk3tjvTRW5GpDr%PB#J>MSsP&V| z*R_s@p&_dr-mdbx!nS6Y2kV>%+e#NcV=WfpiV#_~=F)Bv5f9GK94DL8uj?{$yc4T+ zN!*h=v$yTy@5;bdL$;-&x%XX{DR;8GIrevvw0BhG^K7FthZWXw$%U{j*v`06>%!~= zM}6Vw>nmq>72Ic;zKLT4XQ8ZV>c}V~XG2u~JboGseYqp6J`}J#FSf-&7=l#&)OR>XgFtiA9{k(G&F3ZmFyd4K=j3Xl`@RyX|(W{0W;i!!2jQC0@NrY!@4^ zU6**Q(-|~(x$Kz-k0ZDLZ*AE0hn~C z0tK&LaI;hF=ADr=`IF!daYCt zn6^7sWQ(Klz6B5Ncdctb8zFn#*?Eni)rD};wjEx#m2&&GG*0859r0-RPqMboDBriaznZT*#g}OfpN&#esGdQxzyVFcPZ5GwPh?Jc zUqA26Q3Fw>q`gaBlcaMwgPxyJNwrW|DfXSwbl%CO31x>3OPA)x+HonEottn+;(_*Q zS2MjosurvbLf#oiv>05XW=-L0Wm4F=lB;2Fp^*Mj-PD<}K3i4_EzXT}d~xDlbbFjt z>FbuJvbOIkt<%zZyB5wh*H|6!!DVXnt3}3oG3{M@RfE|vLe#o3)I6GfTb|8`#KUnIR?ea6e3hj`9=DJmIlWtd;O^GF!4n)3EyK^Z?d|VZ;huA_A%7{eiSa##CznnaRV9n<^{_0hd*Ci# z!PMP#XyKv6t(Qc<^5klBHRK&SJT>&?hhE0g&l#t9UI?p7CDrt_MrH@9a6f;rUq?yG zTzmUuu0I>6WVUO4P@T)R*p`Ja!;r~AB|d;#^yY=F6aAO^SxB7V^=rG}G23J3SuTg} zi*aSw-zO_N+s|d?vcDmoAuBrd+E%4=ZVyTyx112_F+2YC-Y~tBg+6@&1qe zvN_;F*YrnSk2q7S19xS(<*#=&T;ZuSH(;w_WmRWu(+5+F!#``cUi~qlIYHw*LqO=# z-VQ5<-P>Q?p4IpJ^UjM7O!3^ezG`U1EOTK?*Ep)h{4KNUQh%*xA7^Wj+06>8Ht8lu z)~;JTnx_*}D&JZBn)kZ9V9lvTDeS-2IfXxAe%|adW#!3@L8h-|rg;e8PPbU)#Oe4x zE1*cV)5}=#zIJZok_TQ3qo)qk?VWjd#?I;K zuZ23opEKTS)G=Ig=EscNFAV}KS6j__Q8({6XR73$O%YYspIPjE@U_Gv*gERF@m;=% zhhH2{ofN*YchQ6HE$zxIEXvWL4;!*Hrbez>=srV1eU8<1m1SzrxDLg-@jBct%6!P} z&~=>S#@ZVeEa&E^h3#-w3}m;yR?b82SOkb9-E?Z|W_4Lh87DErG<%?V=iM_ag z!LR7BOQGVToHwuKzgo=lT%GZt{3b`c*L4LOPFMAmn2&zTZn@3ZdG2@l*Z=a5)3{VN HGB5xDZ}zph diff --git a/stdlib/ufloat.mlw b/stdlib/ufloat.mlw index 219e15409..a5c5b1986 100644 --- a/stdlib/ufloat.mlw +++ b/stdlib/ufloat.mlw @@ -387,7 +387,7 @@ module UFloatLemmas use real.Abs use UFloat - let lemma uadd_double_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real) + let lemma uadd_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real) requires { abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs } @@ -459,49 +459,8 @@ module UFloatLemmas } end end -(* - assert { - 0. <=. x_rel /\ 0. <=. y_rel -> - delta <=. - (eps +. y_rel) *. x_factor +. (eps +. x_rel) *. y_factor - +. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs - by - (delta <=. x_factor *. x_rel +. x_abs +. x_factor - so - x_factor +. x_abs <=. eps *. (y_factor +. y_abs) -> - delta <=. (eps +. x_rel) *. y_factor - +. (eps +. y_rel) *. x_factor - +. (y_rel +. eps) *. x_abs +. (x_rel +. eps) *. y_abs - by - delta <=. eps *. (y_factor +. y_abs) *. x_rel - +. (eps *. (y_factor +. y_abs))) - /\ - (delta <=. y_factor *. y_rel +. y_abs +. y_factor - so - abs y_factor +. y_abs <=. eps *. (x_factor +. x_abs) -> - delta <=. (eps +. y_rel) *. x_factor - +. (eps +. x_rel) *. y_factor - +. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs - by - delta <=. eps *. (x_factor +. x_abs) *. y_rel - +. (eps *. (x_factor +. x_abs))) - /\ - ( - (eps *. (x_factor +. x_abs) <. abs y_factor +. y_abs /\ - eps *. (y_factor +. y_abs) <. abs x_factor +. x_abs) -> - (delta <=. - (eps +. y_rel) *. x_factor +. (eps +. x_rel) *. y_factor - +. (x_rel +. eps) *. y_abs +. (y_rel +. eps) *. x_abs - by - abs (to_real x_f +. to_real y_f) <=. - abs (to_real x_f -. x) +. x_factor +. (abs (to_real y_f -. y) +. y_factor) - so - x_factor *. x_rel <=. (y_factor +. y_abs) /. eps *. x_rel /\ - y_factor *. y_rel <=. (x_factor +. x_abs) /. eps *. y_rel)) - } -*) - let lemma usub_double_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real) + let lemma usub_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs y y_factor y_rel y_abs : real) requires { abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs } @@ -520,11 +479,11 @@ module UFloatLemmas <=. (x_rel +. y_rel +. eps) *. (x_factor +. y_factor) +. ((1. +. eps +. y_rel) *. x_abs +. (1. +. eps +. x_rel) *. y_abs) } - = uadd_double_error_propagation x_f (--. y_f) r x x_factor x_rel x_abs (-. y) y_factor y_rel y_abs + = uadd_error_propagation x_f (--. y_f) r x x_factor x_rel x_abs (-. y) y_factor y_rel y_abs use HelperLemmas - let lemma umul_double_error_propagation (x_f y_f r : u) + let lemma umul_error_propagation (x_f y_f r : u) (x x_factor x_rel x_abs : real) (y y_factor y_rel y_abs : real) : unit requires { abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs @@ -558,7 +517,7 @@ module UFloatLemmas use real.ExpLog - let lemma log_double_error_propagation (logx_f x_f : u) + let lemma log_error_propagation (logx_f x_f : u) (x_exact x_factor log_rel log_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -581,7 +540,7 @@ module UFloatLemmas <=. (abs (log (x_exact)) -. log (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel } - let lemma log2_double_error_propagation (log2x_f x_f : u) + let lemma log2_error_propagation (log2x_f x_f : u) (x_exact x_factor log_rel log_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -604,7 +563,7 @@ module UFloatLemmas <=. (abs (log2 (x_exact)) -. log2 (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel } - let lemma log2_double_error_propagation_simple (log2x_f x_f : u) + let lemma log2_error_propagation_simple (log2x_f x_f : u) (x_exact log_rel x_rel : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_exact } requires { @@ -619,9 +578,9 @@ module UFloatLemmas <=. log_rel *. abs (log2 x_exact) -. log2 (1. -. x_rel) *. (1. +. log_rel) } = - log2_double_error_propagation log2x_f x_f x_exact x_exact log_rel 0.0 x_rel 0.0 + log2_error_propagation log2x_f x_f x_exact x_exact log_rel 0.0 x_rel 0.0 - let lemma log10_double_error_propagation (log10x_f x_f : u) + let lemma log10_error_propagation (log10x_f x_f : u) (x_exact x_factor log_rel log_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -644,7 +603,7 @@ module UFloatLemmas <=. (abs (log10 (x_exact)) -. log10 (1.0 -. (((x_rel *. x_factor) +. x_abs) /. x_exact))) *. log_rel } - let lemma exp_double_error_propagation (expx_f x_f : u) + let lemma exp_error_propagation (expx_f x_f : u) (x_exact x_factor exp_rel exp_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -680,7 +639,7 @@ module UFloatLemmas use real.Trigonometry - let lemma sin_double_error_propagation (sinx_f x_f : u) + let lemma sin_error_propagation (sinx_f x_f : u) (x_exact x_factor sin_rel sin_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -700,7 +659,7 @@ module UFloatLemmas <=. (abs (sin x_exact) +. (x_rel *. x_factor +. x_abs)) *. sin_rel } - let lemma cos_double_error_propagation (cosx_f x_f : u) + let lemma cos_error_propagation (cosx_f x_f : u) (x_exact x_factor cos_rel cos_abs x_rel x_abs : real) requires { abs (to_real x_f -. x_exact) <=. x_rel *. x_factor +. x_abs } requires { @@ -726,7 +685,7 @@ module UFloatLemmas function real_fun (f:int -> u) : int -> real = fun i -> to_real (f i) - let lemma sum_double_error_propagation (x : u) + let lemma sum_error_propagation (x : u) (f : int -> u) (f_exact f_factor f_factor' : int -> real) (n:int) (sum_rel sum_abs f_rel f_abs : real) requires { @@ -757,7 +716,7 @@ module UFloatLemmas } (* We don't have an error on y_f because in practice we won't have an exact division with an approximate divisor *) - let lemma udiv_exact_double_error_propagation (x_f y_f r: u) (x x_factor x_rel x_abs : real) + let lemma udiv_exact_error_propagation (x_f y_f r: u) (x x_factor x_rel x_abs : real) requires { abs (to_real x_f -. x) <=. x_rel *. x_factor +. x_abs } @@ -804,6 +763,8 @@ module UFloatLemmas in () end + + (** {2 Single propagation lemmas} *) module USingleLemmas