Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2018 Sylvie Boldo
Copyright (C) 2010-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2010-2018 Guillaume Melquiond
Locations: where a real number is positioned with respect to its rounded-down value in an arbitrary format.
Require Import Raux Defs Float_prop. Require Import SpecFloatCompat. Notation location := location (only parsing). Notation loc_Exact := loc_Exact (only parsing). Notation loc_Inexact := loc_Inexact (only parsing). Section Fcalc_bracket. Variable d u : R. Hypothesis Hdu : (d < u)%R. Variable x : R. Definition inbetween_loc := match Rcompare x d with | Gt => loc_Inexact (Rcompare x ((d + u) / 2)) | _ => loc_Exact end.
Locates a real number with respect to the middle of two other numbers.
Inductive inbetween : location -> Prop := | inbetween_Exact : x = d -> inbetween loc_Exact | inbetween_Inexact l : (d < x < u)%R -> Rcompare x ((d + u) / 2)%R = l -> inbetween (loc_Inexact l).d, u:RHdu:(d < u)%Rx:R(d <= x < u)%R -> inbetween inbetween_locd, u:RHdu:(d < u)%Rx:R(d <= x < u)%R -> inbetween inbetween_locd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%Rinbetween inbetween_locd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%Rinbetween match Rcompare x d with | Gt => SpecFloatCopy.loc_Inexact (Rcompare x ((d + u) / 2)) | _ => SpecFloatCopy.loc_Exact endd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(x < d)%Rinbetween SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:x = dinbetween SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%Rinbetween (SpecFloatCopy.loc_Inexact (Rcompare x ((d + u) / 2)))d, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:x = dinbetween SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%Rinbetween (SpecFloatCopy.loc_Inexact (Rcompare x ((d + u) / 2)))d, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%Rinbetween (SpecFloatCopy.loc_Inexact (Rcompare x ((d + u) / 2)))d, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%R(d < x < u)%Rd, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%RRcompare x ((d + u) / 2) = Rcompare x ((d + u) / 2)easy. Qed.d, u:RHdu:(d < u)%Rx:RHx:(d <= x < u)%RH:(d < x)%RRcompare x ((d + u) / 2) = Rcompare x ((d + u) / 2)d, u:RHdu:(d < u)%Rx:Rforall l l' : SpecFloatCopy.location, inbetween l -> inbetween l' -> l = l'd, u:RHdu:(d < u)%Rx:Rforall l l' : SpecFloatCopy.location, inbetween l -> inbetween l' -> l = l'd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationHl:inbetween lHl':inbetween l'l = l'd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationH, H0:x = dSpecFloatCopy.loc_Exact = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationH:x = dl0:comparisonH0:(d < x < u)%RH1:Rcompare x ((d + u) / 2) = l0SpecFloatCopy.loc_Exact = SpecFloatCopy.loc_Inexact l0d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0H1:x = dSpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationH:x = dl0:comparisonH0:(d < x < u)%RH1:Rcompare x ((d + u) / 2) = l0SpecFloatCopy.loc_Exact = SpecFloatCopy.loc_Inexact l0d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0H1:x = dSpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationH:x = dl0:comparisonH0:(d < d < u)%RH1:Rcompare x ((d + u) / 2) = l0SpecFloatCopy.loc_Exact = SpecFloatCopy.loc_Inexact l0d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0H1:x = dSpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0H1:x = dSpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < d < u)%RH0:Rcompare x ((d + u) / 2) = l0H1:x = dSpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Exactd, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1SpecFloatCopy.loc_Inexact l0 = SpecFloatCopy.loc_Inexact l1now rewrite <- H0. Qed. Section Fcalc_bracket_any. Variable l : location.d, u:RHdu:(d < u)%Rx:Rl, l':SpecFloatCopy.locationl0:comparisonH:(d < x < u)%RH0:Rcompare x ((d + u) / 2) = l0l1:comparisonH1:(d < x < u)%RH2:Rcompare x ((d + u) / 2) = l1l0 = l1d, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationinbetween l -> (d <= x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationinbetween l -> (d <= x < u)%Rd, u:RHdu:(d < u)%Rx:RHx:x = d(d <= x < u)%Rd, u:RHdu:(d < u)%Rx:Rl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'(d <= x < u)%Rd, u:RHdu:(d < u)%Rx:RHx:x = d(d <= d < u)%Rd, u:RHdu:(d < u)%Rx:Rl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'(d <= x < u)%Rd, u:RHdu:(d < u)%Rx:RHx:x = d(d <= d)%Rd, u:RHdu:(d < u)%Rx:RHx:x = d(d < u)%Rd, u:RHdu:(d < u)%Rx:Rl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'(d <= x < u)%Rd, u:RHdu:(d < u)%Rx:RHx:x = d(d < u)%Rd, u:RHdu:(d < u)%Rx:Rl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'(d <= x < u)%Rnow split ; try apply Rlt_le. Qed.d, u:RHdu:(d < u)%Rx:Rl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'(d <= x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationinbetween l -> l <> SpecFloatCopy.loc_Exact -> (d < x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationinbetween l -> l <> SpecFloatCopy.loc_Exact -> (d < x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationHx:x = dH:SpecFloatCopy.loc_Exact <> SpecFloatCopy.loc_Exact(d < x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'H:SpecFloatCopy.loc_Inexact l' <> SpecFloatCopy.loc_Exact(d < x < u)%Rexact Hx. Qed. End Fcalc_bracket_any.d, u:RHdu:(d < u)%Rx:Rl:SpecFloatCopy.locationl':comparisonHx:(d < x < u)%RHl:Rcompare x ((d + u) / 2) = l'H:SpecFloatCopy.loc_Inexact l' <> SpecFloatCopy.loc_Exact(d < x < u)%Rd, u:RHdu:(d < u)%Rx:Rforall l : comparison, inbetween (SpecFloatCopy.loc_Inexact l) -> Rcompare (x - d) (u - x) = ld, u:RHdu:(d < u)%Rx:Rforall l : comparison, inbetween (SpecFloatCopy.loc_Inexact l) -> Rcompare (x - d) (u - x) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)Rcompare (x - d) (u - x) = lnow rewrite Rcompare_middle. Qed.d, u:RHdu:(d < u)%Rx:Rl:comparisonHl':(d < x < u)%RHx:Rcompare x ((d + u) / 2) = lRcompare (x - d) (u - x) = ld, u:RHdu:(d < u)%Rx:Rforall l : comparison, inbetween (SpecFloatCopy.loc_Inexact l) -> Rcompare (Rabs (d - x)) (Rabs (u - x)) = ld, u:RHdu:(d < u)%Rx:Rforall l : comparison, inbetween (SpecFloatCopy.loc_Inexact l) -> Rcompare (Rabs (d - x)) (Rabs (u - x)) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)Rcompare (Rabs (d - x)) (Rabs (u - x)) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)Rcompare (- (d - x)) (Rabs (u - x)) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)Rcompare (- (d - x)) (u - x) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(0 <= u - x)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)Rcompare (x - d) (u - x) = ld, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(0 <= u - x)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(0 <= u - x)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(x <= u)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(x < u)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rd, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d - x <= 0)%Rapply (inbetween_bounds _ Hl). Qed. End Fcalc_bracket.d, u:RHdu:(d < u)%Rx:Rl:comparisonHl:inbetween (SpecFloatCopy.loc_Inexact l)(d <= x)%Rforall (d u : R) (l : SpecFloatCopy.location), (d < u)%R -> exists x : R, inbetween d u x lforall (d u : R) (l : SpecFloatCopy.location), (d < u)%R -> exists x : R, inbetween d u x ld, u:RHdu:(d < u)%Rexists x : R, inbetween d u x SpecFloatCopy.loc_Exactd, u:Rl:comparisonHdu:(d < u)%Rexists x : R, inbetween d u x (SpecFloatCopy.loc_Inexact l)d, u:RHdu:(d < u)%Rinbetween d u d SpecFloatCopy.loc_Exactd, u:Rl:comparisonHdu:(d < u)%Rexists x : R, inbetween d u x (SpecFloatCopy.loc_Inexact l)d, u:Rl:comparisonHdu:(d < u)%Rexists x : R, inbetween d u x (SpecFloatCopy.loc_Inexact l)d, u:Rl:comparisonHdu:(d < u)%Rinbetween d u (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) (SpecFloatCopy.loc_Inexact l)(* *)d, u:Rl:comparisonHdu:(d < u)%R(d < d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < v)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < match l with | Eq => 2 | Lt => 1 | Gt => 3 end * / 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < match l with | Eq => 2 | Lt => 1 | Gt => 3 end)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < / 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < / 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(v < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(match l with | Eq => 2 | Lt => 1 | Gt => 3 end * / 4 < 1)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(0 < 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(match l with | Eq => 2 | Lt => 1 | Gt => 3 end * / 4 * 4 < 1 * 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(match l with | Eq => 2 | Lt => 1 | Gt => 3 end * / 4 * 4 < 1 * 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(match l with | Eq => 2 | Lt => 1 | Gt => 3 end * 1 < 1 * 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R4%R <> 0%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(match l with | Eq => 2 | Lt => 1 | Gt => 3 end < 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R4%R <> 0%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R4%R <> 0%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:R(4 > 0)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < d + v * (u - d))%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + d * (v - 1) < d + v * (u - d) + d * (v - 1))%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d * v < v * u)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(v * d < v * u)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d + v * (u - d) < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(- u * v + (d + v * (u - d)) < - u * v + u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d * (1 - v) < - u * v + u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d * (1 - v) < u * (1 - v))%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(0 < 1 - v)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(0 + v < 1 - v + v)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=(match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4)%R:RH:(0 < v < 1)%R(d < u)%Rd, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = l(* *)d, u:Rl:comparisonHdu:(d < u)%RRcompare (d + match l with | Eq => 2 | Lt => 1 | Gt => 3 end / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare (d + v / 4 * (u - d)) ((d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare (d + v / 4 * (u - d) + - (d + u) / 2) ((d + u) / 2 + - (d + u) / 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare ((d + v / 4 * (u - d) + - (d + u) / 2) * 4) (((d + u) / 2 + - (d + u) / 2) * 4) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:R(0 < 4)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare ((d + v / 4 * (u - d) + - (d + u) / 2) * 4) (((d + u) / 2 + - (d + u) / 2) * 4) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare ((d + v / 4 * (u - d) + - (d + u) / 2) * 4) ((u - d) * 0) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare ((u - d) * (v - 2)) ((u - d) * 0) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare (v - 2) 0 = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:R(0 < u - d)%Rd, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare (v - 2) 0 = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare (v - 2 + 2) (0 + 2) = ld, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare v 2 = lcase l ; apply Rcompare_IZR. Qed. Section Fcalc_bracket_step. Variable start step : R. Variable nb_steps : Z. Variable Hstep : (0 < step)%R.d, u:Rl:comparisonHdu:(d < u)%Rv:=match l with | Eq => 2%R | Lt => 1%R | Gt => 3%R end:RRcompare match l with | Eq => 2 | Lt => 1 | Gt => 3 end 2 = lstart, step:Rnb_steps:ZHstep:(0 < step)%Rforall k : Z, (start + IZR k * step < start + IZR (k + 1) * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rforall k : Z, (start + IZR k * step < start + IZR (k + 1) * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(start + IZR k * step < start + IZR (k + 1) * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(IZR k * step < IZR (k + 1) * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(IZR k < IZR (k + 1))%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(IZR k < IZR (k + 1))%Rapply Zlt_succ. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z(k < k + 1)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%Rforall k : Z, ((start + (start + IZR k * step)) / 2)%R = (start + IZR k / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%Rforall k : Z, ((start + (start + IZR k * step)) / 2)%R = (start + IZR k / 2 * step)%Rfield. Qed. Hypothesis (Hnb_steps : (1 < nb_steps)%Z).start, step:Rnb_steps:ZHstep:(0 < step)%Rk:Z((start + (start + IZR k * step)) / 2)%R = (start + IZR k / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location) (l' : comparison), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k < nb_steps)%Z -> Rcompare x (start + IZR nb_steps / 2 * step) = l' -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location) (l' : comparison), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k < nb_steps)%Z -> Rcompare x (start + IZR nb_steps / 2 * step) = l' -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')(* . *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'(start < x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start < x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start < start + IZR k * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start + 0 < start + IZR k * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < IZR k * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < IZR k)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start + IZR (k + 1) * step <= start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR (k + 1) * step <= IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 <= step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR (k + 1) <= IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR (k + 1) <= IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Hx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(k + 1 <= nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'(* . *) now rewrite middle_range. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationl':comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk:(0 < k < nb_steps)%ZHl':Rcompare x (start + IZR nb_steps / 2 * step) = l'Rcompare x ((start + (start + IZR nb_steps * step)) / 2) = l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%Z(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZRcompare x (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZRcompare x (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%Z(x < start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(x < start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start + IZR (k + 1) * step <= start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%RRcompare (start + IZR nb_steps / 2 * step) (start + IZR (k + 1) * step) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%RRcompare (IZR nb_steps) (2 * IZR (k + 1)) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(2 * IZR (k + 1) <= IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR (2 * (k + 1)) <= IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(2 * (k + 1) <= nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rexact Hstep. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(0 < k)%ZHk2:(2 * k + 1 < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (nb_steps < 2 * k)%Z -> (k < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> (nb_steps < 2 * k)%Z -> (k < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%Z(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZRcompare x (start + IZR nb_steps / 2 * step) = Gtstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZRcompare x (start + IZR nb_steps / 2 * step) = Gtstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%Z(start + IZR nb_steps / 2 * step < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start + IZR nb_steps / 2 * step < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(start + IZR nb_steps / 2 * step < start + IZR k * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%RRcompare (start + IZR nb_steps / 2 * step) (start + IZR k * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%RRcompare (IZR nb_steps) (2 * IZR k) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR nb_steps < 2 * IZR k)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(IZR nb_steps < IZR (2 * k))%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(nb_steps < 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rexact Hstep. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk1:(nb_steps < 2 * k)%ZHk2:(k < nb_steps)%ZHx':(start + IZR k * step <= x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (l : SpecFloatCopy.location), inbetween start (start + step) x l -> l <> SpecFloatCopy.loc_Exact -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (l : SpecFloatCopy.location), inbetween start (start + step) x l -> l <> SpecFloatCopy.loc_Exact -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_Exactinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%Rinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)(* . *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(start < x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(start < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(x < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(start + step < start + IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(step < IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(1 * step < IZR nb_steps * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(1 < IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(1 < IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Lt(* . *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare x ((start + (start + IZR nb_steps * step)) / 2) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(x < (start + (start + IZR nb_steps * step)) / 2)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(start + step <= (start + (start + IZR nb_steps * step)) / 2)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(start + step <= start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare (start + IZR nb_steps / 2 * step) (start + step) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare (start + IZR nb_steps / 2 * step) (start + 1 * step) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare (IZR nb_steps) (2 * 1) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%RRcompare (IZR nb_steps) 2 <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(2 <= IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(2 <= nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rexact Hstep. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rl:SpecFloatCopy.locationHx:inbetween start (start + step) x lHl:l <> SpecFloatCopy.loc_ExactHx':(start < x < start + step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall k : Z, (2 * k + 1)%Z = nb_steps -> ((start + IZR k * step + (start + IZR (k + 1) * step)) / 2)%R = (start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall k : Z, (2 * k + 1)%Z = nb_steps -> ((start + IZR k * step + (start + IZR (k + 1) * step)) / 2)%R = (start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zk:ZHk:(2 * k + 1)%Z = nb_steps((start + IZR k * step + (start + IZR (k + 1) * step)) / 2)%R = (start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zk:ZHk:(2 * k + 1)%Z = nb_steps((start + IZR k * step + (start + IZR (k + 1) * step)) / 2)%R = (start + IZR (2 * k + 1) / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zk:ZHk:(2 * k + 1)%Z = nb_steps((start + IZR k * step + (start + (IZR k + 1) * step)) / 2)%R = (start + (2 * IZR k + 1) / 2 * step)%Rfield. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zk:ZHk:(2 * k + 1)%Z = nb_steps((start + IZR k * step + (start + (IZR k + 1) * step)) / 2)%R = (start + (2 * IZR k + 1) / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : comparison), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l) -> (2 * k + 1)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : comparison), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l) -> (2 * k + 1)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l)Hk:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l)Hk:(2 * k + 1)%Z = nb_steps(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l)Hk:(2 * k + 1)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = lstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:comparisonHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact l)Hk:(2 * k + 1)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = lnow rewrite (middle_odd _ Hk) in Hl. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:comparisonHk:(2 * k + 1)%Z = nb_stepsHl:Rcompare x ((start + IZR k * step + (start + IZR (k + 1) * step)) / 2) = lRcompare x (start + IZR nb_steps / 2 * step) = lstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_Exact -> (2 * k + 1)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_Exact -> (2 * k + 1)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k + 1)%Z = nb_steps(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k + 1)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k + 1)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%RRcompare x (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%RRcompare (start + IZR k * step) (start + IZR nb_steps / 2 * step) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%RRcompare (2 * IZR k) (IZR nb_steps) = Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(2 * IZR k < IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(IZR (2 * k) < IZR nb_steps)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(2 * k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(2 * k < 2 * k + 1)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rexact Hstep. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k + 1)%Z = nb_stepsHl:x = (start + IZR k * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> l <> SpecFloatCopy.loc_Exact -> (2 * k)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> l <> SpecFloatCopy.loc_Exact -> (2 * k)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_steps(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Gtstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Gtstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_steps(start + IZR nb_steps / 2 * step < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(start + IZR nb_steps / 2 * step < x)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(start + IZR nb_steps / 2 * step <= start + IZR k * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%RRcompare (start + IZR k * step) (start + IZR nb_steps / 2 * step) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%RRcompare (2 * IZR k) (IZR nb_steps) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%RRcompare (IZR (2 * k)) (IZR nb_steps) <> Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(IZR nb_steps <= IZR (2 * k))%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(nb_steps <= 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(nb_steps <= nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rexact Hstep. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHl:l <> SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsHx':(start + IZR k * step < x < start + IZR (k + 1) * step)%R(0 < step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_Exact -> (2 * k)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Eq)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z), inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_Exact -> (2 * k)%Z = nb_steps -> inbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Eq)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Eq)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_steps(0 < k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Eqstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsRcompare x (start + IZR nb_steps / 2 * step) = Eqstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk:(2 * k)%Z = nb_stepsx = (start + IZR nb_steps / 2 * step)%Rstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k)%Z = nb_stepsHx':x = (start + IZR k * step)%Rx = (start + IZR nb_steps / 2 * step)%Rfield. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:ZHk:(2 * k)%Z = nb_stepsHx':x = (start + IZR k * step)%R(start + IZR k * step)%R = (start + 2 * IZR k / 2 * step)%R
Computes a new location when the interval containing a real
number is split into nb_steps subintervals and the real is
in the k-th one. (Even radix.)
Definition new_location_even k l := if Zeq_bool k 0 then match l with loc_Exact => l | _ => loc_Inexact Lt end else loc_Inexact match Z.compare (2 * k) nb_steps with | Lt => Lt | Eq => match l with loc_Exact => Eq | _ => Gt end | Gt => Gt end.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZZ.even nb_steps = true -> forall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_even k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZZ.even nb_steps = true -> forall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_even k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x (new_location_even k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x (if Zeq_bool k 0 then match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end else SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)(* k = 0 *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + 0 * step) (start + IZR (0 + 1) * step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationl = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH:l = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH:l = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactinbetween start (start + IZR nb_steps * step) x SpecFloatCopy.loc_Exactstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactx = startstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x SpecFloatCopy.loc_ExactHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactx = startstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)(* k <> 0 *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end | Lt => Lt | Gt => Gt end)(* . 2 * k < nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Z(0 < k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Z(2 * k + 1 < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Z(2 * k + 1 < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Zx0:ZH:nb_steps = (2 * x0 + (if Z.even nb_steps then 0 else 1))%Z(2 * k + 1 < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k < nb_steps)%Zx0:ZH:nb_steps = (2 * x0 + 0)%Z(2 * k + 1 < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)(* . 2 * k = nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisoninbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonl = SpecFloatCopy.loc_Exact /\ l' = Eq \/ l <> SpecFloatCopy.loc_Exact /\ l' = Gtstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH:l = SpecFloatCopy.loc_Exact /\ l' = Eq \/ l <> SpecFloatCopy.loc_Exact /\ l' = Gtinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH:l = SpecFloatCopy.loc_Exact /\ l' = Eq \/ l <> SpecFloatCopy.loc_Exact /\ l' = Gtinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact l')start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH1:l = SpecFloatCopy.loc_ExactH2:l' = Eqinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Eq)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH1:l <> SpecFloatCopy.loc_ExactH2:l' = Gtinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH1:l = SpecFloatCopy.loc_ExactH2:l' = Eqinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Eq)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH1:l <> SpecFloatCopy.loc_ExactH2:l' = Gtinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k)%Z = nb_stepsl':=match l with | SpecFloatCopy.loc_Exact => Eq | SpecFloatCopy.loc_Inexact _ => Gt end:comparisonH1:l <> SpecFloatCopy.loc_ExactH2:l' = Gtinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)(* . 2 * k > nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Z(nb_steps < 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Z(k < nb_steps)%Zapply Hk. Qed.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHe:Z.even nb_steps = truex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k)%Z(k < nb_steps)%Z
Computes a new location when the interval containing a real
number is split into nb_steps subintervals and the real is
in the k-th one. (Odd radix.)
Definition new_location_odd k l := if Zeq_bool k 0 then match l with loc_Exact => l | _ => loc_Inexact Lt end else loc_Inexact match Z.compare (2 * k + 1) nb_steps with | Lt => Lt | Eq => match l with loc_Inexact l => l | loc_Exact => Lt end | Gt => Gt end.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZZ.even nb_steps = false -> forall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_odd k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZZ.even nb_steps = false -> forall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location_odd k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x (new_location_odd k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x (if Zeq_bool k 0 then match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end else SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)(* k = 0 *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + 0 * step) (start + IZR (0 + 1) * step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zinbetween start (start + IZR nb_steps * step) x match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt endstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationl = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH:l = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH:l = SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Exact \/ l <> SpecFloatCopy.loc_Exact /\ l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x l'start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactinbetween start (start + IZR nb_steps * step) x SpecFloatCopy.loc_Exactstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactx = startstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x SpecFloatCopy.loc_ExactHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l = SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Exactx = startstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween start (start + step) x lHk0:k = 0%Zl':=match l with | SpecFloatCopy.loc_Exact => l | SpecFloatCopy.loc_Inexact _ => SpecFloatCopy.loc_Inexact Lt end:SpecFloatCopy.locationH1:l <> SpecFloatCopy.loc_ExactH2:l' = SpecFloatCopy.loc_Inexact Ltinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)(* k <> 0 *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match (2 * k + 1 ?= nb_steps)%Z with | Eq => match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end | Lt => Lt | Gt => Gt end)(* . 2 * k + 1 < nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k + 1 < nb_steps)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k + 1 < nb_steps)%Z(0 < k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)(* . 2 * k + 1 = nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact match l with | SpecFloatCopy.loc_Exact => Lt | SpecFloatCopy.loc_Inexact l0 => l0 end)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:ZHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x SpecFloatCopy.loc_ExactHk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Lt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zc:comparisonHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact c)Hk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact c)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zc:comparisonHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x (SpecFloatCopy.loc_Inexact c)Hk0:k <> 0%ZHk1:(2 * k + 1)%Z = nb_stepsinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact c)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)(* . 2 * k + 1 > nb_steps *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zinbetween start (start + IZR nb_steps * step) x (SpecFloatCopy.loc_Inexact Gt)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Z(nb_steps < 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Z(k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zx0:ZH:nb_steps = (2 * x0 + (if Z.even nb_steps then 0 else 1))%Z(nb_steps < 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Z(k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Zx0:ZH:nb_steps = (2 * x0 + 1)%Z(nb_steps < 2 * k)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Z(k < nb_steps)%Zapply Hk. Qed. Definition new_location := if Z.even nb_steps then new_location_even else new_location_odd.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%ZHo:Z.even nb_steps = falsex:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHk0:k <> 0%ZHk1:(nb_steps < 2 * k + 1)%Z(k < nb_steps)%Zstart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zforall (x : R) (k : Z) (l : SpecFloatCopy.location), (0 <= k < nb_steps)%Z -> inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x l -> inbetween start (start + IZR nb_steps * step) x (new_location k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x (new_location k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x linbetween start (start + IZR nb_steps * step) x ((if Z.even nb_steps then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lnb_steps = nb_steps -> (0 < nb_steps)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even nb_steps then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lnb_steps = 0%Z -> (0 < 0)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even 0 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.pos p -> (0 < Z.pos p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)(* . *)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.pos p -> (0 < Z.pos p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~1inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p~1) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~0inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p~0) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHp:nb_steps = 1%Zinbetween start (start + IZR nb_steps * step) x ((if Z.even 1 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~1Z.even nb_steps = falsestart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~0inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p~0) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHp:nb_steps = 1%Zinbetween start (start + IZR nb_steps * step) x ((if Z.even 1 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~0inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.pos p~0) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHp:nb_steps = 1%Zinbetween start (start + IZR nb_steps * step) x ((if Z.even 1 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lp:positiveHp:nb_steps = Z.pos p~0Z.even nb_steps = truestart, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHp:nb_steps = 1%Zinbetween start (start + IZR nb_steps * step) x ((if Z.even 1 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lHp:nb_steps = 1%Zinbetween start (start + IZR nb_steps * step) x ((if Z.even 1 then new_location_even else new_location_odd) k l)start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)(* . *) now intros p _. Qed. End Fcalc_bracket_step. Section Fcalc_bracket_scale.start, step:Rnb_steps:ZHstep:(0 < step)%RHnb_steps:(1 < nb_steps)%Zx:Rk:Zl:SpecFloatCopy.locationHk:(0 <= k < nb_steps)%ZHx:inbetween (start + IZR k * step) (start + IZR (k + 1) * step) x lforall p : positive, nb_steps = Z.neg p -> (0 < Z.neg p)%Z -> inbetween start (start + IZR nb_steps * step) x ((if Z.even (Z.neg p) then new_location_even else new_location_odd) k l)forall x d s : R, ((x * s + d * s) / 2)%R = ((x + d) / 2 * s)%Rforall x d s : R, ((x * s + d * s) / 2)%R = ((x + d) / 2 * s)%Rfield. Qed.x, d, s:R((x * s + d * s) / 2)%R = ((x + d) / 2 * s)%Rforall (x d u : R) (l : SpecFloatCopy.location) (s : R), (0 < s)%R -> inbetween x d u l -> inbetween (x * s) (d * s) (u * s) lforall (x d u : R) (l : SpecFloatCopy.location) (s : R), (0 < s)%R -> inbetween x d u l -> inbetween (x * s) (d * s) (u * s) lx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%RHx:u = x(u * s)%R = (x * s)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'(x * s < u * s < d * s)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'Rcompare (u * s) ((x * s + d * s) / 2) = l'x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'(x * s < u * s < d * s)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'Rcompare (u * s) ((x * s + d * s) / 2) = l'x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'Rcompare (u * s) ((x * s + d * s) / 2) = l'now rewrite Rcompare_mult_r. Qed.x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x < u < d)%RHl:Rcompare u ((x + d) / 2) = l'Rcompare (u * s) ((x + d) / 2 * s) = l'forall (x d u : R) (l : SpecFloatCopy.location) (s : R), (0 < s)%R -> inbetween (x * s) (d * s) (u * s) l -> inbetween x d u lforall (x d u : R) (l : SpecFloatCopy.location) (s : R), (0 < s)%R -> inbetween (x * s) (d * s) (u * s) l -> inbetween x d u lx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%RHx:(u * s)%R = (x * s)%Ru = xx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'(x < u < d)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'Rcompare u ((x + d) / 2) = l'x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%RHx:(u * s)%R = (x * s)%Rs <> 0%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'(x < u < d)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'Rcompare u ((x + d) / 2) = l'x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'(x < u < d)%Rx, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'Rcompare u ((x + d) / 2) = l'x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'Rcompare u ((x + d) / 2) = l'now rewrite inbetween_mult_aux in Hl. Qed. End Fcalc_bracket_scale. Section Fcalc_bracket_generic. Variable beta : radix. Notation bpow e := (bpow beta e).x, d, u:Rl:SpecFloatCopy.locations:RHs:(0 < s)%Rl':comparisonHx:(x * s < u * s < d * s)%RHl:Rcompare (u * s) ((x * s + d * s) / 2) = l'Rcompare (u * s) ((x + d) / 2 * s) = l'
Specialization of inbetween for two consecutive floating-point numbers.
Definition inbetween_float m e x l := inbetween (F2R (Float beta m e)) (F2R (Float beta (m + 1) e)) x l.beta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location), inbetween_float m e x l -> (F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location), inbetween_float m e x l -> (F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(F2R {| Fnum := m; Fexp := e |} <= F2R {| Fnum := m; Fexp := e |} < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(F2R {| Fnum := m; Fexp := e |} <= F2R {| Fnum := m; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(F2R {| Fnum := m; Fexp := e |} < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(F2R {| Fnum := m; Fexp := e |} < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:x = F2R {| Fnum := m; Fexp := e |}(m < m + 1)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x < F2R {| Fnum := m + 1; Fexp := e |})%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(F2R {| Fnum := m; Fexp := e |} <= x)%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(x < F2R {| Fnum := m + 1; Fexp := e |})%Rapply Hx. Qed.beta:radixx:Rm, e:Zl:SpecFloatCopy.locationl':comparisonHx:(F2R {| Fnum := m; Fexp := e |} < x < F2R {| Fnum := m + 1; Fexp := e |})%RHl:Rcompare x ((F2R {| Fnum := m; Fexp := e |} + F2R {| Fnum := m + 1; Fexp := e |}) / 2) = l'(x < F2R {| Fnum := m + 1; Fexp := e |})%R
Specialization of inbetween for two consecutive integers.
Definition inbetween_int m x l := inbetween (IZR m) (IZR (m + 1)) x l.beta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location) (k : Z), (0 < k)%Z -> inbetween_float m e x l -> inbetween_float (m / beta ^ k) (e + k) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location) (k : Z), (0 < k)%Z -> inbetween_float m e x l -> inbetween_float (m / beta ^ k) (e + k) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween_float m e x linbetween_float (m / beta ^ k) (e + k) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x linbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lforall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixe, k:ZHk:(0 < k)%Zforall m : Z, F2R {| Fnum := m; Fexp := e + k |} = F2R {| Fnum := m * beta ^ k; Fexp := e |}beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixe, k:ZHk:(0 < k)%Zm:ZF2R {| Fnum := m; Fexp := e + k |} = F2R {| Fnum := m * beta ^ k; Fexp := e |}beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixe, k:ZHk:(0 < k)%Zm:ZF2R {| Fnum := m * beta ^ (e + k - e); Fexp := e |} = F2R {| Fnum := m * beta ^ k; Fexp := e |}beta:radixe, k:ZHk:(0 < k)%Zm:Z(e <= e + k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixe, k:ZHk:(0 < k)%Zm:Z(e + k - e)%Z = kbeta:radixe, k:ZHk:(0 < k)%Zm:Z(e <= e + k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixe, k:ZHk:(0 < k)%Zm:Z(e <= e + k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}inbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}(beta ^ k > 0)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}(0 < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}(0 <= k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)(* . *)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k; Fexp := e + k |}) (F2R {| Fnum := m / beta ^ k + 1; Fexp := e + k |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k * beta ^ k; Fexp := e |}) (F2R {| Fnum := (m / beta ^ k + 1) * beta ^ k; Fexp := e |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k * beta ^ k; Fexp := e |}) (F2R {| Fnum := m / beta ^ k * beta ^ k + beta ^ k; Fexp := e |}) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k * beta ^ k; Fexp := e |}) (IZR (Fnum {| Fnum := m / beta ^ k * beta ^ k + beta ^ k; Fexp := e |}) * bpow (Fexp {| Fnum := m / beta ^ k * beta ^ k + beta ^ k; Fexp := e |})) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k * beta ^ k; Fexp := e |}) (IZR (m / beta ^ k * beta ^ k + beta ^ k) * bpow e) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (F2R {| Fnum := m / beta ^ k * beta ^ k; Fexp := e |}) (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (beta ^ k) * bpow e) x (new_location (beta ^ k) (m mod beta ^ k) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(0 < bpow e)%Rbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(1 < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(0 <= m mod beta ^ k < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k) * bpow e) (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k + 1) * bpow e) x lbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(1 < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(0 <= m mod beta ^ k < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k) * bpow e) (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k + 1) * bpow e) x lbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Z(0 <= m mod beta ^ k < beta ^ k)%Zbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k) * bpow e) (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k + 1) * bpow e) x lbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k) * bpow e) (IZR (m / beta ^ k * beta ^ k) * bpow e + IZR (m mod beta ^ k + 1) * bpow e) x lbeta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (m / beta ^ k * beta ^ k + m mod beta ^ k) * bpow e) (IZR (m / beta ^ k * beta ^ k + (m mod beta ^ k + 1)) * bpow e) x lnow rewrite <- Z_div_mod_eq. Qed.beta:radixx:Rm, e:Zl:SpecFloatCopy.locationk:ZHk:(0 < k)%ZHx:inbetween (F2R {| Fnum := m; Fexp := e |}) (F2R {| Fnum := m + 1; Fexp := e |}) x lHr:forall m0 : Z, F2R {| Fnum := m0; Fexp := e + k |} = F2R {| Fnum := m0 * beta ^ k; Fexp := e |}Hp:(beta ^ k > 0)%Zinbetween (IZR (beta ^ k * (m / beta ^ k) + m mod beta ^ k) * bpow e) (IZR (beta ^ k * (m / beta ^ k) + m mod beta ^ k + 1) * bpow e) x lbeta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location), inbetween_float m e x l -> inbetween_float (m / beta) (e + 1) x (new_location beta (m mod beta) l)beta:radixforall (x : R) (m e : Z) (l : SpecFloatCopy.location), inbetween_float m e x l -> inbetween_float (m / beta) (e + 1) x (new_location beta (m mod beta) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:inbetween_float m e x linbetween_float (m / beta) (e + 1) x (new_location beta (m mod beta) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:inbetween_float m e x linbetween_float (m / beta ^ 1) (e + 1) x (new_location (beta ^ 1) (m mod beta ^ 1) l)beta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:inbetween_float m e x l(beta ^ 1)%Z = betaapply Zmult_1_r. Qed.beta:radixx:Rm, e:Zl:SpecFloatCopy.locationHx:inbetween_float m e x l(beta ^ 1)%Z = betabeta:radixforall (m e : Z) (l : SpecFloatCopy.location), exists x : R, inbetween_float m e x lbeta:radixforall (m e : Z) (l : SpecFloatCopy.location), exists x : R, inbetween_float m e x lbeta:radixm, e:Zl:SpecFloatCopy.locationexists x : R, inbetween_float m e x lbeta:radixm, e:Zl:SpecFloatCopy.location(F2R {| Fnum := m; Fexp := e |} < F2R {| Fnum := m + 1; Fexp := e |})%Rapply Zlt_succ. Qed.beta:radixm, e:Zl:SpecFloatCopy.location(m < m + 1)%Zbeta:radixforall (x : R) (e m : Z) (l : SpecFloatCopy.location) (m' : Z) (l' : SpecFloatCopy.location), inbetween_float m e x l -> inbetween_float m' e x l' -> m = m' /\ l = l'beta:radixforall (x : R) (e m : Z) (l : SpecFloatCopy.location) (m' : Z) (l' : SpecFloatCopy.location), inbetween_float m e x l -> inbetween_float m' e x l' -> m = m' /\ l = l'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'm = m' /\ l = l'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'Hm:m = m'l = l'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'm = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m e x l'Hm:m = m'l = l'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'm = m'beta:radixx:Re, m:Zl, l':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m e x l'l = l'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'm = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'm = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'H1:(F2R {| Fnum := m; Fexp := e |} <= x)%RH2:(x < F2R {| Fnum := m + 1; Fexp := e |})%Rm = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'H1:(F2R {| Fnum := m; Fexp := e |} <= x)%RH2:(x < F2R {| Fnum := m + 1; Fexp := e |})%RH3:(F2R {| Fnum := m'; Fexp := e |} <= x)%RH4:(x < F2R {| Fnum := m' + 1; Fexp := e |})%Rm = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'H1:(F2R {| Fnum := m; Fexp := e |} <= x)%RH2:(x < F2R {| Fnum := m + 1; Fexp := e |})%RH3:(F2R {| Fnum := m'; Fexp := e |} <= x)%RH4:(x < F2R {| Fnum := m' + 1; Fexp := e |})%R(m < m' + 1)%Z /\ (m' < m + 1)%Z -> m = m'beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'H1:(F2R {| Fnum := m; Fexp := e |} <= x)%RH2:(x < F2R {| Fnum := m + 1; Fexp := e |})%RH3:(F2R {| Fnum := m'; Fexp := e |} <= x)%RH4:(x < F2R {| Fnum := m' + 1; Fexp := e |})%R(m < m' + 1)%Z /\ (m' < m + 1)%Znow split ; apply lt_F2R with beta e ; apply Rle_lt_trans with x. Qed. End Fcalc_bracket_generic.beta:radixx:Re, m:Zl:SpecFloatCopy.locationm':Zl':SpecFloatCopy.locationH:inbetween_float m e x lH':inbetween_float m' e x l'H1:(F2R {| Fnum := m; Fexp := e |} <= x)%RH2:(x < F2R {| Fnum := m + 1; Fexp := e |})%RH3:(F2R {| Fnum := m'; Fexp := e |} <= x)%RH4:(x < F2R {| Fnum := m' + 1; Fexp := e |})%R(m < m' + 1)%Z /\ (m' < m + 1)%Z