~ubuntu-branches/debian/sid/coq-float/sid : revision 13

1

Require Import AllFloat.

2

Require Import Veltkamp.

3

4

Section AFZ.

5

Variable b : Fbound.

6

Variable radix : Z.

7

Variable precision : nat.

8

9

Coercion Local FtoRradix := FtoR radix.

10

Hypothesis radixMoreThanOne : (1 < radix)%Z.

11

Hypothesis precisionGreaterThanOne : 1 < precision.

12

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix precision.

13

14

15

Definition AFZClosest (r : R) (p : float) :=

16

Closest b radix r p /\

17

((Rabs r <= Rabs p)%R \/ (forall q : float, Closest b radix r q -> q = p :>R)).

18

19

Theorem AFZClosestTotal : TotalP AFZClosest.

20

red in |- *; intros r.

21

case MinEx with (r := r) (3 := pGivesBound); auto with arith.

22

intros min H'.

23

case MaxEx with (r := r) (3 := pGivesBound); auto with arith.

24

intros max H'0.

25

cut (min <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'); auto ].

26

cut (r <= max)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'0) ].

27

case (Rle_or_lt (r - min) (max - r)); intros H'1.

28

case H'1; intros H'2; auto.

29

exists min; split.

30

apply ClosestMin with (max := max); auto.

31

replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

32

apply Rminus_le; auto.

33

fold FtoRradix; replace (r + r - (min + max))%R with (r - min - (max - r))%R;

34

[ idtac | simpl in |- *; ring ].

35

apply Rle_minus; auto.

36

right; intros q H'3.

37

apply ClosestMinEq with (r := r) (max := max) (b:=b) ; auto.

38

fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

39

apply Rminus_lt; auto.

40

replace (r + r - (min + max))%R with (r - min - (max - r))%R;

41

[ idtac | simpl in |- *; ring ].

42

apply Rlt_minus; auto.

43

case (Rle_or_lt (Rabs r) (Rabs min)); intros G.

44

exists min; split; auto.

45

apply ClosestMin with (max := max); auto.

46

fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

47

apply Rminus_le; auto.

48

replace (r + r - (min + max))%R with (r - min - (max - r))%R;

49

[ idtac | simpl in |- *; ring ].

50

apply Rle_minus; auto.

51

exists max; split; auto.

52

apply ClosestMax with (min := min); auto.

53

fold FtoRradix; replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

54

apply Rminus_le; auto.

55

replace (min + max - (r + r))%R with (max - r - (r - min))%R;

56

[ idtac | simpl in |- *; ring ].

57

apply Rle_minus; auto.

58

rewrite H'2; auto with real.

59

case (Rle_or_lt 0 r); intros M.

60

left; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

61

apply Rle_trans with (1:=M); auto.

62

absurd ((Rabs min < Rabs r)%R); auto.

63

apply Rle_not_lt.

64

repeat rewrite Rabs_left1; auto with real.

65

apply Rle_trans with (1:=Rl1); auto with real.

66

exists max; split; auto.

67

apply ClosestMax with (min := min); auto.

68

replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

69

apply Rminus_le; auto.

70

fold FtoRradix; replace (min + max - (r + r))%R with (max - r - (r - min))%R;

71

[ idtac | simpl in |- *; ring ].

72

apply Rle_minus; auto with real.

73

right; intros q H'2.

74

apply ClosestMaxEq with (r := r) (min := min) (b:=b); auto.

75

replace (2%nat * r)%R with (r + r)%R; [ idtac | simpl in |- *; ring ].

76

apply Rminus_lt; auto.

77

fold FtoRradix; replace (min + max - (r + r))%R with (max - r - (r - min))%R;

78

[ idtac | simpl in |- *; ring ].

79

apply Rlt_minus; auto.

80

Qed.

81

82

83

Theorem AFZClosestCompatible : CompatibleP b radix AFZClosest.

84

red in |- *; simpl in |- *.

85

intros r1 r2 p q H' H'0 H'1 H'2; red in |- *.

86

inversion H'.

87

split.

88

apply (ClosestCompatible b radix r1 r2 p q); auto.

89

case H0; intros H1.

90

left.

91

rewrite <- H'0; fold FtoRradix in H'1; rewrite <- H'1; auto.

92

right; intros q0 H'3.

93

unfold FtoRradix in |- *; rewrite <- H'1; auto.

94

apply H1; auto.

95

apply (ClosestCompatible b radix r2 r1 q0 q0); auto.

96

case H'3; auto.

97

Qed.

98

99

100

101

Theorem AFZClosestMinOrMax : MinOrMaxP b radix AFZClosest.

102

red in |- *; intros r p H'; case (ClosestMinOrMax b radix r p); auto.

103

case H'; auto.

104

Qed.

105

106

Theorem AFZClosestMonotone : MonotoneP radix AFZClosest.

107

red in |- *; simpl in |- *; intros p q p' q' H' H'0 H'1.

108

apply (ClosestMonotone b radix p q); auto; case H'0; case H'1; auto.

109

Qed.

110

111

Theorem AFZClosestRoundedModeP : RoundedModeP b radix AFZClosest.

112

red in |- *; split.

113

exact AFZClosestTotal.

114

split.

115

exact AFZClosestCompatible.

116

split.

117

exact AFZClosestMinOrMax.

118

exact AFZClosestMonotone.

119

Qed.

120

121

Theorem AFZClosestUniqueP : UniqueP radix AFZClosest.

122

red in |- *; simpl in |- *.

123

intros r p q H' H'0.

124

inversion H'; inversion H'0; case H0; case H2; auto.

125

intros H'1 H'2; case (AFZClosestMinOrMax r p);

126

case (AFZClosestMinOrMax r q); auto.

127

intros H'3 H'4; apply (MinUniqueP b radix r); auto.

128

intros H'3 H'4; case (Req_dec p q); auto; intros H'5.

129

Contradict H'1; auto.

130

apply Rlt_not_le.

131

cut (p <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'4); auto ].

132

cut (r <= q)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'3) ].

133

assert (FtoRradix p=r -> False).

134

intros; Contradict H'5.

135

apply

136

(RoundedProjector b radix _

137

(MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne

138

pGivesBound)); auto.

139

case H'4; auto.

140

fold FtoRradix; rewrite H3; auto.

141

case (Rle_or_lt 0 r); intros G.

142

absurd ( (Rabs r <= Rabs p)%R); auto.

143

apply Rlt_not_le; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

144

case Rl1; auto.

145

intros; absurd False; auto; apply H3; auto.

146

apply RleMinR0 with b precision r; auto with real zarith.

147

repeat rewrite Rabs_left1; auto with real.

148

case Rl2; auto with real.

149

intros; Contradict H'5; apply sym_eq.

150

apply

151

(RoundedProjector b radix _

152

(MinRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne

153

pGivesBound)); auto.

154

case H'3; auto.

155

fold FtoRradix; rewrite <- H4; auto.

156

apply RleMaxR0 with b precision r; auto with real zarith.

157

intros H'3 H'4; case (Req_dec p q); auto; intros H'5.

158

Contradict H'1; auto.

159

apply Rlt_not_le.

160

cut (q <= r)%R; [ intros Rl1 | apply isMin_inv1 with (1 := H'3); auto ].

161

cut (r <= p)%R; [ intros Rl2 | apply isMax_inv1 with (1 := H'4) ].

162

case (Rle_or_lt 0 r); intros G.

163

repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

164

case Rl1; auto with real.

165

intros; Contradict H'5; apply sym_eq.

166

apply

167

(RoundedProjector b radix _

168

(MaxRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne

169

pGivesBound)); auto.

170

case H'3; auto.

171

fold FtoRradix; rewrite H3; auto.

172

apply RleMinR0 with b precision r; auto with real zarith.

173

absurd ( (Rabs r <= Rabs p)%R); auto.

174

apply Rlt_not_le; repeat rewrite Rabs_left1; auto with real.

175

case Rl2; auto with real.

176

intros; Contradict H'5.

177

apply

178

(RoundedProjector b radix _

179

(MinRoundedModeP _ _ _ radixMoreThanOne precisionGreaterThanOne

180

pGivesBound)); auto.

181

case H'4; auto.

182

fold FtoRradix; rewrite <- H3; auto.

183

apply RleMaxR0 with b precision r; auto with real zarith.

184

intros H'3 H'4; apply (MaxUniqueP b radix r); auto.

185

intros H'1 H'2; apply sym_eq; auto.

186

Qed.

187

188

189

Theorem AFZClosestSymmetric : SymmetricP AFZClosest.

190

red in |- *; intros r p H'; case H'; clear H'.

191

intros H' H'0; case H'0; clear H'0; intros H'0.

192

split; auto.

193

apply (ClosestSymmetric b radix r p); auto.

194

left.

195

unfold FtoRradix; rewrite Fopp_correct; auto with zarith.

196

repeat rewrite Rabs_Ropp; auto with real.

197

split; auto.

198

apply (ClosestSymmetric b radix r p); auto.

199

right.

200

intros q H'1.

201

cut (Fopp q = p :>R).

202

intros H'2; unfold FtoRradix in |- *; rewrite Fopp_correct.

203

unfold FtoRradix in H'2; rewrite <- H'2.

204

rewrite Fopp_correct; ring.

205

apply H'0; auto.

206

replace r with (- - r)%R; [ idtac | ring ].

207

apply (ClosestSymmetric b radix (- r)%R q); auto.

208

Qed.

209

210

End AFZ.

211

Section Closest2.

212

Variable b : Fbound.

213

Variable prec : nat.

214

Variable radix:Z.

215

216

Let FtoRradix := FtoR radix.

217

Coercion FtoRradix : float >-> R.

218

219

220

Hypothesis radixMoreThanOne : (1 < radix)%Z.

221

Hypothesis precisionGreaterThan : 1 < prec.

222

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.

223

224

225

Lemma ClosestClosestPredSucc: forall (f g:float) (r:R),

226

(Closest b radix r f) -> (Closest b radix r g) ->

227

(FtoRradix f=g)

228

\/ (FtoRradix f=FNPred b radix prec g)

229

\/ (FtoRradix f=FNSucc b radix prec g).

230

intros.

231

elim H; intros Bf T; elim H0; intros Bg T'; clear T T'.

232

case (ClosestMinOrMax b radix r f); auto; intros T1;

233

case (ClosestMinOrMax b radix r g); auto; intros T2.

234

left; unfold FtoRradix; apply (MinUniqueP b radix r); auto.

235

assert (f <= g)%R.

236

elim T1; elim T2; intros; apply Rle_trans with r; intuition.

237

case H1; auto; intros.

238

right; left; unfold FtoRradix.

239

rewrite <- FnormalizeCorrect with radix b prec f; auto with zarith.

240

rewrite <- FPredSuc with b radix prec (Fnormalize radix b prec f); auto with zarith.

241

2: apply FnormalizeCanonic; auto with zarith.

242

unfold FNPred.

243

replace (FSucc b radix prec (Fnormalize radix b prec f)) with (Fnormalize radix b prec g); auto.

244

apply FcanonicUnique with radix b prec; auto with zarith float.

245

unfold FtoRradix; apply (MaxUniqueP b radix r); auto.

246

apply (MaxCompatible b radix r r g); auto with real zarith float.

247

rewrite FnormalizeCorrect; auto with zarith real.

248

apply MinMax; auto with zarith.

249

fold FtoRradix; Contradict H2.

250

replace (FtoRradix f) with (FtoRradix g); auto with real.

251

apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

252

eapply ClosestRoundedModeP; eauto.

253

fold FtoRradix; rewrite <- H2; auto.

254

assert (g <= f)%R.

255

elim T1; elim T2; intros; apply Rle_trans with r; intuition.

256

case H1; auto; intros.

257

right; right; unfold FtoRradix.

258

unfold FtoRradix; apply (MaxUniqueP b radix r); auto.

259

apply MinMax; auto with zarith.

260

fold FtoRradix; Contradict H2.

261

replace (FtoRradix f) with (FtoRradix g); auto with real.

262

apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

263

eapply ClosestRoundedModeP; eauto.

264

fold FtoRradix; rewrite <- H2; auto.

265

left; unfold FtoRradix; apply (MaxUniqueP b radix r); auto.

266

Qed.

267

268

269

270

Lemma ClosestStrictMonotone2l: forall (r1 r2 : R) (f1 f2 : float),

271

Closest b radix r1 f1 -> (Fcanonic radix b f2) ->

272

(Rabs (r2 - f2) < Rabs (r2 - FSucc b radix prec f2))%R ->

273

(Rabs (r2 - f2) < Rabs (r2 - FPred b radix prec f2))%R ->

274

(r2 <= r1)%R ->

275

(FtoRradix f2 <= FtoRradix f1)%R.

276

intros.

277

assert (Closest b radix r2 f2).

278

apply ClosestSuccPred with prec; auto with real.

279

eapply FcanonicBound; eauto.

280

case H3; intros.

281

generalize ClosestMonotone; unfold MonotoneP; intros T.

282

unfold FtoRradix; apply T with b r2 r1; auto.

283

case (ClosestClosestPredSucc f1 f2 r1); auto with real.

284

rewrite <- H5; auto.

285

intros K; case K; intros.

286

absurd ( (Rabs (r2 - f2) < Rabs (r2 - f1)))%R.

287

apply Rle_not_lt.

288

rewrite <- Rabs_Ropp with (r2-f1)%R; rewrite <- Rabs_Ropp with (r2-f2)%R.

289

replace (-(r2-f1))%R with (f1-r2)%R by ring.

290

replace (-(r2-f2))%R with (f2-r2)%R by ring.

291

rewrite H5.

292

elim H; intros T1 T2; apply T2; auto.

293

elim H4; auto.

294

rewrite H6; unfold FNPred.

295

rewrite FcanonicFnormalizeEq; auto with zarith real.

296

rewrite H6; left; apply FNSuccLt; auto with zarith.

297

Qed.

298

299

Lemma ClosestStrictMonotone2r: forall (r1 r2 : R) (f1 f2 : float),

300

Closest b radix r1 f1 -> (Fcanonic radix b f2) ->

301

(Rabs (r2 - f2) < Rabs (r2 - FSucc b radix prec f2))%R ->

302

(Rabs (r2 - f2) < Rabs (r2 - FPred b radix prec f2))%R ->

303

(r1 <= r2)%R ->

304

(FtoRradix f1 <= FtoRradix f2)%R.

305

intros.

306

assert (Closest b radix r2 f2).

307

apply ClosestSuccPred with prec; auto with real.

308

eapply FcanonicBound; eauto.

309

case H3; intros.

310

generalize ClosestMonotone; unfold MonotoneP; intros T.

311

unfold FtoRradix; apply T with b r1 r2; auto.

312

case (ClosestClosestPredSucc f1 f2 r1); auto with real.

313

rewrite H5; auto.

314

intros K; case K; intros.

315

rewrite H6; left; apply FNPredLt; auto with zarith.

316

absurd ( (Rabs (r2 - f2) < Rabs (r2 - f1)))%R.

317

apply Rle_not_lt.

318

rewrite <- Rabs_Ropp with (r2-f1)%R; rewrite <- Rabs_Ropp with (r2-f2)%R.

319

replace (-(r2-f1))%R with (f1-r2)%R by ring.

320

replace (-(r2-f2))%R with (f2-r2)%R by ring.

321

rewrite <- H5.

322

elim H; intros T1 T2; apply T2; auto.

323

elim H4; auto.

324

rewrite H6; unfold FNSucc.

325

rewrite FcanonicFnormalizeEq; auto with zarith real.

326

Qed.

327

328

Lemma ClosestStrictEq: forall (r : R) (f1 f2 : float),

329

Closest b radix r f1 -> (Fcanonic radix b f2) ->

330

(Rabs (r - f2) < Rabs (r - FSucc b radix prec f2))%R ->

331

(Rabs (r - f2) < Rabs (r - FPred b radix prec f2))%R ->

332

(FtoRradix f1 = FtoRradix f2)%R.

333

intros.

334

assert (FtoRradix f1 <= f2)%R.

335

apply ClosestStrictMonotone2r with r r; auto with real.

336

assert (FtoRradix f2 <= f1)%R; auto with real.

337

apply ClosestStrictMonotone2l with r r; auto with real.

338

Qed.

339

340

341

End Closest2.

342

343

344

345

Section PredComput.

346

Variable b : Fbound.

347

Variable prec : nat.

348

Variable radix radixH : Z.

349

350

Let FtoRradix := FtoR radix.

351

Coercion FtoRradix : float >-> R.

352

353

Hypothesis radixMoreThanOne : (1 < radix)%Z.

354

Hypothesis precisionGreaterThan : 3 <= prec.

355

Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat radix prec.

356

Hypotheses ReasonnableFormat: (2*prec-1 <= dExp b)%Z.

357

Hypotheses radixEven: (radix=2*radixH)%Z.

358

359

Lemma radixHPos: (0 < radixH)%Z.

360

apply Zmult_lt_reg_r with 2%Z; auto with zarith.

361

Qed.

362

363

Hint Resolve radixHPos.

364

365

366

Lemma RoundedToZero_aux: forall (c:float) (r:R),

367

(Fcanonic radix b c) ->

368

(0 <= r)%R ->

369

(r < /2 * powerRZ radix (-dExp b))%R ->

370

(Closest b radix r c) ->

371

(FtoRradix c=0)%R.

372

intros.

373

assert (0 <= c)%R.

374

unfold FtoRradix; apply RleRoundedR0 with b prec (Closest b radix) r; auto with real zarith.

375

apply ClosestRoundedModeP with prec; auto with zarith.

376

case H3; auto; clear H3; intros H3.

377

elim H2; intros.

378

absurd (Rabs (c-r) <= Rabs r)%R.

379

apply Rlt_not_le.

380

apply Rlt_le_trans with (Rabs c -Rabs r)%R;[idtac|apply Rabs_triang_inv].

381

repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

382

apply Rplus_lt_reg_r with r.

383

replace (r+r)%R with (2*r)%R;[idtac| ring].

384

apply Rlt_le_trans with (2*(/ 2 * powerRZ radix (- dExp b)))%R.

385

apply Rmult_lt_compat_l; auto with real.

386

apply Rle_trans with (powerRZ radix (- dExp b)).

387

right; simpl; field; auto with real.

388

apply Rle_trans with c;[idtac|right; ring].

389

apply Rle_trans with (FSucc b radix prec (Float 0 (-(dExp b)))).

390

right; rewrite FSuccSimpl4; auto with zarith.

391

unfold FtoRradix, FtoR, Zsucc; simpl; ring.

392

simpl; assert (0 < pPred (vNum b))%Z; auto with zarith.

393

apply pPredMoreThanOne with radix prec; auto with zarith.

394

simpl; assert (0 < nNormMin radix prec)%Z; auto with zarith.

395

unfold nNormMin; auto with zarith.

396

unfold FtoRradix; apply FSuccProp; auto with zarith.

397

right; split; split; simpl; auto with zarith.

398

replace (radix*0)%Z with 0%Z; simpl; auto with zarith.

399

apply Rle_lt_trans with 0%R; auto with real zarith.

400

unfold FtoR; simpl; right; ring.

401

rewrite <- (Rabs_Ropp r).

402

replace (-r)%R with (FtoRradix (Float 0 (-(dExp b)))-r)%R.

403

apply H5.

404

split; simpl; auto with zarith.

405

unfold FtoRradix, FtoR; simpl; ring.

406

Qed.

407

408

409

410

Lemma RoundedToZero_aux2: forall (c:float) (r:R),

411

(Fcanonic radix b c) ->

412

(Rabs r < /2 * powerRZ radix (-dExp b))%R ->

413

(Closest b radix r c) ->

414

(FtoRradix c=0)%R.

415

intros.

416

case (Rle_or_lt 0 r); intros.

417

apply RoundedToZero_aux with r; auto.

418

rewrite <- (Rabs_right r); try apply Rle_ge; auto.

419

apply Rmult_eq_reg_l with (-1)%R; auto with real.

420

apply trans_eq with 0%R;[idtac|ring].

421

apply trans_eq with (FtoRradix (Fopp c)).

422

unfold FtoRradix; rewrite Fopp_correct; ring.

423

apply RoundedToZero_aux with (-r)%R; auto with real.

424

apply FcanonicFopp; auto.

425

rewrite <- (Rabs_left r); auto with real.

426

apply ClosestOpp; auto.

427

Qed.

428

429

Lemma RoundedToZero: forall (c:float) (r:R),

430

(Rabs r < /2 * powerRZ radix (-dExp b))%R ->

431

(Closest b radix r c) ->

432

(FtoRradix c=0)%R.

433

intros.

434

unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec c; auto with zarith.

435

fold FtoRradix; apply RoundedToZero_aux2 with r; auto.

436

apply FnormalizeCanonic; auto with zarith.

437

elim H0; auto.

438

generalize ClosestCompatible; unfold CompatibleP.

439

intros T; apply T with r c; auto with zarith float.

440

rewrite FnormalizeCorrect; auto with zarith real.

441

apply FnormalizeBounded; auto with zarith.

442

elim H0; auto.

443

Qed.

444

445

446

Definition u:= powerRZ radix (-prec).

447

Definition phi:=(u*(radixH+radix*u))%R.

448

Definition eta:= powerRZ radix (-(dExp b)).

449

450

451

452

Lemma phi_Pos: (0 < phi)%R.

453

unfold phi,u.

454

apply Rle_lt_trans with (powerRZ radix (- prec)*0)%R; auto with real.

455

apply Rmult_lt_compat_l; auto with real zarith.

456

apply Rle_lt_trans with (0+radix*0)%R; [right; ring|idtac].

457

apply Rplus_lt_compat; auto with real zarith.

458

Qed.

459

460

461

462

Lemma phi_bounded_aux:

463

(Zabs (radixH*nNormMin radix prec + 1) < Zpos (vNum b))%Z.

464

assert (0 < nNormMin radix prec+1)%Z.

465

apply Zlt_le_trans with (0+1)%Z; unfold nNormMin; auto with zarith.

466

rewrite Zabs_eq; auto with zarith.

467

rewrite pGivesBound; unfold nNormMin.

468

apply Zlt_le_trans with (radixH*Zpower_nat radix (pred prec)+radixH*Zpower_nat radix (pred prec))%Z; auto with zarith.

469

apply Zplus_lt_compat_l.

470

apply Zle_lt_trans with (radixH*1)%Z; auto with zarith.

471

apply Zle_lt_trans with (radixH*Zpower_nat radix 0)%Z; auto with zarith.

472

apply Zmult_lt_compat_l; auto with zarith.

473

apply Zle_trans with ((2*radixH)*Zpower_nat radix (pred prec))%Z.

474

apply Zeq_le; ring.

475

replace (2*radixH)%Z with (Zpower_nat radix 1).

476

rewrite <- Zpower_nat_is_exp; auto with zarith.

477

rewrite <- radixEven;unfold Zpower_nat;simpl; auto with zarith.

478

Qed.

479

480

Lemma phi_bounded: (exists f:float,

481

Fbounded b f /\ (FtoRradix f=phi)).

482

exists (Float (radixH*nNormMin radix prec+1) (-(2*prec-1))); split.

483

split.

484

apply Zle_lt_trans with (Zabs (radixH*nNormMin radix prec+1))%Z; auto with zarith.

485

apply phi_bounded_aux.

486

apply Zle_trans with (-(2*prec-1))%Z; auto with zarith.

487

unfold FtoRradix, FtoR, pPred, phi, u.

488

replace (IZR (Fnum (Float (radixH*nNormMin radix prec + 1) (- (2 * prec - 1))))) with

489

(radixH*powerRZ radix (prec-1) +1)%R.

490

replace (Fexp (Float (radixH*nNormMin radix prec + 1) (- (2 * prec - 1)))) with (-(2*prec-1))%Z; auto with zarith.

491

apply trans_eq with (radixH*((powerRZ radix (prec-1)*powerRZ radix (- (2 * prec-1))))

492

+ powerRZ radix (- (2 * prec-1)))%R;[ring|idtac].

493

apply trans_eq with (radixH*powerRZ radix (- prec)

494

+ radix * (powerRZ radix (- prec) * powerRZ radix (- prec)))%R;[idtac|ring].

495

repeat rewrite <- powerRZ_add; auto with real zarith.

496

replace (prec -1+ - (2 * prec-1))%Z with (-prec)%Z; auto with zarith.

497

pattern (IZR radix) at 4; replace (IZR radix) with (powerRZ radix 1); auto with zarith.

498

rewrite <- powerRZ_add; auto with real zarith.

499

replace (1+(- prec + - prec))%Z with (-(2*prec-1))%Z; auto with zarith real.

500

simpl; auto with real.

501

apply trans_eq with (IZR (radixH*nNormMin radix prec+1)); auto with zarith real.

502

rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

503

rewrite inj_pred; auto with zarith.

504

Qed.

505

506

Lemma GepetaGeExp: forall (c:float),

507

Fcanonic radix b c ->

508

(powerRZ radix (prec-dExp b) <= c)%R ->

509

(-dExp b < Fexp c)%Z.

510

intros.

511

assert (-(dExp b)+1 <= Fexp c)%Z; auto with zarith.

512

apply Zle_trans with (Fexp (Float (nNormMin radix prec) (-(dExp b)+1))); auto with zarith.

513

apply Fcanonic_Rle_Zle with radix b prec; auto with zarith.

514

left; split; try split; simpl; auto with zarith.

515

rewrite Zabs_eq.

516

apply ZltNormMinVnum; auto with zarith.

517

apply Zlt_le_weak; apply nNormPos; auto with zarith.

518

rewrite PosNormMin with radix b prec; auto with zarith.

519

apply Rle_trans with (powerRZ radix (prec - dExp b)).

520

rewrite <- Fabs_correct; auto with zarith.

521

unfold FtoR, Fabs; simpl.

522

unfold nNormMin; rewrite Zabs_eq; auto with zarith.

523

rewrite Zpower_nat_Z_powerRZ.

524

rewrite <- powerRZ_add; auto with real zarith.

525

replace (pred prec + (- dExp b + 1))%Z with (prec - dExp b)%Z; auto with real.

526

rewrite inj_pred; unfold Zpred; auto with zarith.

527

fold FtoRradix; rewrite Rabs_right; auto.

528

apply Rle_ge; apply Rle_trans with (2:=H0); auto with real zarith.

529

Qed.

530

531

Lemma GepetaIsNormal: forall (c:float),

532

Fcanonic radix b c ->

533

(powerRZ radix (prec-dExp b) <= c)%R ->

534

Fnormal radix b c.

535

intros.

536

case H; intros; auto.

537

absurd (-dExp b < Fexp c)%Z.

538

elim H1; intros H2 (H3,H4); rewrite H3; auto with zarith.

539

apply GepetaGeExp; auto.

540

Qed.

541

542

543

544

Lemma predSmallOnes: forall (c:float),

545

Fcanonic radix b c ->

546

(Rabs c < powerRZ radix (prec-dExp b))%R

547

-> (FtoRradix (FPred b radix prec c) = c-eta)%R.

548

intros.

549

assert (Fexp c = (-dExp b))%Z.

550

case (Zle_lt_or_eq (-(dExp b)) (Fexp c)); auto with zarith.

551

assert (Fbounded b c); auto with zarith float.

552

apply FcanonicBound with radix; auto with zarith.

553

intros; absurd (Rabs c < Rabs c)%R; auto with real.

554

apply Rlt_le_trans with (1:=H0).

555

replace (prec-dExp b)%Z with ((prec-1)+(-dExp b+1))%Z;[idtac|ring].

556

rewrite powerRZ_add; auto with real zarith.

557

unfold FtoRradix; rewrite <- Fabs_correct; auto with zarith.

558

unfold FtoR, Fabs; simpl.

559

apply Rmult_le_compat; auto with real zarith.

560

apply Rle_trans with (IZR (nNormMin radix prec)).

561

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

562

apply Rle_powerRZ; auto with real zarith.

563

rewrite inj_pred; auto with zarith.

564

apply Rle_IZR.

565

apply pNormal_absolu_min with b; auto with zarith.

566

case H; auto; intros H2; elim H2; intros H3 (H4,H5).

567

absurd (-dExp b <Fexp c)%Z; auto with zarith.

568

apply Rle_powerRZ; auto with real zarith.

569

case (Z_eq_dec (Fnum c) (- pPred (vNum b))%Z); intros H2.

570

rewrite FPredSimpl1; auto with zarith.

571

unfold FtoRradix, FtoR, eta; simpl; rewrite H1; rewrite H2.

572

repeat rewrite Ropp_Ropp_IZR.

573

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

574

rewrite Ropp_mult_distr_l_reverse.

575

rewrite <- powerRZ_add; auto with real zarith.

576

unfold pPred, Zpred; rewrite plus_IZR.

577

rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.

578

apply trans_eq with (-(powerRZ radix prec *powerRZ radix (- dExp b)))%R;

579

[idtac|simpl; ring].

580

rewrite <- powerRZ_add; auto with real zarith.

581

replace (pred prec + Zsucc (- dExp b))%Z with (prec + - dExp b)%Z; auto with real.

582

rewrite inj_pred; unfold Zpred, Zsucc; auto with zarith.

583

case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros H3.

584

replace c with (Float (nNormMin radix prec) (- dExp b)).

585

rewrite FPredSimpl3; auto with zarith.

586

unfold FtoRradix, FtoR, Zpred, eta; simpl.

587

rewrite plus_IZR; simpl; ring.

588

apply sym_eq; apply floatEq; auto.

589

rewrite FPredSimpl4; auto.

590

unfold FtoRradix, FtoR, eta; simpl.

591

rewrite H1; unfold Zpred.

592

rewrite plus_IZR; simpl; ring.

593

Qed.

594

595

596

Lemma predNormal1: forall (c:float),

597

Fcanonic radix b c ->

598

(powerRZ radix (prec-dExp b) <= c)%R ->

599

(Fnum c=nNormMin radix prec) ->

600

(FtoRradix (FPred b radix prec c) = c-powerRZ radix (Fexp c-1))%R.

601

intros c Cc; intros.

602

rewrite FPredSimpl2; auto with zarith.

603

unfold FtoRradix, FtoR; simpl; rewrite H0; simpl.

604

unfold pPred, Zpred; rewrite plus_IZR.

605

rewrite Rmult_plus_distr_r; unfold Rminus.

606

replace (Zpos (vNum b) * powerRZ radix (Fexp c + -1))%R with

607

(nNormMin radix prec * powerRZ radix (Fexp c))%R.

608

replace ((-1)%Z * powerRZ radix (Fexp c + -1))%R with

609

(- powerRZ radix (Fexp c - 1))%R; auto with real.

610

unfold Zminus; simpl; ring.

611

unfold nNormMin; rewrite pGivesBound.

612

repeat rewrite Zpower_nat_Z_powerRZ.

613

repeat rewrite <- powerRZ_add; auto with real zarith.

614

replace (pred prec + Fexp c)%Z with (prec + (Fexp c + -1))%Z; auto.

615

rewrite inj_pred; unfold Zpred; auto with zarith.

616

assert (-dExp b < Fexp c)%Z; auto with zarith.

617

apply GepetaGeExp; auto.

618

Qed.

619

620

621

622

Lemma predNormal2: forall (c:float),

623

Fcanonic radix b c ->

624

(powerRZ radix (prec-dExp b) <= c)%R ->

625

(Fnum c <> nNormMin radix prec) ->

626

(FtoRradix (FPred b radix prec c) = c-powerRZ radix (Fexp c))%R.

627

intros.

628

rewrite FPredSimpl4; auto with zarith.

629

unfold FtoRradix, FtoR, Zpred; simpl.

630

rewrite plus_IZR; simpl; ring.

631

assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.

632

apply Zlt_le_trans with 0%Z.

633

assert (0 < pPred (vNum b))%Z; auto with zarith float.

634

apply pPredMoreThanOne with radix prec; auto with zarith.

635

apply LeR0Fnum with radix ; auto with real zarith.

636

fold FtoRradix; apply Rle_trans with (2:=H0); auto with real zarith.

637

Qed.

638

639

Lemma succNormal: forall (c:float),

640

Fcanonic radix b c ->

641

(0 <= c)%R ->

642

(FtoRradix (FSucc b radix prec c) = c+powerRZ radix (Fexp c))%R.

643

intros.

644

apply Rplus_eq_reg_l with (-c)%R.

645

apply trans_eq with (FtoRradix (Fminus radix (FSucc b radix prec c) c)).

646

unfold FtoRradix; rewrite Fminus_correct; auto with real zarith; ring.

647

unfold FtoRradix; rewrite FSuccDiff1; auto with zarith.

648

unfold FtoR; simpl; ring.

649

unfold nNormMin.

650

assert (-(Zpower_nat radix (pred prec)) < Fnum c)%Z; auto with zarith.

651

apply Zlt_le_trans with (-0)%Z; auto with zarith.

652

simpl; apply LeR0Fnum with radix; auto with real zarith.

653

Qed.

654

655

656

Lemma eGe: forall (c c' e:float),

657

Fcanonic radix b c ->

658

(0 <= c)%R ->

659

Closest b radix (phi*c) c' ->

660

Closest b radix (c'+eta) e ->

661

(powerRZ radix (Fexp c)/2 < e)%R.

662

intros.

663

case (Zle_or_lt (-dExp b) (Fexp c -prec)); intros.

664

assert (powerRZ radix (prec - dExp b) <= c)%R.

665

unfold FtoRradix, FtoR; simpl.

666

apply Rle_trans with (1*powerRZ radix (prec - dExp b))%R; auto with real.

667

apply Rmult_le_compat; auto with real zarith.

668

apply Rle_trans with (IZR 1); auto with real zarith.

669

apply Rle_IZR.

670

apply Zle_trans with (nNormMin radix prec); auto with zarith float.

671

assert (0 < nNormMin radix prec)%Z; auto with zarith.

672

apply nNormPos; auto with zarith.

673

rewrite <- (Zabs_eq (Fnum c)).

674

apply pNormal_absolu_min with b; auto with zarith real.

675

case H; auto; intros M.

676

elim M; intros M1 (M2,M3).

677

absurd (- dExp b <= Fexp c - prec)%Z; auto.

678

rewrite M2; auto with zarith.

679

apply LeR0Fnum with radix; auto with real zarith.

680

apply Rle_powerRZ; auto with real zarith.

681

apply Rlt_le_trans with c'.

682

apply Rlt_le_trans with (Float (radixH*nNormMin radix prec + 1)

683

(Fexp c -prec)).

684

unfold FtoRradix, FtoR; simpl.

685

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

686

apply Rlt_le_trans with (powerRZ radix (Fexp c) *

687

((radixH*nNormMin radix prec + 1)%Z* powerRZ radix (- prec)))%R;[idtac|right; ring].

688

unfold Rdiv; apply Rmult_lt_compat_l; auto with real zarith.

689

rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

690

rewrite Rmult_plus_distr_r.

691

replace (radixH*powerRZ radix (pred prec) * powerRZ radix (- prec))%R with (/2)%R.

692

apply Rle_lt_trans with (/2+0)%R; auto with real zarith.

693

apply Rplus_lt_compat_l; simpl.

694

apply Rlt_le_trans with (powerRZ radix (- prec)); auto with real zarith.

695

rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.

696

replace (pred prec + - prec)%Z with (-1)%Z.

697

simpl; rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real zarith.

698

rewrite inj_pred; unfold Zpred; auto with zarith.

699

unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.

700

apply ClosestRoundedModeP with prec; auto with zarith.

701

split; simpl; auto with zarith.

702

apply phi_bounded_aux.

703

unfold FtoRradix, FtoR; simpl.

704

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

705

apply Rle_trans with (powerRZ radix (- prec)*

706

((radixH*nNormMin radix prec + 1)%Z*powerRZ radix (Fexp c)))%R;[right; ring|idtac].

707

unfold phi.

708

apply Rle_trans with (powerRZ radix (-prec)*

709

(((radixH + radix * u)*Fnum c)*powerRZ radix (Fexp c)))%R;[idtac|unfold phi,u; simpl; right;ring].

710

apply Rmult_le_compat_l; auto with real zarith.

711

apply Rmult_le_compat_r; auto with real zarith.

712

apply Rle_trans with ((radixH + radix * u) * nNormMin radix prec)%R.

713

rewrite plus_IZR; rewrite mult_IZR; rewrite Rmult_plus_distr_r.

714

apply Rplus_le_compat; auto with real.

715

unfold u; simpl; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

716

pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1).

717

repeat rewrite <- powerRZ_add; auto with real zarith.

718

replace (1 + - prec + pred prec)%Z with 0%Z.

719

simpl; auto with real.

720

rewrite inj_pred; unfold Zpred; auto with zarith.

721

simpl; auto with real.

722

apply Rmult_le_compat_l.

723

unfold u; apply Rle_trans with (0+0)%R; auto with real; apply Rplus_le_compat; auto with real zarith.

724

apply Rmult_le_pos; auto with real zarith.

725

rewrite <- (Zabs_eq (Fnum c)).

726

apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.

727

apply GepetaIsNormal; auto.

728

apply LeR0Fnum with radix; auto with real zarith.

729

unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

730

apply ClosestRoundedModeP with prec; auto with zarith.

731

elim H1; auto.

732

fold FtoRradix; apply Rle_trans with (c'+0)%R; auto with real zarith.

733

unfold eta; apply Rplus_le_compat_l; auto with real zarith.

734

assert (powerRZ radix (Fexp c) / 2 = (Float radixH (Fexp c -1)))%R.

735

unfold FtoRradix, FtoR; simpl.

736

unfold Zminus; rewrite powerRZ_add; auto with real zarith; simpl.

737

rewrite radixEven; rewrite mult_IZR; simpl.

738

field; auto with real zarith.

739

case (Zle_lt_or_eq (-dExp b) (Fexp c)).

740

assert (Fbounded b c); auto with zarith float.

741

apply FcanonicBound with radix; auto with zarith.

742

intros.

743

assert (powerRZ radix (Fexp c) / 2 <= c')%R.

744

rewrite H4.

745

unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.

746

apply ClosestRoundedModeP with prec; auto with zarith.

747

split; simpl; auto with zarith.

748

rewrite Zabs_eq; auto with zarith.

749

rewrite pGivesBound.

750

apply Zlt_le_trans with (Zpower_nat radix 1); auto with zarith.

751

unfold Zpower_nat; simpl; rewrite radixEven; auto with zarith.

752

unfold phi.

753

apply Rle_trans with (u*radixH*c)%R.

754

unfold FtoRradix, FtoR,u; simpl.

755

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

756

apply Rle_trans with (radixH*(powerRZ radix (Fexp c) *

757

(powerRZ radix (- prec) *Fnum c)))%R;[idtac|right; ring].

758

repeat apply Rmult_le_compat_l; auto with real zarith.

759

apply Rle_trans with (powerRZ radix (- prec) * nNormMin radix prec)%R.

760

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

761

rewrite <- powerRZ_add; auto with real zarith; apply Rle_powerRZ; auto with real zarith.

762

rewrite inj_pred; unfold Zpred; auto with zarith.

763

apply Rmult_le_compat_l; auto with real zarith.

764

rewrite <- (Zabs_eq (Fnum c)).

765

apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.

766

case H; auto; intros M.

767

elim M; intros M1 (M2,M3).

768

Contradict M2; auto with zarith.

769

apply LeR0Fnum with radix; auto with real zarith.

770

apply Rle_trans with (u*(radixH+0*0)*c)%R;[right; ring|idtac].

771

apply Rmult_le_compat_r; auto.

772

apply Rmult_le_compat_l; unfold u; auto with real zarith.

773

apply Rle_lt_trans with (1:=H6).

774

replace (FtoRradix e) with (c'+eta)%R.

775

unfold eta; apply Rle_lt_trans with (c'+0)%R; auto with real zarith.

776

replace eta with (FtoRradix (Float 1 (-dExp b))).

777

2: unfold eta, FtoRradix, FtoR; simpl; ring.

778

unfold FtoRradix; rewrite <- Fplus_correct; auto with zarith.

779

apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

780

apply ClosestRoundedModeP with prec; auto with zarith.

781

2: rewrite Fplus_correct; auto with zarith real.

782

2: replace (FtoR radix (Float 1 (-dExp b))) with eta; auto with real.

783

2: unfold eta, FtoRradix, FtoR; simpl; ring.

784

unfold Fplus.

785

simpl (Fexp (Float 1 (- dExp b))); simpl (Fnum (Float 1 (- dExp b))).

786

rewrite Zmin_le2.

787

replace (1 * Zpower_nat radix (Zabs_nat (- dExp b - - dExp b)))%Z with 1%Z.

788

split; simpl; auto with zarith.

789

apply Zlt_Rlt.

790

rewrite <- Rabs_Zabs; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.

791

rewrite plus_IZR.

792

apply Rle_lt_trans with (Rabs ((Fnum c' * Zpower_nat radix (Zabs_nat (Fexp c' - - dExp b)))%Z) + Rabs 1%Z)%R.

793

apply Rabs_triang.

794

rewrite mult_IZR; rewrite Zpower_nat_Z_powerRZ.

795

replace (Rabs (IZR 1)) with 1%R.

796

apply Rplus_lt_reg_r with (-1)%R.

797

apply Rle_lt_trans with (Rabs (Fnum c' * powerRZ radix (Zabs_nat (Fexp c' - - dExp b))));[right; ring|idtac].

798

apply Rmult_lt_reg_l with (powerRZ radix (-dExp b)); auto with real zarith.

799

apply Rle_lt_trans with (Rabs c').

800

unfold FtoRradix, FtoR; simpl; repeat rewrite Rabs_mult.

801

rewrite (Rabs_right (powerRZ radix (Zabs_nat (Fexp c' - - dExp b)))).

802

rewrite (Rabs_right (powerRZ radix (Fexp c'))).

803

right;apply trans_eq with (Rabs (Fnum c') * (

804

powerRZ radix (- dExp b) *powerRZ radix (Zabs_nat (Fexp c' - - dExp b))))%R;[ring|idtac].

805

rewrite <- powerRZ_add; auto with real zarith.

806

replace (- dExp b + Zabs_nat (Fexp c' - - dExp b))%Z with (Fexp c')%Z; auto.

807

rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.

808

assert (-dExp b <= Fexp c')%Z; auto with zarith float.

809

elim H1; auto with zarith float.

810

apply Rle_ge; auto with real zarith.

811

apply Rle_ge; auto with real zarith.

812

assert (FtoRradix (Float (radixH*nNormMin radix prec+1) (-dExp b)) =

813

radixH*powerRZ radix (prec-1-dExp b) + powerRZ radix (-dExp b))%R.

814

unfold FtoRradix, FtoR; simpl.

815

rewrite plus_IZR; rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

816

rewrite inj_pred; auto with zarith.

817

apply trans_eq with (radixH*(powerRZ radix (Zpred prec)*powerRZ radix (- dExp b)) + powerRZ radix (- dExp b))%R.

818

simpl; ring.

819

rewrite <- powerRZ_add; auto with zarith real.

820

apply Rle_lt_trans with (Float (radixH*nNormMin radix prec+1) (-dExp b)).

821

unfold FtoRradix; apply RoundAbsMonotoner with b prec (Closest b radix) (phi*c)%R; auto with zarith.

822

apply ClosestRoundedModeP with prec; auto with zarith.

823

split; simpl; auto with zarith.

824

apply phi_bounded_aux.

825

fold FtoRradix; rewrite H7.

826

rewrite Rabs_mult; repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

827

2: left; apply phi_Pos.

828

unfold phi.

829

apply Rle_trans with ((radixH+radix*u)*powerRZ radix (Fexp c))%R.

830

apply Rle_trans with ((radixH + radix * u) *(u*c))%R;[right; ring|idtac].

831

apply Rmult_le_compat_l.

832

apply Rle_trans with (0+0*0)%R; [right; ring|apply Rplus_le_compat; auto with real zarith].

833

apply Rmult_le_compat; unfold u; auto with real zarith.

834

unfold FtoRradix, FtoR, u; simpl.

835

apply Rle_trans with (powerRZ radix (- prec) * (powerRZ radix prec * powerRZ radix (Fexp c)))%R.

836

apply Rmult_le_compat_l; auto with real zarith.

837

apply Rmult_le_compat_r; auto with real zarith.

838

rewrite <- Zpower_nat_Z_powerRZ; rewrite <- pGivesBound.

839

apply Rle_IZR.

840

apply Zle_trans with (Zabs (Fnum c)); auto with zarith float.

841

assert (Fbounded b c); [apply FcanonicBound with radix|idtac]; auto with zarith float.

842

repeat rewrite <- powerRZ_add; auto with real zarith.

843

replace ((- prec + (prec + Fexp c)))%Z with (Fexp c); auto with real; ring.

844

apply Rle_trans with ((radixH + radix * u) * powerRZ radix (prec-1-dExp b))%R.

845

apply Rmult_le_compat_l.

846

apply Rle_trans with (0+0*0)%R; [right; ring|unfold u; apply Rplus_le_compat; auto with real zarith].

847

apply Rle_powerRZ; auto with real zarith.

848

rewrite Rmult_plus_distr_r.

849

apply Rplus_le_compat; auto with real.

850

pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1);[idtac|simpl; auto with real].

851

unfold u; repeat rewrite <- powerRZ_add; auto with real zarith.

852

apply Rle_powerRZ; auto with real zarith.

853

rewrite H7.

854

apply Rle_lt_trans with (powerRZ radix (- dExp b) *(powerRZ radix prec / 2+1))%R.

855

rewrite Rmult_plus_distr_l; apply Rplus_le_compat; auto with real.

856

unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith; simpl.

857

replace (IZR radixH) with (radix/2)%R.

858

right; field; auto with real zarith.

859

rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real.

860

apply Rmult_lt_compat_l; auto with real zarith.

861

apply Rplus_lt_reg_r with (1-powerRZ radix prec / 2)%R.

862

apply Rmult_lt_reg_l with 2%R; auto with real.

863

apply Rle_lt_trans with (IZR 2*IZR 2)%R;[simpl; right; ring|idtac].

864

apply Rlt_le_trans with (powerRZ radix prec)%R;[idtac|right; field; auto with real].

865

apply Rle_lt_trans with (powerRZ radix 2); auto with real zarith.

866

apply Rle_trans with (radix*radix)%R;[idtac|simpl; right; ring].

867

apply Rmult_le_compat; auto with real zarith.

868

rewrite Rabs_right; try apply Rle_ge; auto with real.

869

replace (- dExp b - - dExp b)%Z with 0%Z; auto with zarith.

870

elim H1; auto with zarith float.

871

intros.

872

apply Rlt_le_trans with (Float 1 (-(dExp b))).

873

unfold FtoRradix, FtoR; simpl.

874

unfold Rdiv; rewrite Rmult_comm; rewrite H5.

875

apply Rmult_lt_compat_r; auto with real zarith.

876

apply Rlt_le_trans with (/1)%R; auto with real.

877

unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

878

apply ClosestRoundedModeP with prec; auto with zarith.

879

split; simpl; auto with zarith float.

880

apply vNumbMoreThanOne with radix prec; auto with zarith.

881

apply Rle_trans with (0+eta)%R.

882

right; unfold eta, FtoR; simpl; ring.

883

apply Rplus_le_compat_r.

884

unfold FtoRradix; apply RleRoundedR0 with b prec (Closest b radix) (phi*c)%R; auto with zarith real float.

885

apply ClosestRoundedModeP with prec; auto with zarith.

886

apply Rmult_le_pos; auto.

887

left; apply phi_Pos.

888

Qed.

889

890

891

Lemma Algo1_correct_aux_aux:forall (c cinf:float) (r:R),

892

Fcanonic radix b c -> (0 <= c)%R ->

893

(powerRZ radix (Fexp c)/2 < r)%R ->

894

Closest b radix (c-r) cinf ->

895

(FtoRradix cinf <= FPred b radix prec c)%R.

896

intros.

897

assert (N:Fbounded b c).

898

apply FcanonicBound with radix; auto.

899

generalize ClosestMonotone; unfold MonotoneP; intros.

900

cut (exists f:float, Fbounded b f /\ (FtoRradix f <= FPred b radix prec c)%R /\

901

Closest b radix (c-powerRZ radix (Fexp c) / 2)%R f).

902

intros (f,(L1,(L2,L3))).

903

apply Rle_trans with (2:=L2).

904

unfold FtoRradix; apply H3 with b (c-r)%R (c-powerRZ radix (Fexp c) / 2)%R; auto; clear H3.

905

unfold Rminus; apply Rplus_lt_compat_l; auto with real.

906

case (Rle_or_lt (powerRZ radix (prec - dExp b)) c); intros.

907

case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros.

908

cut (exists f:float, Fbounded b f /\

909

(FtoRradix f = (c-powerRZ radix (Fexp c) / 2))%R).

910

intros (f,(L1,L2)).

911

exists f; split; auto; split.

912

rewrite L2; rewrite predNormal1; auto with real zarith.

913

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

914

unfold Rminus, Rdiv; apply Rplus_le_compat_l.

915

apply Ropp_le_contravar.

916

apply Rmult_le_compat_l; auto with real zarith.

917

simpl; apply Rle_Rinv; auto with real zarith.

918

replace (radix*1)%R with (IZR radix); auto with real; replace 2%R with (IZR 2); auto with real zarith.

919

rewrite <- L2; unfold FtoRradix.

920

apply RoundedModeProjectorIdem with b; auto with zarith.

921

apply ClosestRoundedModeP with prec; auto with zarith.

922

exists (Float (Zpos (vNum b) -radixH) (Fexp c-1)).

923

split; try split.

924

apply Zle_lt_trans with (Zabs (Zpos (vNum b) - radixH)); auto with zarith.

925

rewrite Zabs_eq; auto with zarith.

926

apply Zplus_le_reg_l with (radixH).

927

ring_simplify.

928

rewrite pGivesBound; apply Zle_trans with (Zpower_nat radix 1); auto with zarith.

929

unfold Zpower_nat;simpl.

930

ring_simplify; rewrite radixEven; auto with zarith.

931

simpl.

932

assert (- dExp b < Fexp c)%Z; auto with zarith.

933

apply GepetaGeExp; auto.

934

unfold FtoRradix, FtoR.

935

replace (Fnum (Float (Zpos (vNum b) - radixH) (Fexp c - 1)))

936

with (Zpos (vNum b) - radixH)%Z; auto.

937

simpl (Fexp (Float (Zpos (vNum b) - radixH) (Fexp c - 1))).

938

unfold Zminus; rewrite plus_IZR.

939

rewrite Ropp_Ropp_IZR.

940

rewrite pGivesBound; rewrite e; unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.

941

rewrite inj_pred; auto with zarith; unfold Zpred.

942

repeat rewrite powerRZ_add; auto with real zarith; simpl.

943

replace (radix*1)%R with (2*radixH)%R.

944

field; auto with real zarith.

945

rewrite radixEven; rewrite mult_IZR; simpl; ring.

946

exists (FPred b radix prec c); split.

947

apply FBoundedPred; auto with zarith.

948

split; auto with real.

949

apply ClosestSuccPred with prec; auto with zarith.

950

apply FBoundedPred; auto with zarith.

951

apply FPredCanonic; auto with zarith.

952

rewrite FSucPred; fold FtoRradix; auto with zarith.

953

replace (c - powerRZ radix (Fexp c) / 2 - c)%R with (-(powerRZ radix (Fexp c)/2))%R;[idtac|ring].

954

rewrite Rabs_Ropp; rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).

955

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

956

rewrite predNormal2; auto.

957

replace (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with

958

(powerRZ radix (Fexp c) / 2)%R.

959

rewrite Rabs_right; auto with real.

960

apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

961

field; auto with real.

962

rewrite predNormal2; auto with zarith real.

963

replace (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with

964

(powerRZ radix (Fexp c) / 2)%R.

965

rewrite Rabs_right; auto with real.

966

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

967

2: field; auto with real.

968

case (Zle_lt_or_eq (nNormMin radix prec +1) (Fnum c)).

969

assert (nNormMin radix prec <= Fnum c)%Z; auto with zarith.

970

rewrite <- (Zabs_eq (Fnum c)).

971

apply pNormal_absolu_min with b; auto with zarith real.

972

apply GepetaIsNormal; auto.

973

apply LeR0Fnum with radix; auto with real zarith.

974

intros.

975

rewrite predNormal2; auto with zarith real.

976

rewrite FPredSimpl4; auto with zarith.

977

simpl; unfold FtoRradix, FtoR, Zpred; simpl.

978

rewrite plus_IZR.

979

replace (Fnum c * powerRZ radix (Fexp c) - powerRZ radix (Fexp c) / 2 -

980

((Fnum c + (-1)%Z) * powerRZ radix (Fexp c) - powerRZ radix (Fexp c)))%R with

981

((3*powerRZ radix (Fexp c)/2))%R.

982

rewrite Rabs_right.

983

apply Rle_trans with (1*powerRZ radix (Fexp c) / 2)%R;auto with real.

984

right; unfold Rdiv; ring.

985

unfold Rdiv; apply Rmult_le_compat_r; auto with real.

986

apply Rmult_le_compat_r; auto with real zarith.

987

apply Rle_trans with 2%R; auto with real.

988

unfold Rdiv; apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.

989

apply Rle_trans with (IZR 3); auto with real zarith.

990

right; simpl; ring.

991

simpl; field.

992

assert (- pPred (vNum b) < Fnum c)%Z; auto with zarith.

993

apply Zle_lt_trans with (2:=H5).

994

apply Zle_trans with 0%Z; auto with zarith.

995

assert (0 < pPred (vNum b))%Z; auto with zarith.

996

apply pPredMoreThanOne with radix prec; auto with zarith.

997

unfold nNormMin; auto with zarith.

998

apply FPredCanonic; auto with zarith float.

999

case H4; intros.

1000

assert (FtoRradix (Float 1 (prec-dExp b))=powerRZ radix (prec - dExp b))%R.

1001

unfold FtoRradix, FtoR; simpl; ring.

1002

rewrite <- H7.

1003

unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec (Float 1 (prec-dExp b)); auto.

1004

apply FPredProp; auto with zarith.

1005

apply FnormalizeCanonic; auto with zarith.

1006

split; simpl; auto with zarith float.

1007

apply vNumbMoreThanOne with radix prec; auto with zarith.

1008

rewrite FnormalizeCorrect; auto with zarith.

1009

fold FtoRradix; rewrite H7; auto.

1010

assert (c=Float (nNormMin radix prec) (-dExp b+1)).

1011

apply FcanonicUnique with radix b prec; auto with zarith real.

1012

left; split; try split; simpl; auto with zarith float.

1013

rewrite Zabs_eq.

1014

apply ZltNormMinVnum; auto with zarith.

1015

unfold nNormMin; auto with zarith.

1016

rewrite <- PosNormMin with radix b prec; auto with zarith.

1017

fold FtoRradix; rewrite <- H6; unfold FtoRradix, FtoR; simpl.

1018

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1019

rewrite <- powerRZ_add; auto with real zarith.

1020

replace (pred prec + (- dExp b + 1))%Z with (prec-dExp b)%Z; auto.

1021

rewrite inj_pred; auto with zarith.

1022

unfold Zpred; ring.

1023

absurd (Fnum c = nNormMin radix prec)%Z; auto with zarith.

1024

rewrite H7; simpl; auto.

1025

assert ((nNormMin radix prec < Fnum (FPred b radix prec c)))%Z; auto with zarith.

1026

rewrite FPredSimpl4; auto with zarith.

1027

simpl; unfold Zpred; auto with zarith.

1028

assert (0 < pPred (vNum b))%Z.

1029

apply pPredMoreThanOne with radix prec; auto with zarith.

1030

assert (0 < Fnum c)%Z; auto with zarith.

1031

apply Zle_lt_trans with (2:=H5).

1032

unfold nNormMin; auto with zarith.

1033

intros.

1034

rewrite FPredSimpl4 with (x:=c); auto with zarith.

1035

rewrite FPredSimpl2; auto with zarith.

1036

simpl.

1037

replace (c - powerRZ radix (Fexp c) / 2 -

1038

FtoR radix (Float (pPred (vNum b)) (Zpred (Fexp c))))%R with

1039

(powerRZ radix (Fexp c)* (/2 +/radix))%R.

1040

rewrite Rabs_right; unfold Rdiv.

1041

apply Rmult_le_compat_l; auto with real zarith.

1042

apply Rle_trans with (/2+0)%R; auto with real zarith.

1043

apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

1044

apply Rle_trans with (0+0)%R; auto with real zarith.

1045

apply Rplus_le_compat; auto with real zarith.

1046

unfold FtoRradix, FtoR; simpl.

1047

rewrite <- H5; unfold pPred, Zpred; repeat rewrite plus_IZR; rewrite pGivesBound; simpl.

1048

unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.

1049

rewrite inj_pred; auto with zarith; unfold Zpred.

1050

repeat rewrite powerRZ_add; auto with real zarith; simpl.

1051

field; auto with real zarith.

1052

rewrite <- H5; simpl; unfold Zpred; auto with zarith.

1053

assert (-dExp b < Fexp c)%Z; auto with zarith.

1054

apply GepetaGeExp; auto.

1055

assert (0 < pPred (vNum b))%Z.

1056

apply pPredMoreThanOne with radix prec; auto with zarith.

1057

assert (0 < Fnum c)%Z; auto with zarith.

1058

rewrite <- H5; unfold nNormMin; auto with zarith.

1059

apply Zlt_le_trans with (0+1)%Z; auto with zarith.

1060

case (Zle_lt_or_eq (-dExp b) (Fexp c)); auto.

1061

assert (Fbounded b c); auto with zarith float.

1062

intros; absurd (c < powerRZ radix (prec - dExp b))%R; auto.

1063

apply Rle_not_lt.

1064

unfold FtoRradix, FtoR; simpl.

1065

replace (prec-dExp b)%Z with ((prec-1)+(-dExp b+1))%Z;[idtac| ring].

1066

rewrite powerRZ_add; auto with real zarith.

1067

apply Rmult_le_compat; auto with real zarith.

1068

apply Rle_trans with (nNormMin radix prec).

1069

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1070

apply Rle_powerRZ; auto with real zarith.

1071

rewrite inj_pred; auto with zarith.

1072

rewrite <- (Zabs_eq (Fnum c)).

1073

apply Rle_IZR; apply pNormal_absolu_min with b; auto with zarith real.

1074

case H; auto.

1075

intros L; elim L; intros L1 (L2,L3).

1076

Contradict L2; auto with zarith.

1077

apply LeR0Fnum with radix; auto with real zarith.

1078

apply Rle_powerRZ; auto with zarith real.

1079

intros.

1080

exists (FPred b radix prec c); split.

1081

apply FBoundedPred; auto with zarith.

1082

split; auto with real.

1083

apply ClosestSuccPred with prec; auto with zarith.

1084

apply FBoundedPred; auto with zarith.

1085

apply FPredCanonic; auto with zarith.

1086

rewrite FSucPred; fold FtoRradix; auto with zarith.

1087

replace (c - powerRZ radix (Fexp c) / 2 - c)%R with (-(powerRZ radix (Fexp c)/2))%R;[idtac|ring].

1088

rewrite Rabs_Ropp; rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).

1089

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1090

rewrite predSmallOnes; auto.

1091

unfold eta; replace (-dExp b)%Z with (Fexp c).

1092

replace (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R with

1093

(powerRZ radix (Fexp c) / 2)%R.

1094

rewrite Rabs_right; auto with real.

1095

apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1096

field; auto with real.

1097

rewrite Rabs_right; try apply Rle_ge; auto with real.

1098

repeat rewrite predSmallOnes; auto.

1099

unfold eta; rewrite H5.

1100

replace (c - powerRZ radix (Fexp c) / 2 - (c - powerRZ radix (Fexp c)))%R

1101

with (powerRZ radix (Fexp c) */ 2)%R;[idtac|field].

1102

replace (c - powerRZ radix (Fexp c) / 2 -

1103

(c - powerRZ radix (Fexp c) - powerRZ radix (Fexp c)))%R with

1104

((3*powerRZ radix (Fexp c) */ 2))%R;[idtac|field].

1105

repeat rewrite Rabs_right; try apply Rle_ge.

1106

apply Rmult_le_compat_r; auto with real zarith.

1107

apply Rle_trans with (1*powerRZ radix (Fexp c))%R; auto with real.

1108

apply Rmult_le_compat_r; auto with real zarith.

1109

apply Rle_trans with (IZR 3); auto with real zarith.

1110

simpl; right; ring.

1111

repeat apply Rmult_le_pos; auto with real zarith.

1112

apply Rle_trans with (IZR 3); auto with real zarith.

1113

simpl; right; ring.

1114

apply Rmult_le_pos; auto with real zarith.

1115

rewrite Rabs_right; try apply Rle_ge; auto with real.

1116

apply FPredCanonic; auto with zarith.

1117

case (Rle_or_lt 0 (c-eta)); intros.

1118

rewrite Rabs_right;[idtac|apply Rle_ge; auto with real].

1119

apply Rle_lt_trans with (FtoRradix c); auto with real.

1120

apply Rle_trans with (c-0)%R; auto with real.

1121

unfold Rminus, eta; auto with real zarith.

1122

rewrite Rabs_left; auto.

1123

apply Rle_lt_trans with eta.

1124

apply Rle_trans with (eta-c)%R;[right; ring|idtac].

1125

apply Rle_trans with (eta-0)%R;[auto with real|right; ring].

1126

unfold Rminus; apply Rplus_le_compat_l; auto with real.

1127

unfold eta; apply Rlt_powerRZ; auto with zarith real.

1128

rewrite Rabs_right; try apply Rle_ge; auto with real.

1129

rewrite Rabs_right; try apply Rle_ge; auto with real.

1130

Qed.

1131

1132

Lemma Algo1_correct_aux_aux2:forall (c csup:float) (r:R),

1133

Fcanonic radix b c -> (0 <= c)%R ->

1134

(powerRZ radix (Fexp c)/2 < r)%R ->

1135

Closest b radix (c+r) csup ->

1136

(FtoRradix (FSucc b radix prec c) <= csup)%R.

1137

intros.

1138

assert (N:Fbounded b c).

1139

apply FcanonicBound with radix; auto.

1140

generalize ClosestMonotone; unfold MonotoneP; intros.

1141

cut (exists f:float, Fbounded b f /\ (FtoRradix (FSucc b radix prec c) <= f)%R /\

1142

Closest b radix (c+powerRZ radix (Fexp c) / 2)%R f).

1143

intros (f,(L1,(L2,L3))).

1144

apply Rle_trans with (1:=L2).

1145

unfold FtoRradix; apply H3 with b (c+powerRZ radix (Fexp c) / 2)%R (c+r)%R; auto; clear H3.

1146

unfold Rminus; apply Rplus_lt_compat_l; auto with real.

1147

exists (FSucc b radix prec c); split.

1148

apply FBoundedSuc; auto with zarith.

1149

split; auto with real.

1150

apply ClosestSuccPred with prec; auto with zarith.

1151

apply FBoundedSuc; auto with zarith.

1152

apply FSuccCanonic; auto with zarith.

1153

rewrite succNormal; auto with zarith.

1154

replace (c + powerRZ radix (Fexp c) / 2 -

1155

(c + powerRZ radix (Fexp c)))%R with

1156

(-(powerRZ radix (Fexp c)/2))%R.

1157

2: field.

1158

rewrite Rabs_Ropp; rewrite Rabs_right.

1159

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1160

rewrite succNormal; auto with zarith.

1161

rewrite succNormal; auto with zarith.

1162

replace (c + powerRZ radix (Fexp c) / 2 -

1163

(c + powerRZ radix (Fexp c) +

1164

powerRZ radix (Fexp (FSucc b radix prec c))))%R with

1165

(-(powerRZ radix (Fexp c)/2+powerRZ radix

1166

(Fexp (FSucc b radix prec c))))%R.

1167

2: field.

1168

rewrite Rabs_Ropp; rewrite Rabs_right.

1169

apply Rle_trans with (powerRZ radix (Fexp c) / 2+0)%R; auto with real zarith.

1170

apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.

1171

apply Rplus_le_compat; auto with real zarith.

1172

unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1173

apply FSuccCanonic; auto with zarith.

1174

apply Rle_trans with (1:=H0).

1175

left; unfold FtoRradix; apply FSuccLt; auto with zarith.

1176

rewrite FPredSuc; fold FtoRradix; auto with zarith.

1177

replace (c + powerRZ radix (Fexp c) / 2 - c)%R with ((powerRZ radix (Fexp c)/2))%R;[idtac|ring].

1178

rewrite (Rabs_right (powerRZ radix (Fexp c) / 2)).

1179

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1180

rewrite succNormal; auto.

1181

replace (c + powerRZ radix (Fexp c) / 2 - (c + powerRZ radix (Fexp c)))%R with

1182

(-(powerRZ radix (Fexp c) / 2))%R.

1183

rewrite Rabs_Ropp; rewrite Rabs_right; auto with real.

1184

apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

1185

field; auto with real.

1186

Qed.

1187

1188

1189

1190

Lemma Algo1_correct_aux: forall (c c' e cinf csup:float),

1191

Fcanonic radix b c ->

1192

(0 <= c)%R ->

1193

Closest b radix (phi*c) c' ->

1194

Closest b radix (c'+eta) e ->

1195

Closest b radix (c-e) cinf ->

1196

Closest b radix (c+e) csup ->

1197

(FtoRradix cinf <= FPred b radix prec c)%R

1198

/\ (FtoRradix (FSucc b radix prec c) <= csup)%R .

1199

intros c c' e cinf csup Cc Cpos Hc' He Hcinf Hcsup.

1200

assert (powerRZ radix (Fexp c)/2 < e)%R.

1201

apply eGe with c'; auto.

1202

split.

1203

apply Algo1_correct_aux_aux with e; auto.

1204

apply Algo1_correct_aux_aux2 with e; auto.

1205

Qed.

1206

1207

Lemma PredSucc_Algo1_correct: forall (c c' e cinf csup:float),

1208

Fcanonic radix b c ->

1209

Closest b radix (phi*(Rabs c)) c' ->

1210

Closest b radix (c'+eta) e ->

1211

Closest b radix (c-e) cinf ->

1212

Closest b radix (c+e) csup ->

1213

(FtoRradix cinf <= FPred b radix prec c)%R

1214

/\ (FtoRradix (FSucc b radix prec c) <= csup)%R .

1215

intros c c' e cinf csup Cc Hc' He Hcinf Hcsup.

1216

case (Rle_or_lt 0 c); intros.

1217

apply Algo1_correct_aux with c' e; auto.

1218

rewrite <- (Rabs_right c); auto.

1219

apply Rle_ge; auto.

1220

assert ((Fopp csup <= FPred b radix prec (Fopp c))%R

1221

/\ (FSucc b radix prec (Fopp c) <= (Fopp cinf))%R).

1222

apply Algo1_correct_aux with c' e; auto.

1223

apply FcanonicFopp; auto.

1224

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1225

replace (FtoRradix (Fopp c)) with (Rabs c); auto.

1226

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1227

rewrite Rabs_left; auto with real.

1228

replace (Fopp c -e)%R with (-(c+e))%R.

1229

apply ClosestOpp; auto.

1230

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

1231

replace (Fopp c +e)%R with (-(c-e))%R.

1232

apply ClosestOpp; auto.

1233

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

1234

elim H0; intros L1 L2; clear H0; split; apply Ropp_le_cancel.

1235

rewrite FPredFopFSucc; auto with zarith.

1236

apply Rle_trans with (FSucc b radix prec (Fopp c)).

1237

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1238

apply Rle_trans with (1:=L2).

1239

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1240

apply Rle_trans with (Fopp csup).

1241

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1242

apply Rle_trans with (1:=L1).

1243

rewrite FPredFopFSucc; auto with zarith.

1244

rewrite Fopp_Fopp.

1245

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

1246

Qed.

1247

1248

Hypothesis precisionGreaterThanbis : 4 <= prec.

1249

1250

Lemma eLe: forall (c c' e:float),

1251

Fcanonic radix b c ->

1252

(0 <= c)%R ->

1253

Closest b radix (phi*c) c' ->

1254

Closest b radix (c'+eta) e ->

1255

(-dExp b <= Fexp c-2)%Z ->

1256

(e <= powerRZ radix (Fexp c)*(radix/2+powerRZ radix (-2)))%R.

1257

intros c c' e H H0 H1 H2 V.

1258

assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].

1259

assert (powerRZ radix (Fexp c) * radix / 2=Float radixH (Fexp c))%R.

1260

unfold FtoRradix, FtoR; simpl.

1261

pattern radix at 2; rewrite radixEven; rewrite mult_IZR; simpl; field.

1262

assert (Fbounded b (Float radixH (Fexp c))).

1263

split; simpl.

1264

rewrite Zabs_eq; auto with zarith.

1265

rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.

1266

apply Zle_trans with radix;[rewrite radixEven| unfold Zpower_nat; simpl]; auto with zarith.

1267

elim Bc; auto.

1268

assert (powerRZ radix (Fexp c) * radix / 2=

1269

Float (radixH*nNormMin radix prec) (Fexp c -prec+1))%R.

1270

unfold FtoRradix, FtoR; simpl.

1271

rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1272

rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.

1273

replace (pred prec + (Fexp c - prec + 1))%Z with (Fexp c).

1274

rewrite radixEven; rewrite mult_IZR; simpl; field.

1275

rewrite inj_pred; auto with zarith.

1276

unfold Zpred; ring.

1277

assert ( (-dExp b <= Fexp c -prec+1)%Z

1278

-> (Fnormal radix b (Float (radixH*nNormMin radix prec)

1279

(Fexp c -prec+1)))).

1280

intros I; split; try split; simpl; auto with zarith.

1281

rewrite Zabs_eq.

1282

unfold nNormMin; rewrite pGivesBound.

1283

apply Zlt_le_trans with (radix*Zpower_nat radix (pred prec))%Z; auto with zarith.

1284

apply Zmult_gt_0_lt_compat_r; auto with zarith.

1285

apply Zlt_gt; auto with zarith.

1286

pattern radix at 1; replace radix with (Zpower_nat radix 1).

1287

rewrite <- Zpower_nat_is_exp; auto with zarith.

1288

unfold Zpower_nat; simpl; auto with zarith.

1289

unfold nNormMin; auto with zarith.

1290

rewrite Zabs_eq.

1291

replace (radix * (radixH * nNormMin radix prec))%Z with

1292

(radixH * (radix * nNormMin radix prec))%Z;[idtac| ring].

1293

rewrite <- (PosNormMin radix b prec); auto with zarith.

1294

apply Zle_trans with (1*Zpos (vNum b) )%Z; auto with zarith.

1295

unfold nNormMin; auto with zarith.

1296

assert (powerRZ radix (Fexp c) * radix / 2 =

1297

(Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))%R.

1298

unfold FtoRradix, FtoR; simpl.

1299

rewrite mult_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1300

rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith.

1301

replace (IZR radixH) with (radix/2)%R.

1302

replace (pred prec + (Fexp c - prec + 1))%Z with (Fexp c); [unfold Rdiv; ring|idtac].

1303

rewrite inj_pred; auto with zarith; unfold Zpred; ring.

1304

rewrite radixEven; rewrite mult_IZR; simpl; field.

1305

assert (c' <= powerRZ radix (Fexp c) * radix / 2)%R.

1306

rewrite H3.

1307

unfold FtoRradix; rewrite <- FnormalizeCorrect with radix b prec (Float radixH (Fexp c)); auto.

1308

generalize ClosestMonotone; unfold MonotoneP; intros T.

1309

apply T with b (phi*c)%R

1310

(powerRZ radix (Fexp c)*(radixH+powerRZ radix (1-prec) /2))%R; auto; clear T.

1311

apply Rle_lt_trans with (phi*((powerRZ radix prec -1)*powerRZ radix (Fexp c)))%R.

1312

apply Rmult_le_compat_l.

1313

left; apply phi_Pos.

1314

unfold FtoRradix, FtoR; simpl; apply Rmult_le_compat_r; auto with real zarith.

1315

apply Rle_trans with (Zpred (Zpos (vNum b))).

1316

apply Rle_IZR.

1317

assert (Fnum c < (Zpos (vNum b)))%Z; auto with zarith float.

1318

apply Zle_lt_trans with (Zabs (Fnum c)); auto with zarith float.

1319

unfold Zpred; rewrite plus_IZR; rewrite pGivesBound; rewrite Zpower_nat_Z_powerRZ.

1320

simpl; right; ring.

1321

apply Rle_lt_trans with (powerRZ radix (Fexp c)*(phi*(powerRZ radix prec - 1)))%R;[right; ring|idtac].

1322

apply Rmult_lt_compat_l; auto with real zarith.

1323

unfold phi.

1324

apply Rle_lt_trans with ((radixH+radix*u)*(1-powerRZ radix (-prec)))%R.

1325

right; apply trans_eq with ((radixH + radix * u)*

1326

(powerRZ radix prec*u - u))%R;[ring|unfold u].

1327

replace (powerRZ radix prec * powerRZ radix (- prec))%R with 1%R; auto with real.

1328

rewrite <- powerRZ_add; auto with real zarith.

1329

replace (prec+-prec)%Z with 0%Z; simpl; auto with zarith.

1330

apply Rle_lt_trans with (radixH+((radix*u-radixH*powerRZ radix (-prec))-radix*u

1331

*powerRZ radix (-prec)))%R;[right; ring|idtac].

1332

apply Rplus_lt_compat_l.

1333

replace (IZR radixH) with (radix/2)%R.

1334

replace (radix * u - radix/2 * powerRZ radix (- prec))%R with

1335

(powerRZ radix (1 - prec) / 2)%R.

1336

apply Rlt_le_trans with (powerRZ radix (1 - prec) / 2-0)%R;[idtac|right; ring].

1337

unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_contravar.

1338

apply Rle_lt_trans with (radix*u*0)%R;[right; ring|idtac].

1339

unfold u; apply Rmult_lt_compat_l; auto with real zarith.

1340

apply Rle_lt_trans with (radix*0)%R;[right; ring|idtac].

1341

apply Rmult_lt_compat_l; auto with real zarith.

1342

unfold u, Zminus; rewrite powerRZ_add; auto with real zarith.

1343

simpl; field.

1344

rewrite radixEven; rewrite mult_IZR; simpl; field; auto with real.

1345

apply ClosestSuccPred with prec; auto with zarith real float.

1346

rewrite FnormalizeCorrect; auto with zarith.

1347

fold FtoRradix; rewrite <- H3.

1348

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1349

powerRZ radix (Fexp c) * radix / 2)%R with

1350

(powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2)%R.

1351

2: replace (IZR radixH) with (radix/2)%R;[field|idtac].

1352

2:rewrite radixEven; rewrite mult_IZR; simpl; field.

1353

rewrite Rabs_right.

1354

2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1355

rewrite succNormal; auto with zarith float.

1356

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

1357

fold FtoRradix; rewrite <- H3.

1358

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1359

(powerRZ radix (Fexp c) * radix / 2 +

1360

powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c))))))%R

1361

with (powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2

1362

- powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c)))))%R.

1363

case (Zle_or_lt (- dExp b) (Fexp c - prec + 1)); intros I.

1364

replace (Fnormalize radix b prec (Float radixH (Fexp c))) with

1365

(Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)).

1366

simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).

1367

replace (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 -

1368

powerRZ radix (Fexp c - prec + 1))%R with

1369

(-(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2))%R.

1370

rewrite Rabs_Ropp.

1371

rewrite Rabs_right; auto with real.

1372

apply Rle_ge; unfold Rdiv;repeat apply Rmult_le_pos; auto with real zarith.

1373

replace (Fexp c - prec + 1)%Z with (Fexp c+(1-prec))%Z;[idtac| ring].

1374

rewrite powerRZ_add; auto with real zarith; field.

1375

apply FcanonicUnique with radix b prec; auto with zarith float.

1376

left; apply H6; auto.

1377

rewrite FnormalizeCorrect; auto with zarith float; fold FtoRradix; rewrite <- H5;auto.

1378

rewrite Rabs_left1.

1379

apply Rplus_le_reg_l with

1380

(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2)%R.

1381

apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec))%R.

1382

right; field.

1383

apply Rle_trans with

1384

(powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c)))))%R;[idtac|right; ring].

1385

rewrite <- powerRZ_add; auto with real zarith.

1386

apply Rle_powerRZ; auto with real zarith.

1387

apply Zle_trans with (-dExp b)%Z; auto with zarith.

1388

assert (Fbounded b (Fnormalize radix b prec (Float radixH (Fexp c)))); auto with zarith float.

1389

apply Rplus_le_reg_l with

1390

(powerRZ radix (Fexp (Fnormalize radix b prec (Float radixH (Fexp c))))).

1391

ring_simplify.

1392

apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec))%R.

1393

unfold Rdiv; apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) *1)%R;[idtac|right; ring].

1394

apply Rmult_le_compat_l; [apply Rmult_le_pos; auto with real zarith|idtac].

1395

apply Rle_trans with (/1)%R; auto with real.

1396

rewrite <- powerRZ_add; auto with real zarith.

1397

apply Rle_powerRZ; auto with real zarith.

1398

apply Zle_trans with (-dExp b)%Z; auto with zarith.

1399

assert (Fbounded b (Fnormalize radix b prec (Float radixH (Fexp c)))); auto with zarith float.

1400

replace (IZR radixH) with (radix/2)%R;[field|idtac].

1401

rewrite radixEven; rewrite mult_IZR; simpl; field.

1402

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

1403

fold FtoRradix; rewrite <- H3.

1404

unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1405

rewrite FnormalizeCorrect; auto with zarith.

1406

fold FtoRradix; rewrite <- H3.

1407

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1408

powerRZ radix (Fexp c) * radix / 2)%R with

1409

(powerRZ radix (Fexp c)*powerRZ radix (1 - prec) / 2)%R.

1410

2: replace (IZR radixH) with (radix/2)%R;[field|idtac].

1411

2:rewrite radixEven; rewrite mult_IZR; simpl; field.

1412

rewrite Rabs_right.

1413

2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1414

case (Zle_or_lt (- dExp b) (Fexp c - prec + 1)); intros I.

1415

replace (Fnormalize radix b prec (Float radixH (Fexp c)))

1416

with (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)).

1417

2: apply FcanonicUnique with radix b prec; auto with zarith float.

1418

2: left; apply H6; auto.

1419

2: rewrite FnormalizeCorrect; auto with zarith float; fold FtoRradix; rewrite <- H5;auto.

1420

case (Rle_or_lt (powerRZ radix (prec - dExp b))

1421

(powerRZ radix (Fexp c) * radix / 2)); intros M.

1422

case (Z_eq_dec (radixH * nNormMin radix prec) (nNormMin radix prec)); intros N.

1423

rewrite predNormal1; auto.

1424

rewrite <- H7.

1425

simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).

1426

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1427

(powerRZ radix (Fexp c) * radix / 2 -

1428

powerRZ radix (Fexp c - prec + 1 - 1)))%R with

1429

((powerRZ radix (Fexp c) *powerRZ radix (1 - prec)) *(/ 2+/radix))%R.

1430

rewrite Rabs_right.

1431

unfold Rdiv; apply Rmult_le_compat_l.

1432

apply Rmult_le_pos; auto with real zarith.

1433

apply Rle_trans with (/2+0)%R; auto with real zarith.

1434

apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.

1435

apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.

1436

replace (Fexp c - prec + 1-1)%Z with (Fexp c+(1-prec)+(-1))%Z;[idtac|ring].

1437

repeat rewrite powerRZ_add; auto with real zarith.

1438

simpl (powerRZ radix (-1)).

1439

replace (IZR radixH) with (radix/2)%R;[field; auto with real zarith|idtac].

1440

rewrite radixEven; rewrite mult_IZR; simpl; field.

1441

left; auto.

1442

rewrite <- H7; auto.

1443

rewrite predNormal2; auto.

1444

rewrite <- H7.

1445

simpl ((Fexp (Float (radixH * nNormMin radix prec) (Fexp c - prec + 1)))).

1446

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1447

(powerRZ radix (Fexp c) * radix / 2 - powerRZ radix (Fexp c - prec + 1)))%R

1448

with ((3*(powerRZ radix (Fexp c) * powerRZ radix (1 - prec)/ 2)))%R.

1449

rewrite Rabs_right; auto with real.

1450

apply Rle_trans with (1*(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2))%R;

1451

[right; ring|apply Rmult_le_compat_r].

1452

unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1453

apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.

1454

unfold Rdiv; apply Rle_ge; repeat apply Rmult_le_pos; auto with real zarith.

1455

apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.

1456

replace (Fexp c - prec + 1)%Z with (Fexp c+(1-prec))%Z;[idtac| ring].

1457

rewrite powerRZ_add; auto with real zarith.

1458

replace (IZR radixH) with (radix/2)%R;[field|idtac].

1459

rewrite radixEven; rewrite mult_IZR; simpl; field.

1460

left; auto.

1461

rewrite <- H7; auto.

1462

rewrite predSmallOnes.

1463

rewrite <- H7.

1464

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1465

(powerRZ radix (Fexp c) * radix / 2 - eta))%R with

1466

(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 +eta)%R.

1467

rewrite Rabs_right.

1468

apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2+0)%R; auto with real.

1469

apply Rplus_le_compat_l.

1470

unfold eta; auto with real zarith.

1471

apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.

1472

apply Rplus_le_compat; try unfold eta; auto with real zarith.

1473

unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1474

replace (IZR radixH) with (radix/2)%R;[field|idtac].

1475

rewrite radixEven; rewrite mult_IZR; simpl; field.

1476

left; auto.

1477

rewrite <- H7; auto.

1478

rewrite Rabs_right; auto.

1479

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1480

rewrite predSmallOnes.

1481

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

1482

fold FtoRradix; rewrite <- H3.

1483

replace (powerRZ radix (Fexp c) * (radixH + powerRZ radix (1 - prec) / 2) -

1484

(powerRZ radix (Fexp c) * radix / 2 - eta))%R with

1485

(powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2 +eta)%R.

1486

rewrite Rabs_right.

1487

apply Rle_trans with (powerRZ radix (Fexp c) * powerRZ radix (1 - prec) / 2+0)%R; auto with real.

1488

apply Rplus_le_compat_l.

1489

unfold eta; auto with real zarith.

1490

apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.

1491

apply Rplus_le_compat; try unfold eta; auto with real zarith.

1492

unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1493

replace (IZR radixH) with (radix/2)%R;[field|idtac].

1494

rewrite radixEven; rewrite mult_IZR; simpl; field.

1495

apply FnormalizeCanonic; auto with zarith.

1496

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

1497

fold FtoRradix; rewrite <- H3.

1498

rewrite Rabs_right.

1499

apply Rlt_le_trans with (powerRZ radix (Fexp c+1)).

1500

rewrite powerRZ_add; auto with real zarith.

1501

unfold Rdiv; rewrite Rmult_assoc; apply Rmult_lt_compat_l; auto with real zarith.

1502

simpl; apply Rmult_lt_compat_l; auto with real zarith.

1503

apply Rlt_le_trans with (/1)%R; auto with real.

1504

apply Rle_powerRZ; auto with real zarith.

1505

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1506

assert (powerRZ radix (Fexp c-1) <= c')%R.

1507

apply Rle_trans with (Float 1 (Fexp c -1)).

1508

right; unfold FtoRradix, FtoR; simpl; ring.

1509

unfold FtoRradix; apply RleBoundRoundl with b prec (Closest b radix) (phi*c)%R; auto with zarith.

1510

apply ClosestRoundedModeP with prec; auto with zarith.

1511

split; simpl; auto with zarith float.

1512

apply vNumbMoreThanOne with radix prec; auto with zarith.

1513

unfold FtoRradix, FtoR, Zminus; simpl; rewrite powerRZ_add; auto with real zarith.

1514

apply Rle_trans with (/radix*powerRZ radix (Fexp c))%R.

1515

simpl; right; field; auto with real zarith.

1516

rewrite <- Rmult_assoc; apply Rmult_le_compat_r; auto with real zarith.

1517

apply Rle_trans with (phi*nNormMin radix prec)%R.

1518

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1519

unfold phi, u.

1520

apply Rle_trans with (radixH*(powerRZ radix (-prec)

1521

*powerRZ radix (pred prec))+radix*(powerRZ radix (-prec)

1522

*powerRZ radix (pred prec)*powerRZ radix (-prec)))%R;

1523

[idtac|right; ring].

1524

repeat rewrite <- powerRZ_add; auto with real zarith.

1525

apply Rle_trans with (/radix+0)%R; auto with real; apply Rplus_le_compat.

1526

apply Rle_trans with (1*/radix)%R; auto with real.

1527

apply Rmult_le_compat; auto with real zarith.

1528

rewrite inj_pred; auto with zarith; unfold Zpred.

1529

replace (-prec+(prec+-1))%Z with (-1)%Z;[idtac|ring].

1530

simpl; right; field; auto with real zarith.

1531

apply Rmult_le_pos; auto with real zarith.

1532

apply Rmult_le_compat_l.

1533

left; apply phi_Pos.

1534

rewrite <- (Zabs_eq (Fnum c)).

1535

apply Rle_IZR.

1536

apply pNormal_absolu_min with b; auto with zarith.

1537

case H; auto; intros H2'; elim H2'; intros H3' (H4',H5').

1538

absurd (-dExp b <Fexp c)%Z; auto with zarith.

1539

apply LeR0Fnum with radix; auto with zarith.

1540

assert (powerRZ radix (Fexp c) * (radix / 2 + powerRZ radix (- 2))

1541

= Float (radixH * radix*radix + 1) (Fexp c-2))%R.

1542

unfold FtoRradix, FtoR.

1543

apply trans_eq with ((radixH *radix*radix + 1) %Z*

1544

powerRZ radix (Fexp c - 2))%R; auto with real.

1545

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

1546

rewrite plus_IZR; rewrite mult_IZR; rewrite mult_IZR.

1547

replace (IZR radixH) with (radix/2)%R.

1548

simpl; field; auto with real zarith.

1549

rewrite radixEven; rewrite mult_IZR; simpl; field.

1550

assert (Fbounded b

1551

(Float (radixH * radix*radix+ 1) (Fexp c - 2))).

1552

split; simpl; auto with zarith.

1553

rewrite Zabs_eq; auto with zarith.

1554

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.

1555

replace (Zpower_nat radix 3) with ((radixH * radix * radix+radixH * radix * radix))%Z.

1556

apply Zplus_lt_compat_l; auto with zarith.

1557

apply Zlt_le_trans with (1*2*2)%Z; auto with zarith.

1558

repeat apply Zmult_le_compat; auto with zarith.

1559

unfold Zpower_nat; simpl.

1560

repeat rewrite radixEven; ring.

1561

rewrite H10.

1562

apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

1563

apply ClosestRoundedModeP with prec; auto with zarith.

1564

fold FtoRradix; rewrite <- H10.

1565

apply Rle_trans with (powerRZ radix (Fexp c) * radix / 2+

1566

powerRZ radix (Fexp c)*powerRZ radix (- 2))%R;[idtac|right; unfold Rdiv;ring].

1567

apply Rplus_le_compat; auto.

1568

unfold eta; rewrite <- powerRZ_add; auto with real zarith.

1569

apply Rle_powerRZ; auto with real zarith.

1570

Qed.

1571

1572

1573

Lemma Algo1_correct_r2_aux_aux1:forall (c cinf:float) (r:R),

1574

(radix=2)%Z ->

1575

Fcanonic radix b c -> (0 <= c)%R ->

1576

(Fnum c <> nNormMin radix prec) ->

1577

(Fnum c <> nNormMin radix prec+1)%Z ->

1578

(r <= 5/4*powerRZ radix (Fexp c))%R ->

1579

Closest b radix (c-r) cinf ->

1580

(FtoRradix (FPred b radix prec c) <= cinf)%R.

1581

intros c cinf r K; intros.

1582

assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].

1583

assert (G1:(0 < 4)%R).

1584

apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.

1585

assert (G2:(0 < 5)%R).

1586

apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.

1587

assert (FtoRradix (FPred b radix prec c) = c -powerRZ radix (Fexp c))%R.

1588

rewrite FPredSimpl4; auto.

1589

unfold FtoRradix, FtoR, Zpred; simpl.

1590

rewrite plus_IZR; simpl; ring.

1591

assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.

1592

apply Zlt_le_trans with 0%Z.

1593

assert (0 < pPred (vNum b))%Z; auto with zarith float.

1594

apply pPredMoreThanOne with radix prec; auto with zarith.

1595

apply LeR0Fnum with radix ; auto with real zarith.

1596

assert (c - 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)

1597

= (-(/4 * powerRZ radix (Fexp c))))%R.

1598

fold FtoRradix; rewrite H5; field.

1599

unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-r)%R (c-5 / 4 * powerRZ radix (Fexp c))%R; auto with zarith.

1600

apply FPredCanonic; auto with zarith.

1601

rewrite H6; rewrite Rabs_Ropp.

1602

rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

1603

rewrite FSucPred; auto with zarith; fold FtoRradix.

1604

replace (c - 5 / 4 * powerRZ radix (Fexp c) - c)%R with (-(5/4*powerRZ radix (Fexp c)))%R by ring.

1605

rewrite Rabs_Ropp; rewrite Rabs_right.

1606

apply Rmult_lt_compat_r; auto with real zarith.

1607

unfold Rdiv; apply Rle_lt_trans with (1*/4)%R; auto with real.

1608

apply Rmult_lt_compat_r; auto with real.

1609

apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.

1610

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1611

rewrite H6; rewrite Rabs_Ropp.

1612

rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

1613

assert ((FtoRradix (FPred b radix prec (FPred b radix prec c)) =

1614

c-2*powerRZ radix (Fexp c)))%R.

1615

assert (FPred b radix prec c = Float (Zpred (Fnum c)) (Fexp c)).

1616

rewrite FPredSimpl4; auto with zarith.

1617

assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.

1618

apply Zlt_le_trans with 0%Z.

1619

assert (0 < pPred (vNum b))%Z; auto with zarith float.

1620

apply pPredMoreThanOne with radix prec; auto with zarith.

1621

apply LeR0Fnum with radix ; auto with real zarith.

1622

rewrite H7; rewrite FPredSimpl4; auto with zarith.

1623

unfold FtoRradix, FtoR; simpl.

1624

unfold Zpred; repeat rewrite plus_IZR; simpl; ring.

1625

simpl.

1626

assert (-pPred (vNum b) < (Zpred (Fnum c)))%Z; auto with zarith float.

1627

apply Zlt_le_trans with (Zpred 0)%Z; unfold pPred, Zpred.

1628

assert (2 < Zpos (vNum b))%Z; auto with zarith float.

1629

rewrite pGivesBound; apply Zle_lt_trans with (Zpower_nat radix 1); auto with zarith.

1630

unfold Zpower_nat; simpl; auto with zarith.

1631

assert (0 <= Fnum c)%Z; auto with zarith.

1632

apply LeR0Fnum with radix ; auto with real zarith.

1633

simpl; auto with zarith.

1634

Contradict H2; rewrite <- H2; unfold Zpred; ring.

1635

fold FtoRradix; rewrite H7.

1636

replace (c - 5 / 4 * powerRZ radix (Fexp c) - (c - 2 * powerRZ radix (Fexp c)))%R

1637

with ( 3/ 4 * powerRZ radix (Fexp c))%R by field.

1638

rewrite Rabs_right; auto with real.

1639

apply Rmult_lt_compat_r; auto with real zarith.

1640

unfold Rdiv; apply Rle_lt_trans with (1*/4)%R; auto with real.

1641

apply Rmult_lt_compat_r; auto with real.

1642

apply Rlt_le_trans with (IZR 3); auto with real zarith; simpl; right; ring.

1643

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1644

apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.

1645

unfold Rminus; apply Rplus_le_compat_l; auto with real.

1646

Qed.

1647

1648

Lemma Algo1_correct_r2_aux_aux2:forall (c c' e cinf:float),

1649

(radix=2)%Z ->

1650

Fcanonic radix b c -> (0 <= c)%R ->

1651

(Fnum c = nNormMin radix prec+1)%Z ->

1652

(-dExp b <= Fexp c-2)%Z ->

1653

Closest b radix (phi*c) c' ->

1654

Closest b radix (c'+eta) e ->

1655

Closest b radix (c-e) cinf ->

1656

(FtoRradix (FPred b radix prec c) <= cinf)%R.

1657

intros.

1658

assert (Bc:(Fbounded b c));[apply FcanonicBound with radix; auto|idtac].

1659

assert (G1:(0 < 4)%R).

1660

apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.

1661

assert (G2:(0 < 5)%R).

1662

apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.

1663

generalize ClosestMonotone; unfold MonotoneP; intros T.

1664

unfold FtoRradix; apply T with b (c-5 / 4 * powerRZ radix (Fexp c))%R (c-e)%R; auto.

1665

unfold Rminus; apply Rplus_lt_compat_l; auto with real.

1666

apply Ropp_lt_contravar.

1667

apply Rle_lt_trans with (Float 1 (Fexp c)).

1668

apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

1669

apply ClosestRoundedModeP with prec; auto with zarith.

1670

split; simpl; auto with zarith float.

1671

apply vNumbMoreThanOne with radix prec; auto with zarith.

1672

apply Rle_trans with (FtoRradix (Float 3 (Fexp c-2))+powerRZ radix (Fexp c -2))%R.

1673

apply Rplus_le_compat.

1674

apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.

1675

apply ClosestRoundedModeP with prec; auto with zarith.

1676

split; simpl; auto with zarith float.

1677

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 2); auto with zarith.

1678

unfold Zpower_nat; rewrite H; simpl; auto with zarith.

1679

unfold FtoRradix, FtoR; simpl.

1680

rewrite H2; unfold phi, u.

1681

rewrite plus_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1682

replace radixH with 1%Z; auto with zarith.

1683

replace (radix*powerRZ radix (- prec))%R with (powerRZ radix (1-prec)).

1684

apply Rle_trans with

1685

(powerRZ radix (Fexp c) *(powerRZ radix (-prec)*

1686

((powerRZ radix (pred prec) +1 +

1687

powerRZ radix (1 - prec)*powerRZ radix (pred prec) +

1688

powerRZ radix (1 - prec)))))%R;[right; simpl; ring|idtac].

1689

rewrite inj_pred; auto with zarith; unfold Zpred.

1690

replace (powerRZ radix (1 - prec) * powerRZ radix (prec + -1))%R

1691

with 1%R.

1692

apply Rle_trans with (powerRZ radix (Fexp c) *(3/4))%R.

1693

apply Rmult_le_compat_l; auto with real zarith.

1694

apply Rle_trans with (powerRZ radix (- prec) *

1695

powerRZ radix (prec + -1) + (2* powerRZ radix (- prec)

1696

+ powerRZ radix (- prec)*powerRZ radix (1 - prec)))%R;[right; ring|idtac].

1697

repeat rewrite <- powerRZ_add; auto with real zarith.

1698

apply Rle_trans with (/2+/4)%R;[apply Rplus_le_compat|right; field].

1699

replace (- prec + (prec + -1))%Z with (-1)%Z by ring.

1700

simpl; rewrite H; simpl; right; field.

1701

apply Rle_trans with

1702

(2 * powerRZ radix (- 4) + powerRZ radix (- 4))%R.

1703

apply Rplus_le_compat.

1704

apply Rmult_le_compat_l; auto with real zarith.

1705

apply Rle_powerRZ; auto with real zarith.

1706

apply Rle_powerRZ; auto with real zarith.

1707

rewrite H; simpl; apply Rmult_le_reg_l with (IZR 16); auto with real zarith.

1708

apply Rle_trans with (IZR 3);[right; simpl; field|idtac].

1709

apply Rle_trans with (IZR 4);[auto with real zarith|right; simpl; field].

1710

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

1711

rewrite H; simpl; right; field.

1712

rewrite <- powerRZ_add; auto with real zarith.

1713

replace (1 - prec + (prec + -1))%Z with 0%Z by ring; simpl; ring.

1714

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

1715

unfold eta; apply Rle_powerRZ; auto with real zarith.

1716

unfold FtoRradix, FtoR; simpl.

1717

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

1718

rewrite H; simpl; right; field.

1719

unfold FtoRradix, FtoR; simpl; apply Rmult_lt_compat_r; auto with real zarith.

1720

apply Rle_lt_trans with (4/4)%R; auto with real.

1721

right; field.

1722

unfold Rdiv; apply Rmult_lt_compat_r; auto with real.

1723

replace 5%R with (IZR 5);[idtac|simpl; ring].

1724

replace 4%R with (IZR 4);[auto with real zarith|simpl; ring].

1725

assert (FtoRradix (FPred b radix prec c) = c -powerRZ radix (Fexp c))%R.

1726

rewrite FPredSimpl4; auto.

1727

unfold FtoRradix, FtoR, Zpred; simpl.

1728

rewrite plus_IZR; simpl; ring.

1729

assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.

1730

apply Zlt_le_trans with 0%Z.

1731

assert (0 < pPred (vNum b))%Z; auto with zarith float.

1732

apply pPredMoreThanOne with radix prec; auto with zarith.

1733

apply LeR0Fnum with radix ; auto with real zarith.

1734

rewrite H2; auto with zarith.

1735

assert (c - 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)

1736

= (-(/4 * powerRZ radix (Fexp c))))%R.

1737

fold FtoRradix; rewrite H7; field.

1738

apply ClosestSuccPred with prec; auto with zarith.

1739

apply FBoundedPred; auto with zarith.

1740

apply FPredCanonic; auto with zarith.

1741

rewrite H8; rewrite Rabs_Ropp.

1742

rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

1743

rewrite FSucPred; auto with zarith; fold FtoRradix.

1744

replace (c - 5 / 4 * powerRZ radix (Fexp c) - c)%R with (-(5/4*powerRZ radix (Fexp c)))%R by ring.

1745

rewrite Rabs_Ropp; rewrite Rabs_right.

1746

apply Rmult_le_compat_r; auto with real zarith.

1747

unfold Rdiv; apply Rle_trans with (1*/4)%R; auto with real.

1748

apply Rmult_le_compat_r; auto with real.

1749

apply Rle_trans with (IZR 5); auto with real zarith; simpl; right; ring.

1750

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1751

rewrite H8; rewrite Rabs_Ropp.

1752

rewrite Rabs_right;[idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

1753

assert (FPred b radix prec c=Float (nNormMin radix prec) (Fexp c)).

1754

rewrite FPredSimpl4; auto with zarith.

1755

replace (Zpred (Fnum c)) with (nNormMin radix prec); auto.

1756

rewrite H2; unfold Zpred; ring.

1757

assert (-pPred (vNum b) < Fnum c)%Z; auto with zarith float.

1758

apply Zlt_le_trans with 0%Z.

1759

assert (0 < pPred (vNum b))%Z; auto with zarith float.

1760

apply pPredMoreThanOne with radix prec; auto with zarith.

1761

apply LeR0Fnum with radix ; auto with real zarith.

1762

assert ((FtoRradix (FPred b radix prec (FPred b radix prec c)) =

1763

c-3/2*powerRZ radix (Fexp c)))%R.

1764

rewrite H9; rewrite FPredSimpl2; auto with zarith.

1765

unfold FtoRradix, FtoR; simpl.

1766

rewrite H2; unfold pPred, Zpred; repeat rewrite plus_IZR; rewrite pGivesBound.

1767

unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ; simpl.

1768

rewrite inj_pred; auto with zarith; unfold Zpred.

1769

repeat rewrite powerRZ_add; auto with real zarith.

1770

simpl; rewrite H; simpl; field.

1771

simpl; auto with zarith.

1772

fold FtoRradix; rewrite H10.

1773

replace (c - 5 / 4 * powerRZ radix (Fexp c) - (c - 3/2 * powerRZ radix (Fexp c)))%R

1774

with ( / 4 * powerRZ radix (Fexp c))%R by field.

1775

rewrite Rabs_right; auto with real.

1776

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1777

Qed.

1778

1779

1780

1781

Lemma Algo1_correct_r2_aux_aux3:forall (c c' e cinf:float),

1782

(radix=2)%Z ->

1783

Fcanonic radix b c -> (0 <= c)%R ->

1784

(-dExp b <= Fexp c-3)%Z ->

1785

(Fnum c = nNormMin radix prec) ->

1786

Closest b radix (phi*c) c' ->

1787

Closest b radix (c'+eta) e ->

1788

Closest b radix (c-e) cinf ->

1789

(prec=4 -> EvenClosest b radix prec (phi*c)%R c'

1790

\/ AFZClosest b radix (c-e)%R cinf) ->

1791

(FtoRradix (FPred b radix prec c) <= cinf)%R.

1792

intros c c' e cinf H H0 H1 H2 H3 H4 H5 H6 MM.

1793

assert (FtoRradix (FPred b radix prec c) = (c-/2*powerRZ radix (Fexp c)))%R.

1794

rewrite FPredSimpl2; auto with zarith.

1795

unfold FtoRradix, FtoR, pPred, Zpred.

1796

rewrite pGivesBound; rewrite H3; simpl.

1797

rewrite plus_IZR; unfold nNormMin; repeat rewrite Zpower_nat_Z_powerRZ.

1798

rewrite inj_pred; auto with zarith; unfold Zpred.

1799

repeat rewrite powerRZ_add; auto with real zarith.

1800

rewrite H; simpl; field.

1801

case (Zle_or_lt (-dExp b) (Fexp c -prec)); intros I.

1802

assert (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) -

1803

FtoR radix (FPred b radix prec c) =

1804

(-powerRZ radix (Fexp c + 1 - prec)))%R.

1805

fold FtoRradix; rewrite H7; ring.

1806

unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-/2*powerRZ radix (Fexp c) - powerRZ radix (Fexp c +1-prec))%R; auto with zarith.

1807

apply FPredCanonic; auto with zarith.

1808

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

1809

2: apply Rle_ge; auto with real zarith.

1810

rewrite FSucPred; auto with zarith; fold FtoRradix.

1811

replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) - c)%R with

1812

(-(/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c + 1 - prec)))%R by ring.

1813

rewrite Rabs_Ropp; rewrite Rabs_right.

1814

apply Rle_lt_trans with (0+powerRZ radix (Fexp c + 1 - prec))%R;[right; ring|idtac].

1815

apply Rplus_lt_compat_r; auto with real zarith.

1816

apply Rle_lt_trans with (/2*0)%R; try apply Rmult_lt_compat_l; auto with real zarith.

1817

apply Rle_ge; apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.

1818

apply Rmult_le_pos; auto with real zarith.

1819

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

1820

2: apply Rle_ge; auto with real zarith.

1821

rewrite FPredSimpl2 with b radix prec c; auto with zarith.

1822

rewrite FPredSimpl4; simpl; auto with zarith.

1823

replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with

1824

(c-powerRZ radix (Fexp c))%R.

1825

replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec) -

1826

(c - powerRZ radix (Fexp c)))%R with

1827

(/ 2 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c + 1 - prec))%R by field.

1828

rewrite Rabs_right.

1829

apply Rplus_lt_reg_r with (powerRZ radix (Fexp c + 1 - prec)).

1830

apply Rmult_lt_reg_l with 2%R; auto with real.

1831

apply Rle_lt_trans with (4*powerRZ radix (Fexp c + 1 - prec))%R;[right; field|idtac].

1832

apply Rle_lt_trans with (powerRZ radix (Fexp c + 3 - prec)).

1833

right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

1834

rewrite H; simpl; ring.

1835

apply Rlt_le_trans with (powerRZ radix (Fexp c));[idtac|right; field].

1836

apply Rlt_powerRZ; auto with real zarith.

1837

apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (Fexp c + 1 - prec)).

1838

ring_simplify.

1839

apply Rle_trans with (powerRZ radix (Fexp c -1)); auto with real zarith.

1840

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

1841

rewrite H; simpl; right; field.

1842

unfold FtoRradix, FtoR; simpl.

1843

rewrite H3; unfold pPred; rewrite pGivesBound.

1844

unfold nNormMin, Zpred; repeat rewrite plus_IZR.

1845

repeat rewrite Zpower_nat_Z_powerRZ; simpl.

1846

rewrite inj_pred; auto with zarith; unfold Zpred.

1847

repeat rewrite powerRZ_add; auto with real zarith.

1848

rewrite H; simpl; field.

1849

assert (0 < pPred (vNum b))%Z; auto with zarith.

1850

apply pPredMoreThanOne with radix prec; auto with zarith.

1851

assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.

1852

apply nNormMimLtvNum; auto with zarith.

1853

unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.

1854

apply Rle_trans with (-(/ 2 * powerRZ radix (Fexp c)

1855

+powerRZ radix (Fexp c + 1 - prec)))%R;[right; ring|idtac].

1856

apply Ropp_le_contravar.

1857

assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c + 1 - prec)

1858

= Float (nNormMin radix prec +2) (Fexp c -prec))%R.

1859

unfold FtoRradix, FtoR; simpl.

1860

rewrite plus_IZR; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1861

rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.

1862

repeat rewrite powerRZ_add; auto with real zarith.

1863

rewrite H; simpl; rewrite <- Rinv_powerRZ; auto with real zarith.

1864

field; auto with real zarith.

1865

assert (0 < powerRZ 2 prec)%R; auto with real zarith.

1866

rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

1867

apply ClosestRoundedModeP with prec; auto with zarith.

1868

split; simpl; auto with zarith.

1869

rewrite Zabs_eq.

1870

rewrite PosNormMin with radix b prec; auto with zarith.

1871

rewrite H; apply Zlt_le_trans with (nNormMin radix prec + nNormMin radix prec)%Z; auto with zarith.

1872

rewrite H; apply Zplus_lt_compat_l.

1873

unfold nNormMin; apply Zle_lt_trans with (Zpower_nat 2 1); auto with zarith.

1874

apply Zeq_le; rewrite H; ring.

1875

unfold nNormMin; auto with zarith.

1876

fold FtoRradix; rewrite <- H9.

1877

apply Rle_trans with ((/ 2 * powerRZ radix (Fexp c)

1878

+ powerRZ radix (Fexp c- prec)) + powerRZ radix (Fexp c- prec))%R.

1879

2: unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

1880

2: rewrite H; simpl; right; ring.

1881

apply Rplus_le_compat.

1882

2: unfold eta; apply Rle_powerRZ; auto with real zarith.

1883

assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (Fexp c - prec)

1884

= Float (nNormMin radix prec+1) (Fexp c-prec))%R.

1885

unfold FtoRradix, FtoR; simpl; rewrite plus_IZR.

1886

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; simpl.

1887

rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.

1888

repeat rewrite powerRZ_add; auto with real zarith.

1889

rewrite <- Rinv_powerRZ; auto with real zarith; simpl.

1890

rewrite H; simpl; field.

1891

assert (0 < powerRZ 2 prec)%R; auto with real zarith.

1892

rewrite H10.

1893

apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.

1894

apply ClosestRoundedModeP with prec; auto with zarith.

1895

split; simpl; auto with zarith.

1896

replace (nNormMin radix prec) with (radixH*nNormMin radix prec)%Z.

1897

apply phi_bounded_aux.

1898

replace radixH with 1%Z; auto with zarith.

1899

fold FtoRradix; rewrite <- H10.

1900

unfold phi,u, FtoRradix, FtoR; simpl.

1901

rewrite H3; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

1902

rewrite inj_pred; auto with zarith; unfold Zpred.

1903

unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

1904

rewrite <- Rinv_powerRZ; auto with real zarith; simpl.

1905

replace (IZR radixH) with 1%R.

1906

rewrite H; simpl; right; field.

1907

assert (0 < powerRZ 2 prec)%R; auto with real zarith.

1908

replace radixH with 1%Z; auto with real zarith.

1909

case (Zle_lt_or_eq (Fexp c) (-dExp b+prec-1)); auto with zarith; intros I'.

1910

assert (G1: (0 < 8)%R).

1911

apply Rlt_le_trans with (IZR 8); [auto with real zarith|simpl; right; ring].

1912

assert (G2: (0 < 5)%R).

1913

apply Rlt_le_trans with (IZR 5); [auto with real zarith|simpl; right; ring].

1914

assert (c - 5/8* powerRZ radix (Fexp c) - FtoR radix (FPred b radix prec c)

1915

= (-(/ 8 * powerRZ radix (Fexp c))))%R.

1916

fold FtoRradix; rewrite H7; field.

1917

unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-5/8*powerRZ radix (Fexp c))%R; auto with zarith.

1918

apply FPredCanonic; auto with zarith.

1919

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

1920

2: apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

1921

rewrite FSucPred; auto with zarith; fold FtoRradix.

1922

replace (c - 5/8* powerRZ radix (Fexp c) - c)%R with

1923

(- (5/8*powerRZ radix (Fexp c)))%R by ring.

1924

rewrite Rabs_Ropp; rewrite Rabs_right.

1925

2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1926

apply Rmult_lt_compat_r; auto with real zarith.

1927

apply Rle_lt_trans with (1*/8)%R;

1928

[right; ring|unfold Rdiv; apply Rmult_lt_compat_r; auto with real zarith].

1929

apply Rlt_le_trans with (IZR 5)%R; auto with real zarith.

1930

right; simpl; ring.

1931

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

1932

2: apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

1933

rewrite FPredSimpl2 with b radix prec c; auto with zarith.

1934

rewrite FPredSimpl4; simpl; auto with zarith.

1935

replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with

1936

(c-powerRZ radix (Fexp c))%R.

1937

replace (c - 5/ 8 * powerRZ radix (Fexp c) -

1938

(c - powerRZ radix (Fexp c)))%R with

1939

(3/ 8 * powerRZ radix (Fexp c))%R by field.

1940

rewrite Rabs_right.

1941

2: apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

1942

2: apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.

1943

apply Rmult_lt_compat_r; auto with real zarith.

1944

apply Rle_lt_trans with (1*/8)%R;

1945

[right; ring|unfold Rdiv; apply Rmult_lt_compat_r; auto with real zarith].

1946

apply Rlt_le_trans with (IZR 3)%R; auto with real zarith.

1947

right; simpl; ring.

1948

unfold FtoRradix, FtoR; simpl.

1949

rewrite H3; unfold pPred; rewrite pGivesBound.

1950

unfold nNormMin, Zpred; repeat rewrite plus_IZR.

1951

repeat rewrite Zpower_nat_Z_powerRZ; simpl.

1952

rewrite inj_pred; auto with zarith; unfold Zpred.

1953

repeat rewrite powerRZ_add; auto with real zarith.

1954

rewrite H; simpl; field.

1955

assert (0 < pPred (vNum b))%Z; auto with zarith.

1956

apply pPredMoreThanOne with radix prec; auto with zarith.

1957

assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.

1958

apply nNormMimLtvNum; auto with zarith.

1959

unfold Rminus; apply Rplus_le_compat_l; apply Ropp_le_contravar.

1960

assert (5 / 8 * powerRZ radix (Fexp c)= Float 5 (Fexp c-3))%R.

1961

unfold FtoRradix, FtoR, Zminus; simpl.

1962

rewrite powerRZ_add; auto with real zarith.

1963

rewrite H; simpl; field.

1964

rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

1965

apply ClosestRoundedModeP with prec; auto with zarith.

1966

split; simpl; auto with zarith.

1967

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.

1968

rewrite H; simpl; auto with zarith.

1969

fold FtoRradix; rewrite <- H9.

1970

apply Rle_trans with (powerRZ radix (Fexp c-1)+ powerRZ radix (Fexp c-3))%R.

1971

2: right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

1972

2: rewrite H; simpl; field.

1973

apply Rplus_le_compat.

1974

2: unfold eta; apply Rle_powerRZ; auto with real zarith.

1975

assert (powerRZ radix (Fexp c - 1) = Float (Zpower_nat radix (Zabs_nat (Fexp c-1+dExp b))) (-dExp b))%R.

1976

unfold FtoRradix, FtoR; simpl; rewrite Zpower_nat_Z_powerRZ.

1977

rewrite <- powerRZ_add; auto with real zarith.

1978

replace (Zabs_nat (Fexp c - 1 + dExp b) + - dExp b)%Z with (Fexp c-1)%Z; auto with zarith.

1979

rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.

1980

assert (Fsubnormal radix b (Float (Zpower_nat radix (Zabs_nat (Fexp c - 1 + dExp b))) (- dExp b))).

1981

split; try split; simpl; auto with zarith.

1982

rewrite Zabs_eq; auto with zarith.

1983

rewrite pGivesBound; apply Zpower_nat_monotone_lt; auto with zarith.

1984

apply ZleLe.

1985

apply Zle_trans with (Zabs_nat (Fexp c - 1 + dExp b)+1)%nat; auto with zarith.

1986

rewrite inj_plus; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.

1987

simpl; auto with zarith.

1988

rewrite Zabs_eq; auto with zarith.

1989

apply Zle_lt_trans with (Zpower_nat radix (1+Zabs_nat (Fexp c - 1 + dExp b))).

1990

apply Zeq_le;rewrite Zpower_nat_is_exp; auto with zarith.

1991

replace (Zpower_nat radix 1) with radix; auto with zarith.

1992

unfold Zpower_nat; simpl; ring.

1993

rewrite pGivesBound; apply Zpower_nat_monotone_lt; auto with zarith.

1994

apply ZleLe.

1995

apply Zle_trans with ((1+Zabs_nat (Fexp c - 1 + dExp b)+1))%nat; auto with zarith.

1996

repeat rewrite inj_plus; rewrite <- Zabs_absolu; rewrite Zabs_eq; auto with zarith.

1997

apply Zle_trans with (Fexp c +dExp b +1)%Z; auto with zarith.

1998

replace (Z_of_nat 1) with 1%Z; auto with zarith.

1999

rewrite H10.

2000

apply ClosestStrictMonotone2r with b prec (phi*c)%R (powerRZ radix (Fexp c -1) + powerRZ radix (Fexp c -prec))%R; auto with zarith.

2001

right; auto.

2002

fold FtoRradix; rewrite <- H10.

2003

ring_simplify (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -

2004

powerRZ radix (Fexp c - 1))%R.

2005

rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).

2006

rewrite succNormal.

2007

2: right; auto.

2008

2: rewrite <- H10; auto with real zarith.

2009

rewrite <- H10; simpl.

2010

replace (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -

2011

(powerRZ radix (Fexp c - 1) + powerRZ radix (- dExp b)))%R with

2012

( - (powerRZ radix (- dExp b) - powerRZ radix (Fexp c - prec)))%R by ring.

2013

rewrite Rabs_Ropp; rewrite Rabs_right.

2014

apply Rplus_lt_reg_r with (powerRZ radix (Fexp c - prec)); ring_simplify.

2015

apply Rle_lt_trans with (powerRZ radix (1+(Fexp c - prec))).

2016

rewrite powerRZ_add; auto with real zarith.

2017

rewrite H; simpl; right; ring.

2018

apply Rlt_powerRZ; auto with real zarith.

2019

apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (Fexp c - prec)); ring_simplify.

2020

apply Rle_powerRZ; auto with real zarith.

2021

fold FtoRradix; rewrite <- H10.

2022

ring_simplify (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -

2023

powerRZ radix (Fexp c - 1))%R.

2024

rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).

2025

rewrite predSmallOnes; auto with zarith.

2026

rewrite <- H10; unfold eta.

2027

replace (powerRZ radix (Fexp c - 1) + powerRZ radix (Fexp c - prec) -

2028

(powerRZ radix (Fexp c - 1) - powerRZ radix (- dExp b)))%R with

2029

(powerRZ radix (- dExp b)+powerRZ radix (Fexp c - prec))%R by ring.

2030

rewrite Rabs_right.

2031

apply Rle_lt_trans with (0+powerRZ radix (Fexp c - prec))%R; auto with real zarith.

2032

apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.

2033

apply Rplus_le_compat; auto with real zarith.

2034

right; auto.

2035

rewrite <- H10.

2036

rewrite Rabs_right; try (apply Rle_ge; auto with real zarith).

2037

apply Rlt_powerRZ; auto with real zarith.

2038

unfold phi, u, FtoRradix, FtoR; simpl; rewrite H3.

2039

replace radixH with 1%Z; auto with zarith.

2040

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

2041

rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.

2042

repeat rewrite powerRZ_add; auto with real zarith.

2043

rewrite <- Rinv_powerRZ; auto with real zarith.

2044

rewrite H; simpl; right; field.

2045

assert (0 < powerRZ 2 prec)%R; auto with real zarith.

2046

case (Zle_lt_or_eq 4 prec); auto with zarith; intros precBis.

2047

assert (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) -

2048

FtoR radix (FPred b radix prec c) = -powerRZ radix (1- dExp b))%R.

2049

fold FtoRradix; rewrite H7; ring.

2050

unfold FtoRradix; apply ClosestStrictMonotone2l with b prec (c-e)%R (c-/2*powerRZ radix (Fexp c) - powerRZ radix (1-dExp b))%R; auto with zarith.

2051

apply FPredCanonic; auto with zarith.

2052

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

2053

2: apply Rle_ge; auto with real zarith.

2054

rewrite FSucPred; auto with zarith; fold FtoRradix.

2055

replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) - c)%R with

2056

(-(/2*powerRZ radix (Fexp c) + powerRZ radix (1-dExp b)))%R by ring.

2057

rewrite Rabs_Ropp; rewrite Rabs_right.

2058

apply Rle_lt_trans with (0+powerRZ radix (1- dExp b))%R; auto with real.

2059

apply Rplus_lt_compat_r.

2060

apply Rle_lt_trans with (/2*0)%R; auto with real.

2061

apply Rmult_lt_compat_l; auto with real zarith.

2062

apply Rle_ge; apply Rle_trans with (0+0)%R; auto with real.

2063

apply Rplus_le_compat; try apply Rmult_le_pos; auto with real zarith.

2064

rewrite H8; rewrite Rabs_Ropp; rewrite Rabs_right.

2065

2: apply Rle_ge; auto with real zarith.

2066

rewrite FPredSimpl2 with b radix prec c; auto with zarith.

2067

rewrite FPredSimpl4;auto with zarith.

2068

simpl (Fnum (Float (pPred (vNum b)) (Zpred (Fexp c)))).

2069

simpl (Fexp (Float (pPred (vNum b)) (Zpred (Fexp c)))).

2070

replace (FtoR radix (Float (Zpred (pPred (vNum b))) (Zpred (Fexp c)))) with

2071

(c-powerRZ radix (Fexp c))%R.

2072

replace (c - / 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b) -

2073

(c - powerRZ radix (Fexp c)))%R with

2074

(/ 2 * powerRZ radix (Fexp c) - powerRZ radix (1- dExp b))%R by field.

2075

rewrite Rabs_right.

2076

apply Rplus_lt_reg_r with (powerRZ radix (1- dExp b)); ring_simplify.

2077

apply Rle_lt_trans with (powerRZ radix (1+(1- dExp b))).

2078

rewrite powerRZ_add; auto with real zarith.

2079

rewrite H; simpl; right; ring.

2080

apply Rlt_le_trans with (powerRZ radix (Fexp c-1)).

2081

apply Rlt_powerRZ; auto with real zarith.

2082

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2083

rewrite H; simpl; right; field.

2084

apply Rle_ge; apply Rplus_le_reg_l with (powerRZ radix (1- dExp b)); ring_simplify.

2085

apply Rle_trans with (powerRZ radix (Fexp c-1)).

2086

apply Rle_powerRZ; auto with real zarith.

2087

unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

2088

rewrite H; simpl; right; field.

2089

unfold FtoRradix, FtoR; simpl.

2090

rewrite H3; unfold pPred; rewrite pGivesBound.

2091

unfold nNormMin, Zpred; repeat rewrite plus_IZR.

2092

repeat rewrite Zpower_nat_Z_powerRZ; simpl.

2093

rewrite inj_pred; auto with zarith; unfold Zpred.

2094

repeat rewrite powerRZ_add; auto with real zarith.

2095

rewrite H; simpl; field.

2096

simpl; assert (0 < pPred (vNum b))%Z; auto with zarith.

2097

apply pPredMoreThanOne with radix prec; auto with zarith.

2098

simpl; assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.

2099

apply nNormMimLtvNum; auto with zarith.

2100

unfold Rminus; rewrite Rplus_assoc; apply Rplus_le_compat_l.

2101

apply Rle_trans with (-(/ 2 * powerRZ radix (Fexp c)

2102

+powerRZ radix (1- dExp b)))%R;[right; ring|idtac].

2103

apply Ropp_le_contravar.

2104

assert (/ 2 * powerRZ radix (Fexp c) + powerRZ radix (1 - dExp b)

2105

= Float (Zpower_nat radix (pred (pred prec)) +2) (-dExp b))%R.

2106

unfold FtoRradix, FtoR.

2107

simpl (Fnum (Float (Zpower_nat radix (pred (pred prec)) + 2) (- dExp b))).

2108

simpl (Fexp (Float (Zpower_nat radix (pred (pred prec)) + 2) (- dExp b))).

2109

rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite I'.

2110

repeat rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.

2111

repeat rewrite powerRZ_add; auto with real zarith.

2112

rewrite H; simpl; field.

2113

rewrite H9; apply RleBoundRoundr with b prec (Closest b radix) (c'+eta)%R; auto with zarith.

2114

apply ClosestRoundedModeP with prec; auto with zarith.

2115

split; simpl; auto with zarith.

2116

rewrite Zabs_eq; auto with zarith.

2117

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix (pred prec+1)); auto with zarith.

2118

apply Zlt_le_trans with (Zpower_nat radix (pred prec)+Zpower_nat radix (pred prec))%Z; auto with zarith.

2119

apply Zplus_lt_compat; auto with zarith.

2120

replace 2%Z with (Zpower_nat radix 1); auto with zarith.

2121

rewrite H; simpl; auto.

2122

rewrite Zpower_nat_is_exp; auto with zarith; rewrite H.

2123

replace (Zpower_nat 2 1) with 2%Z; auto with zarith.

2124

fold FtoRradix; rewrite <- H9.

2125

apply Rle_trans with ( (/2 * powerRZ radix (Fexp c)

2126

+powerRZ radix (- dExp b))+powerRZ radix (- dExp b))%R.

2127

unfold eta; apply Rplus_le_compat_r.

2128

2: unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2129

2: rewrite H; simpl; right; ring.

2130

clear H8 H9.

2131

assert ( /2 * powerRZ radix (Fexp c) + powerRZ radix (- dExp b)

2132

= Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))%R.

2133

unfold FtoRradix, FtoR.

2134

simpl (Fnum (Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))).

2135

simpl (Fexp (Float (Zpower_nat radix (pred (pred prec)) + 1) (- dExp b))).

2136

rewrite plus_IZR; rewrite Zpower_nat_Z_powerRZ; rewrite I'.

2137

repeat rewrite inj_pred; auto with zarith; unfold Zpred, Zminus.

2138

repeat rewrite powerRZ_add; auto with real zarith.

2139

rewrite H; simpl; field.

2140

rewrite H8.

2141

apply RleBoundRoundr with b prec (Closest b radix) (phi*c)%R; auto with zarith.

2142

apply ClosestRoundedModeP with prec; auto with zarith.

2143

split; simpl; auto with zarith.

2144

rewrite Zabs_eq; auto with zarith.

2145

rewrite pGivesBound.

2146

apply Zle_lt_trans with (Zpower_nat radix (pred prec)+1)%Z.

2147

apply Zplus_le_compat_r.

2148

apply Zpower_nat_monotone_le; auto with zarith.

2149

apply Zlt_le_trans with (Zpower_nat radix (pred prec) +Zpower_nat radix (pred prec))%Z.

2150

apply Zplus_lt_compat_l.

2151

apply Zle_lt_trans with (Zpower_nat radix 0); auto with zarith.

2152

pattern prec at 3; replace prec with (pred prec +1); auto with zarith.

2153

rewrite Zpower_nat_is_exp; rewrite H; simpl; auto with zarith.

2154

unfold Zpower_nat at 4; simpl; auto with zarith.

2155

fold FtoRradix; rewrite <- H8.

2156

unfold phi,u, FtoRradix, FtoR; simpl.

2157

rewrite H3; rewrite I'; unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

2158

replace radixH with 1%Z; auto with zarith.

2159

apply Rle_trans with

2160

(powerRZ radix (- prec)*powerRZ radix (pred prec) * powerRZ radix (- dExp b + prec - 1)

2161

+ radix*(powerRZ radix (- prec)*powerRZ radix (- prec)

2162

*powerRZ radix (pred prec) * powerRZ radix (- dExp b + prec - 1)))%R;[simpl; right; ring|idtac].

2163

repeat rewrite <- powerRZ_add; auto with real zarith.

2164

apply Rplus_le_compat.

2165

apply Rle_trans with (powerRZ radix (-1+((- dExp b + prec - 1)))).

2166

apply Rle_powerRZ; auto with real zarith.

2167

rewrite inj_pred; auto with zarith; unfold Zpred; auto with zarith.

2168

rewrite powerRZ_add; auto with real zarith.

2169

rewrite H; simpl; right; field.

2170

pattern (IZR radix) at 1; replace (IZR radix) with (powerRZ radix 1); auto with real zarith.

2171

rewrite <- powerRZ_add; auto with real zarith.

2172

apply Rle_powerRZ; auto with real zarith.

2173

rewrite inj_pred; auto with zarith; unfold Zpred; auto with zarith.

2174

(* the one problematic float *)

2175

assert (FtoRradix c=powerRZ radix (6-dExp b))%R.

2176

unfold FtoRradix, FtoR; rewrite H3; rewrite I'.

2177

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add; auto with real zarith.

2178

replace (pred prec + (- dExp b + prec - 1))%Z with (6 - dExp b)%Z; auto.

2179

replace prec with 4%nat; auto with zarith.

2180

simpl (pred 4); simpl (Z_of_nat 4); simpl (Z_of_nat 3); auto with zarith.

2181

assert (FtoRradix (Float 4 (-dExp b)) = 4*powerRZ radix (-dExp b))%R.

2182

unfold FtoRradix, FtoR; simpl; ring.

2183

assert (EvenClosest b radix prec (phi * c) c' -> FtoRradix c'=Float 4 (-dExp b))%R.

2184

intros; generalize EvenClosestUniqueP; unfold UniqueP; intros T.

2185

unfold FtoRradix; apply T with b prec (phi*c)%R; auto with zarith; clear T.

2186

assert (Fcanonic radix b (Float 4 (- dExp b))).

2187

right; repeat split; simpl; auto with zarith.

2188

rewrite pGivesBound; replace 4%Z with (Zpower_nat radix 2); auto with zarith.

2189

unfold Zpower_nat; rewrite H; simpl; auto with zarith.

2190

rewrite pGivesBound; rewrite H.

2191

rewrite Zabs_eq; auto with zarith.

2192

replace (2*4)%Z with (Zpower_nat 2 3); auto with zarith.

2193

assert (phi * c - FtoR radix (Float 4 (- dExp b)) = powerRZ radix (-1-dExp b))%R.

2194

rewrite H8; unfold phi,u.

2195

replace radixH with 1%Z; auto with zarith.

2196

fold FtoRradix; rewrite H9.

2197

rewrite Rmult_plus_distr_l; rewrite Rmult_plus_distr_r.

2198

replace (powerRZ radix (- prec) * 1%Z)%R with (powerRZ radix (- prec));

2199

[idtac|simpl; ring].

2200

pattern (IZR radix) at 4; replace (IZR radix) with (powerRZ radix 1); auto with real.

2201

repeat rewrite <- powerRZ_add; auto with real zarith.

2202

replace (- prec + (6 - dExp b))%Z with (2-dExp b)%Z; auto with zarith.

2203

replace (- prec + (1 + - prec) + (6 - dExp b))%Z with (-1-dExp b)%Z; auto with zarith.

2204

replace (powerRZ radix (2 - dExp b)) with (4 * powerRZ radix (- dExp b))%R;[ring|idtac].

2205

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2206

rewrite H; simpl; ring.

2207

split.

2208

apply ClosestSuccPred with prec; auto with zarith.

2209

apply FcanonicBound with radix; auto with zarith.

2210

rewrite H12.

2211

rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].

2212

rewrite succNormal; auto with zarith.

2213

replace ((phi * c -

2214

(Float 4 (- dExp b) + powerRZ radix (Fexp (Float 4 (- dExp b))))))%R with

2215

((phi * c - FtoR radix (Float 4 (- dExp b))) -

2216

powerRZ radix (Fexp (Float 4 (- dExp b))))%R;[rewrite H12|unfold FtoRradix; ring].

2217

simpl (Fexp (Float 4 (- dExp b))).

2218

replace (powerRZ radix (-1 - dExp b) - powerRZ radix (- dExp b))%R with

2219

(-powerRZ radix (-1 - dExp b))%R.

2220

rewrite Rabs_Ropp; rewrite Rabs_right; [idtac|apply Rle_ge]; auto with real zarith.

2221

unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

2222

rewrite H; simpl; field.

2223

rewrite H9; repeat apply Rmult_le_pos; auto with real zarith.

2224

rewrite H12.

2225

rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].

2226

rewrite predSmallOnes; auto.

2227

replace ((phi * c - (Float 4 (- dExp b) -eta )))%R with

2228

((phi * c - FtoR radix (Float 4 (- dExp b))) + eta)%R;[rewrite H12|unfold FtoRradix; ring].

2229

unfold eta; rewrite Rabs_right.

2230

apply Rle_trans with (powerRZ radix (-1 - dExp b)+0)%R; auto with real zarith.

2231

apply Rle_ge; apply Rle_trans with (0+0)%R; try apply Rplus_le_compat; auto with real zarith.

2232

replace (FtoRradix (Float 4 (- dExp b))) with (powerRZ radix (2-dExp b)).

2233

rewrite Rabs_right; try apply Rle_ge; auto with real zarith.

2234

rewrite H9; unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2235

rewrite H; simpl; ring.

2236

left; unfold FNeven.

2237

rewrite FcanonicFnormalizeEq; auto with zarith.

2238

unfold Feven; simpl; unfold Even.

2239

exists 2%Z; auto with zarith.

2240

assert (FtoRradix c' = Float 4 (- dExp b) -> (FPred b radix prec c <= cinf)%R).

2241

intros.

2242

assert (FtoRradix(Float 5 (- dExp b)) = (5 * powerRZ radix (- dExp b)))%R.

2243

unfold FtoRradix, FtoR; simpl; ring.

2244

assert (FtoRradix e=Float 5 (- dExp b)).

2245

apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

2246

apply ClosestRoundedModeP with prec; auto with zarith.

2247

split; simpl; auto with zarith.

2248

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.

2249

rewrite H; unfold Zpower_nat; simpl; auto with zarith.

2250

replace (FtoR radix (Float 5 (- dExp b))) with (c'+eta)%R; auto.

2251

fold FtoRradix; rewrite H12; rewrite H11; rewrite H9; unfold eta; ring.

2252

assert (FPred b radix prec c= Float (pPred (vNum b)) (- dExp b +2)).

2253

rewrite FPredSimpl2; auto with zarith.

2254

replace ((Zpred (Fexp c))) with (-dExp b+2)%Z; auto.

2255

rewrite I'; unfold Zpred; rewrite <- precBis; ring.

2256

assert (c - e - FtoR radix (FPred b radix prec c)=

2257

-powerRZ radix (- dExp b))%R.

2258

rewrite predNormal1; auto with zarith.

2259

rewrite H13; rewrite H12; rewrite I'.

2260

replace (powerRZ radix (- dExp b + prec - 1 - 1)) with

2261

(4* powerRZ radix (- dExp b))%R;[ring|idtac].

2262

replace (-dExp b +prec-1-1)%Z with (-dExp b+2)%Z; auto with zarith.

2263

rewrite powerRZ_add; auto with real zarith.

2264

rewrite H; simpl; ring.

2265

rewrite H8; auto with real zarith.

2266

right; apply sym_eq; apply ClosestStrictEq with b prec (c-e)%R; auto with zarith.

2267

apply FPredCanonic; auto with zarith.

2268

rewrite H15; rewrite Rabs_Ropp.

2269

rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].

2270

rewrite FSucPred; auto with zarith.

2271

fold FtoRradix; replace (c-e-c)%R with (-e)%R by ring.

2272

rewrite H13; rewrite H12; rewrite Rabs_Ropp.

2273

rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

2274

apply Rle_lt_trans with (1*powerRZ radix (- dExp b))%R; auto with real.

2275

apply Rmult_lt_compat_r; auto with real zarith.

2276

replace 5%R with (IZR 5); auto with real zarith; simpl; ring.

2277

replace 5%R with (IZR 5); auto with real zarith; simpl; ring.

2278

rewrite H15; rewrite Rabs_Ropp.

2279

rewrite Rabs_right; [idtac|apply Rle_ge; auto with real zarith].

2280

rewrite H14; rewrite FPredSimpl4; auto with zarith; simpl.

2281

replace (FtoR radix (Float (Zpred (pPred (vNum b))) (- dExp b + 2))) with

2282

(c-8*powerRZ radix (- dExp b))%R.

2283

2: unfold pPred, Zpred; rewrite pGivesBound.

2284

2: unfold FtoR; simpl.

2285

2: repeat rewrite plus_IZR; simpl; rewrite Zpower_nat_Z_powerRZ.

2286

2: repeat rewrite Rmult_plus_distr_r with (r3:=powerRZ radix (- dExp b + 2)).

2287

2: rewrite <- powerRZ_add; auto with real zarith; rewrite H8.

2288

2: replace (prec + (- dExp b + 2))%Z with (6 - dExp b)%Z; auto with zarith.

2289

2: repeat rewrite powerRZ_add with (m:=2); auto with real zarith.

2290

2: rewrite H; simpl; ring.

2291

replace (c - e - (c - 8 * powerRZ radix (- dExp b)))%R with ((3*powerRZ radix (- dExp b)))%R.

2292

rewrite Rabs_right; try apply Rle_ge; auto with real zarith.

2293

apply Rle_lt_trans with (1*powerRZ radix (- dExp b))%R; auto with real.

2294

apply Rmult_lt_compat_r; auto with real zarith.

2295

replace 3%R with (IZR 3); auto with real zarith; simpl; ring.

2296

apply Rmult_le_pos; auto with real zarith.

2297

replace 3%R with (IZR 3); auto with real zarith; simpl; ring.

2298

rewrite H13; rewrite H12; ring.

2299

assert (0 < pPred (vNum b))%Z; auto with zarith.

2300

apply pPredMoreThanOne with radix prec; auto with zarith.

2301

assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.

2302

apply nNormMimLtvNum; auto with zarith.

2303

case MM; auto with zarith.

2304

intros.

2305

assert (phi*c=9/2*powerRZ radix (-dExp b))%R.

2306

rewrite H8; unfold phi,u; rewrite <- precBis.

2307

replace (radixH) with 1%Z; auto with zarith.

2308

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2309

rewrite H; simpl; field.

2310

assert (FtoRradix (Float 5 (- dExp b)) = 5 * powerRZ radix (- dExp b))%R.

2311

unfold FtoRradix, FtoR; simpl; ring.

2312

assert (Fcanonic radix b (Float 4 (- dExp b))).

2313

right; split; split; simpl; auto with zarith.

2314

rewrite pGivesBound; rewrite H.

2315

replace prec with 4%nat; auto with zarith.

2316

rewrite pGivesBound; rewrite H.

2317

replace prec with 4%nat; auto with zarith.

2318

assert (Fcanonic radix b (Float 5 (- dExp b))).

2319

right; split; split; simpl; auto with zarith.

2320

rewrite pGivesBound; rewrite H.

2321

replace prec with 4%nat; auto with zarith.

2322

rewrite pGivesBound; rewrite H.

2323

replace prec with 4%nat; auto with zarith.

2324

assert (FtoRradix c'= Float 4 (- dExp b) \/ FtoRradix c'= Float 5 (- dExp b))%R.

2325

generalize ClosestMinOrMax; unfold MinOrMaxP; intros T.

2326

case (T b radix (phi*c)%R c'); auto; clear T.

2327

intros; left.

2328

apply (MinUniqueP b radix (phi*c)%R); auto.

2329

split; auto.

2330

apply FcanonicBound with radix; auto.

2331

split.

2332

fold FtoRradix; rewrite H9; rewrite H13.

2333

apply Rmult_le_compat_r; auto with real zarith.

2334

apply Rmult_le_reg_l with 2%R; auto with real.

2335

apply Rle_trans with 9%R;[auto with real|right; field].

2336

apply Rle_trans with (8+1)%R; auto with real.

2337

intros.

2338

apply Rle_trans with (FtoR radix (FPred b radix prec (Float 5 (- dExp b)))).

2339

rewrite <- FnormalizeCorrect with radix b prec f; auto.

2340

apply FPredProp; auto with zarith.

2341

apply FnormalizeCanonic; auto with zarith.

2342

rewrite FnormalizeCorrect; auto with zarith.

2343

apply Rle_lt_trans with (1:=H19).

2344

fold FtoRradix; rewrite H14; rewrite H13.

2345

apply Rmult_lt_compat_r; auto with real zarith.

2346

apply Rmult_lt_reg_l with 2%R; auto with real.

2347

apply Rle_lt_trans with 9%R;[right; field|idtac].

2348

apply Rlt_le_trans with (9+1)%R; auto with real.

2349

right; ring.

2350

rewrite predSmallOnes; auto with zarith.

2351

fold FtoRradix; rewrite H14; rewrite H9.

2352

unfold eta; right; ring.

2353

rewrite H14; rewrite Rabs_right.

2354

unfold Zminus; rewrite powerRZ_add; auto with real zarith.

2355

apply Rmult_lt_compat_r; auto with real zarith.

2356

rewrite H; rewrite <- precBis; simpl.

2357

apply Rlt_le_trans with (IZR 16); auto with real zarith.

2358

apply Rle_lt_trans with (IZR 5); auto with real zarith.

2359

right; simpl; ring.

2360

right; simpl; ring.

2361

apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

2362

apply Rle_trans with (IZR 5); auto with real zarith; right; simpl; ring.

2363

intros; right.

2364

apply (MaxUniqueP b radix (phi*c)%R); auto.

2365

split; auto.

2366

apply FcanonicBound with radix; auto.

2367

split.

2368

fold FtoRradix; rewrite H14; rewrite H13.

2369

apply Rmult_le_compat_r; auto with real zarith.

2370

apply Rmult_le_reg_l with 2%R; auto with real.

2371

apply Rle_trans with 9%R;[right; field|idtac].

2372

apply Rle_trans with (9+1)%R; auto with real.

2373

right; ring.

2374

intros.

2375

apply Rle_trans with (FtoR radix (FSucc b radix prec (Float 4 (- dExp b)))).

2376

rewrite succNormal; auto with zarith.

2377

fold FtoRradix; rewrite H9; rewrite H14; simpl; right; ring.

2378

rewrite H9; repeat apply Rmult_le_pos; auto with real zarith.

2379

rewrite <- FnormalizeCorrect with radix b prec f; auto.

2380

apply FSuccProp; auto with zarith.

2381

apply FnormalizeCanonic; auto with zarith.

2382

rewrite FnormalizeCorrect; auto with zarith.

2383

apply Rlt_le_trans with (2:=H19).

2384

fold FtoRradix; rewrite H9; rewrite H13.

2385

apply Rmult_lt_compat_r; auto with real zarith.

2386

apply Rmult_lt_reg_l with 2%R; auto with real.

2387

apply Rlt_le_trans with 9%R;[idtac|right; field].

2388

apply Rlt_le_trans with (8+1)%R; auto with real.

2389

case H17; auto.

2390

intros.

2391

assert (FtoRradix e=Float 6 (- dExp b)).

2392

apply sym_eq; apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

2393

apply ClosestRoundedModeP with prec; auto with zarith.

2394

split; simpl; auto with zarith.

2395

rewrite pGivesBound; apply Zlt_le_trans with (Zpower_nat radix 3); auto with zarith.

2396

rewrite H; unfold Zpower_nat; simpl; auto with zarith.

2397

replace (FtoR radix (Float 6 (- dExp b))) with (c'+eta)%R; auto.

2398

rewrite H18; unfold FtoRradix, FtoR; unfold eta; simpl; ring.

2399

assert (FPred b radix prec c= Float (pPred (vNum b)) (- dExp b +2)).

2400

rewrite FPredSimpl2; auto with zarith.

2401

replace ((Zpred (Fexp c))) with (-dExp b+2)%Z; auto.

2402

rewrite I'; unfold Zpred; rewrite <- precBis; ring.

2403

assert (FtoRradix (Float 6 (- dExp b)) = (6 * powerRZ radix (- dExp b))%R).

2404

unfold FtoRradix, FtoR; simpl; ring.

2405

assert (c - e - FtoR radix (FPred b radix prec c)=

2406

-(2* powerRZ radix (- dExp b)))%R.

2407

rewrite predNormal1; auto with zarith.

2408

rewrite H19; rewrite H21; rewrite I'.

2409

replace (powerRZ radix (- dExp b + prec - 1 - 1)) with

2410

(4* powerRZ radix (- dExp b))%R;[ring|idtac].

2411

replace (-dExp b +prec-1-1)%Z with (-dExp b+2)%Z; auto with zarith.

2412

rewrite powerRZ_add; auto with real zarith.

2413

rewrite H; simpl; ring.

2414

rewrite H8; auto with real zarith.

2415

generalize AFZClosestUniqueP; unfold UniqueP; intros T.

2416

right; unfold FtoRradix; apply T with b prec (c-e)%R; auto with zarith.

2417

clear T; split.

2418

apply ClosestSuccPred with prec; auto with zarith.

2419

apply FBoundedPred; auto with zarith.

2420

apply FcanonicBound with radix; auto.

2421

apply FPredCanonic; auto with zarith.

2422

rewrite H22; rewrite Rabs_Ropp.

2423

rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

2424

rewrite FSucPred; auto with zarith.

2425

fold FtoRradix; replace (c-e-c)%R with (-e)%R by ring.

2426

rewrite H19; rewrite H21; rewrite Rabs_Ropp.

2427

rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

2428

apply Rmult_le_compat_r; auto with real zarith.

2429

replace 6%R with (IZR 6); auto with real zarith.

2430

replace 2%R with (IZR 2); auto with real zarith.

2431

simpl; ring.

2432

replace 6%R with (IZR 6); auto with real zarith; simpl; ring.

2433

rewrite H22; rewrite Rabs_Ropp.

2434

rewrite Rabs_right; [idtac|apply Rle_ge; apply Rmult_le_pos; auto with real zarith].

2435

rewrite H20; rewrite FPredSimpl4; auto with zarith; simpl.

2436

replace (FtoR radix (Float (Zpred (pPred (vNum b))) (- dExp b + 2))) with

2437

(c-8*powerRZ radix (- dExp b))%R.

2438

2: unfold pPred, Zpred; rewrite pGivesBound.

2439

2: unfold FtoR; simpl.

2440

2: repeat rewrite plus_IZR; simpl; rewrite Zpower_nat_Z_powerRZ.

2441

2: repeat rewrite Rmult_plus_distr_r with (r3:=powerRZ radix (- dExp b + 2)).

2442

2: rewrite <- powerRZ_add; auto with real zarith; rewrite H8.

2443

2: replace (prec + (- dExp b + 2))%Z with (6 - dExp b)%Z; auto with zarith.

2444

2: repeat rewrite powerRZ_add with (m:=2); auto with real zarith.

2445

2: rewrite H; simpl; ring.

2446

replace (c - e - (c - 8 * powerRZ radix (- dExp b)))%R with ((2*powerRZ radix (- dExp b)))%R.

2447

rewrite Rabs_right; auto with real; try apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

2448

rewrite H19; rewrite H21; ring.

2449

assert (0 < pPred (vNum b))%Z; auto with zarith.

2450

apply pPredMoreThanOne with radix prec; auto with zarith.

2451

assert (nNormMin radix prec < pPred (vNum b))%Z; auto with zarith.

2452

apply nNormMimLtvNum; auto with zarith.

2453

left; repeat rewrite Rabs_right; try apply Rle_ge.

2454

apply Rminus_le; rewrite H22.

2455

apply Rle_trans with (-0)%R; auto with real; apply Ropp_le_contravar.

2456

apply Rmult_le_pos;auto with real zarith.

2457

rewrite H20; apply LeFnumZERO; simpl; auto with zarith.

2458

assert (0 < pPred (vNum b))%Z; auto with zarith.

2459

apply pPredMoreThanOne with radix prec; auto with zarith.

2460

apply Rplus_le_reg_l with e; ring_simplify.

2461

rewrite H19; rewrite H21; rewrite H8; unfold Zminus.

2462

rewrite powerRZ_add; auto with real zarith.

2463

apply Rmult_le_compat_r; auto with real zarith.

2464

apply Rle_trans with (powerRZ radix 3); auto with real zarith.

2465

rewrite H; simpl; apply Rle_trans with (IZR 6).

2466

right; simpl; ring.

2467

apply Rle_trans with (IZR 8); auto with real zarith.

2468

right; simpl; ring.

2469

Qed.

2470

2471

2472

2473

Lemma Algo1_correct_r2_aux_aux4:forall (c csup:float) (r:R),

2474

Fcanonic radix b c -> (0 <= c)%R ->

2475

(r <= 5/4*powerRZ radix (Fexp c))%R ->

2476

Closest b radix (c+r) csup ->

2477

(FtoRradix csup <= FSucc b radix prec c)%R.

2478

intros c csup r; intros.

2479

assert (N:Fbounded b c).

2480

apply FcanonicBound with radix; auto.

2481

assert (G1:(0 < 4)%R).

2482

apply Rlt_le_trans with (IZR 4); auto with real zarith; simpl; right; ring.

2483

assert (G2:(0 < 5)%R).

2484

apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.

2485

assert (c + 5 / 4 * powerRZ radix (Fexp c) - FtoR radix (FSucc b radix prec c)

2486

= (/4*powerRZ radix (Fexp c)))%R.

2487

rewrite succNormal; auto with zarith; field.

2488

apply ClosestStrictMonotone2r with b prec (c+r)%R (c+5/4*powerRZ radix (Fexp c))%R; auto with zarith.

2489

apply FSuccCanonic; auto with zarith.

2490

rewrite H3.

2491

rewrite Rabs_right.

2492

2: apply Rle_ge; unfold Rdiv; apply Rmult_le_pos; auto with real zarith.

2493

rewrite succNormal; auto with zarith.

2494

rewrite succNormal; auto with zarith.

2495

replace (c + 5/4*powerRZ radix (Fexp c) -

2496

(c + powerRZ radix (Fexp c) +

2497

powerRZ radix (Fexp (FSucc b radix prec c))))%R with

2498

((/4*powerRZ radix (Fexp c)-powerRZ radix

2499

(Fexp (FSucc b radix prec c))))%R.

2500

2: field.

2501

assert (Fexp (FSucc b radix prec c) = Fexp c \/

2502

(Fexp (FSucc b radix prec c) = Fexp c+1)%Z).

2503

unfold FSucc.

2504

case (Z_eq_bool (Fnum c) (pPred (vNum b))).

2505

right; simpl; unfold Zsucc; auto.

2506

generalize (Z_eq_bool_correct (Fnum c) (- nNormMin radix prec));

2507

case (Z_eq_bool (Fnum c) (- nNormMin radix prec)).

2508

intros; absurd (0 <= Fnum c)%Z.

2509

apply Zlt_not_le; apply Zlt_le_trans with (-0)%Z; auto with zarith.

2510

rewrite H4; unfold nNormMin; auto with zarith.

2511

apply LeR0Fnum with radix ; auto with real zarith.

2512

intros; left; simpl; auto.

2513

case H4; intros M; rewrite M.

2514

replace (/ 4 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c))%R with

2515

(-(3/4*powerRZ radix (Fexp c) ))%R by field.

2516

rewrite Rabs_Ropp; rewrite Rabs_right.

2517

apply Rmult_lt_compat_r; auto with real zarith.

2518

apply Rle_lt_trans with (1*/4)%R; unfold Rdiv; auto with real.

2519

apply Rmult_lt_compat_r; auto with real.

2520

apply Rlt_le_trans with (IZR 3); auto with real zarith; simpl; right; ring.

2521

apply Rle_ge; unfold Rdiv; repeat apply Rmult_le_pos; auto with real zarith.

2522

apply Rle_trans with (IZR 3); auto with real zarith; simpl; right; ring.

2523

replace (/ 4 * powerRZ radix (Fexp c) - powerRZ radix (Fexp c+1))%R with

2524

(-((radix-/4)*powerRZ radix (Fexp c) ))%R.

2525

2: rewrite powerRZ_add; auto with real zarith; simpl; field.

2526

rewrite Rabs_Ropp; rewrite Rabs_right.

2527

apply Rmult_lt_compat_r; auto with real zarith.

2528

apply Rle_lt_trans with (1*/4)%R; unfold Rdiv; auto with real.

2529

apply Rlt_le_trans with ((4*radix-1)*/4)%R;[idtac|right; field].

2530

apply Rmult_lt_compat_r; auto with real.

2531

apply Rplus_lt_reg_r with 1%R; ring_simplify.

2532

apply Rlt_le_trans with (4*1)%R; auto with real zarith.

2533

apply Rlt_le_trans with (4)%R; auto with real zarith.

2534

apply Rle_lt_trans with (2*1)%R; auto with real zarith.

2535

apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

2536

apply Rplus_le_reg_l with (/4)%R; ring_simplify.

2537

apply Rle_trans with 1%R; auto with real zarith.

2538

apply Rle_trans with (/1)%R; auto with real.

2539

apply Rle_Rinv; auto with real.

2540

apply Rle_trans with (IZR 4); auto with real zarith; simpl; right; ring.

2541

apply FSuccCanonic; auto with zarith.

2542

apply Rle_trans with (1:=H0).

2543

left; unfold FtoRradix; apply FSuccLt; auto with zarith.

2544

rewrite H3.

2545

rewrite FPredSuc; fold FtoRradix; auto with zarith.

2546

replace (c + 5/4*powerRZ radix (Fexp c) - c)%R with (5/4*(powerRZ radix (Fexp c)))%R;[idtac|ring].

2547

rewrite (Rabs_right (5/4*(powerRZ radix (Fexp c) ))).

2548

2: apply Rle_ge; unfold Rdiv;repeat apply Rmult_le_pos; auto with real zarith.

2549

rewrite Rabs_right.

2550

2: apply Rle_ge; apply Rmult_le_pos; auto with real zarith.

2551

apply Rmult_lt_compat_r; auto with real zarith.

2552

apply Rle_lt_trans with (1*/4)%R; auto with real.

2553

apply Rmult_lt_compat_r; auto with real zarith.

2554

apply Rlt_le_trans with (IZR 5); auto with real zarith; simpl; right; ring.

2555

apply Rplus_le_compat_l; auto.

2556

Qed.

2557

2558

2559

2560

Lemma Algo1_correct_r2_aux1: forall (c c' e cinf csup:float),

2561

(radix=2)%Z ->

2562

Fcanonic radix b c ->

2563

(0 <= c)%R ->

2564

(powerRZ radix (prec+1-dExp b) < c)%R ->

2565

Closest b radix (phi*c) c' ->

2566

Closest b radix (c'+eta) e ->

2567

Closest b radix (c-e) cinf ->

2568

Closest b radix (c+e) csup ->

2569

(prec=4 -> EvenClosest b radix prec (phi*c)%R c'

2570

\/ AFZClosest b radix (c-e) cinf) ->

2571

(FtoRradix (FPred b radix prec c) <= cinf)%R

2572

/\ (FtoRradix csup <= FSucc b radix prec c)%R.

2573

intros c c' e cinf csup K Cc Cpos CGe Hc' He Hcinf Hcsup MM.

2574

assert (- dExp b +2 <= Fexp c )%Z.

2575

apply Zle_trans with (Fexp (Float (nNormMin radix prec) (-dExp b+2))); auto with zarith.

2576

apply Fcanonic_Rle_Zle with radix b prec; auto with zarith.

2577

left; split; try split; simpl; auto with zarith.

2578

unfold nNormMin; rewrite pGivesBound; rewrite Zabs_eq; auto with zarith.

2579

rewrite <- (PosNormMin radix b prec); auto with zarith.

2580

fold (FtoRradix c).

2581

replace (FtoR radix (Float (nNormMin radix prec) (- dExp b + 2))) with

2582

(powerRZ radix (prec + 1 - dExp b)).

2583

repeat rewrite Rabs_right; try apply Rle_ge; auto with real zarith.

2584

unfold FtoR; simpl.

2585

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

2586

rewrite <- powerRZ_add; auto with real zarith.

2587

replace (pred prec + (- dExp b + 2))%Z with (prec+1-dExp b)%Z; auto.

2588

rewrite inj_pred; unfold Zpred; auto with zarith.

2589

assert (e <= 5/4*powerRZ radix (Fexp c))%R.

2590

apply Rle_trans with

2591

(powerRZ radix (Fexp c) * (radix / 2 + powerRZ radix (-2)))%R.

2592

apply eLe with c'; auto with zarith.

2593

rewrite K; simpl; right; field.

2594

split.

2595

2: apply Algo1_correct_r2_aux_aux4 with e; auto.

2596

case (Z_eq_dec (Fnum c) (nNormMin radix prec)); intros L1.

2597

apply Algo1_correct_r2_aux_aux3 with c' e; auto.

2598

case (Zle_lt_or_eq (- dExp b + 2) (Fexp c)); auto with zarith.

2599

intros M.

2600

Contradict CGe.

2601

replace (FtoRradix c) with (powerRZ radix (prec + 1 - dExp b)); auto with real.

2602

unfold FtoRradix, FtoR; simpl; rewrite <- M; rewrite L1.

2603

unfold nNormMin; rewrite Zpower_nat_Z_powerRZ.

2604

rewrite <- powerRZ_add; auto with real zarith.

2605

replace (pred prec + (- dExp b + 2))%Z with (prec+1-dExp b)%Z; auto.

2606

rewrite inj_pred; unfold Zpred; auto with zarith.

2607

case (Z_eq_dec (Fnum c) (nNormMin radix prec+1)); intros L2.

2608

apply Algo1_correct_r2_aux_aux2 with c' e; auto with zarith.

2609

apply Algo1_correct_r2_aux_aux1 with e; auto with zarith.

2610

Qed.

2611

2612

2613

2614

Lemma Algo1_correct_r2_aux2: forall (c c' e cinf csup:float),

2615

(radix=2)%Z ->

2616

Fcanonic radix b c ->

2617

(0 <= c)%R ->

2618

(c < powerRZ radix (prec-dExp b-1))%R ->

2619

Closest b radix (phi*c) c' ->

2620

Closest b radix (c'+eta) e ->

2621

Closest b radix (c-e) cinf ->

2622

Closest b radix (c+e) csup ->

2623

(FtoRradix (FPred b radix prec c) <= cinf)%R

2624

/\ (FtoRradix csup <= FSucc b radix prec c)%R.

2625

intros.

2626

cut (FtoRradix e = eta)%R; [intros P|idtac].

2627

split.

2628

right; unfold FtoRradix.

2629

apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

2630

apply ClosestRoundedModeP with prec; auto with zarith.

2631

apply FBoundedPred; auto with zarith.

2632

apply FcanonicBound with radix; auto.

2633

replace (FtoR radix (FPred b radix prec c))%R with (c-e)%R; auto.

2634

fold FtoRradix; rewrite predSmallOnes; auto.

2635

rewrite P; auto.

2636

rewrite Rabs_right; try apply Rle_ge; auto with real zarith.

2637

apply Rlt_le_trans with (1:=H2); auto with real zarith.

2638

right; unfold FtoRradix; apply sym_eq.

2639

apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

2640

apply ClosestRoundedModeP with prec; auto with zarith.

2641

apply FBoundedSuc; auto with zarith.

2642

apply FcanonicBound with radix; auto.

2643

replace (FtoR radix (FSucc b radix prec c))%R with (c+e)%R; auto.

2644

fold FtoRradix; rewrite succNormal; auto.

2645

rewrite P; unfold eta; replace (Fexp c) with (-dExp b)%Z; auto.

2646

case H0; auto; intros J.

2647

absurd (FtoRradix (firstNormalPos radix b prec) <= c)%R.

2648

apply Rlt_not_le; unfold FtoRradix; rewrite firstNormalPos_eq; auto with zarith.

2649

fold FtoRradix; apply Rlt_le_trans with (1:=H2).

2650

apply Rle_powerRZ; unfold Zpred; auto with real zarith.

2651

apply FnormalLtFirstNormalPos; auto with zarith.

2652

elim J; intuition.

2653

apply sym_eq; apply trans_eq with (Float 1 (-(dExp b))).

2654

unfold eta, FtoRradix, FtoR; simpl; ring.

2655

apply RoundedModeProjectorIdemEq with b prec (Closest b radix); auto with zarith.

2656

apply ClosestRoundedModeP with prec; auto with zarith.

2657

split; simpl; auto with zarith float.

2658

apply vNumbMoreThanOne with radix prec; auto with zarith.

2659

replace (FtoR radix (Float 1 (- dExp b))) with (c'+eta)%R; auto.

2660

replace (FtoRradix c') with 0%R.

2661

unfold eta, FtoRradix, FtoR; simpl; ring.

2662

apply sym_eq; apply RoundedToZero with (phi*c)%R; auto.

2663

rewrite Rabs_mult.

2664

repeat rewrite Rabs_right; try apply Rle_ge; auto with real.

2665

assert (exists f:float, Fbounded b f /\ (f=Float 1 (prec - dExp b-1)) /\

2666

(FtoRradix f= powerRZ radix (prec - dExp b-1))%R).

2667

exists (Float 1 (prec-dExp b-1)).

2668

split; try split; simpl; auto with zarith.

2669

apply vNumbMoreThanOne with radix prec; auto with zarith.

2670

unfold FtoRradix, FtoR; simpl; ring.

2671

elim H7; intros f (Bf,(L2,L3)).

2672

apply Rle_lt_trans with (phi*(FPred b radix prec (Fnormalize radix b prec f)))%R.

2673

apply Rmult_le_compat_l; auto with real.

2674

left; apply phi_Pos.

2675

apply FPredProp; auto with zarith real.

2676

apply FnormalizeCanonic; auto with zarith.

2677

rewrite FnormalizeCorrect; auto with zarith.

2678

fold FtoRradix; rewrite L3; auto.

2679

rewrite predSmallOnes.

2680

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

2681

fold FtoRradix; rewrite L3; unfold eta, phi.

2682

unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

2683

replace radixH with 1%Z; auto with zarith.

2684

apply Rle_lt_trans with ( (u * (1 + radix * u) *

2685

(powerRZ radix prec * powerRZ radix (- (1)) -1 )) * powerRZ radix (-(dExp b)))%R.

2686

simpl; right; ring.

2687

apply Rmult_lt_compat_r; auto with real zarith.

2688

apply Rle_lt_trans with (/radix - powerRZ radix (1-prec-prec))%R.

2689

replace (powerRZ radix prec) with (/powerRZ radix (-prec))%R.

2690

unfold u; right; unfold Zminus; repeat rewrite powerRZ_add; auto with real zarith.

2691

simpl; field; auto with real zarith.

2692

rewrite <- Rinv_powerRZ; auto with real zarith.

2693

apply Rlt_le_trans with (/radix-0)%R; auto with real zarith.

2694

unfold Rminus; apply Rplus_lt_compat_l; auto with real zarith.

2695

apply Rle_trans with (/radix)%R; auto with real zarith.

2696

apply Rle_Rinv; auto with real zarith.

2697

apply Rle_trans with (IZR 2); auto with real zarith.

2698

apply FnormalizeCanonic; auto with zarith.

2699

unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith.

2700

fold FtoRradix; rewrite L3.

2701

rewrite Rabs_right; try apply Rle_ge; auto with real zarith.

2702

left; apply phi_Pos.

2703

Qed.

2704

2705

2706

2707

2708

2709

2710

Lemma Algo1_correct_r2_aux3: forall (c c' e cinf csup:float),

2711

(radix=2)%Z ->

2712

Fcanonic radix b c ->

2713

(Rabs c < powerRZ radix (prec-dExp b-1))%R

2714

\/ (powerRZ radix (prec+1-dExp b) < Rabs c)%R ->

2715

Closest b radix (phi*(Rabs c)) c' ->

2716

Closest b radix (c'+eta) e ->

2717

Closest b radix (c-e) cinf ->

2718

Closest b radix (c+e) csup ->

2719

(prec=4 -> EvenClosest b radix prec (phi*Rabs c)%R c'

2720

\/ (AFZClosest b radix (c-e) cinf

2721

/\ AFZClosest b radix (c+e) csup)) ->

2722

(FtoRradix (FPred b radix prec c) <= cinf)%R

2723

/\ (FtoRradix csup <= FSucc b radix prec c)%R.

2724

intros c c' e cinf csup K Cc CInt Hc' He Hcinf Hcsup MM.

2725

case (Rle_or_lt 0 c); intros.

2726

case CInt; intros.

2727

apply Algo1_correct_r2_aux2 with c' e; auto.

2728

rewrite <- (Rabs_right c); auto.

2729

apply Rle_ge; auto.

2730

rewrite <- (Rabs_right c); auto.

2731

apply Rle_ge; auto.

2732

apply Algo1_correct_r2_aux1 with c' e; auto.

2733

rewrite <- (Rabs_right c); auto.

2734

apply Rle_ge; auto.

2735

rewrite <- (Rabs_right c); auto.

2736

apply Rle_ge; auto.

2737

intros; case MM; auto; intros.

2738

left; rewrite <- (Rabs_right c); auto.

2739

apply Rle_ge; auto.

2740

elim H2; auto.

2741

assert ((FPred b radix prec (Fopp c) <= Fopp csup)%R

2742

/\ (Fopp cinf <= FSucc b radix prec (Fopp c) )%R).

2743

case CInt; intros.

2744

apply Algo1_correct_r2_aux2 with c' e; auto.

2745

apply FcanonicFopp; auto.

2746

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2747

replace (FtoRradix (Fopp c)) with (Rabs c); auto.

2748

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2749

rewrite Rabs_left; auto with real.

2750

replace (FtoRradix (Fopp c)) with (Rabs c); auto.

2751

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2752

rewrite Rabs_left; auto with real.

2753

replace (Fopp c -e)%R with (-(c+e))%R.

2754

apply ClosestOpp; auto.

2755

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

2756

replace (Fopp c +e)%R with (-(c-e))%R.

2757

apply ClosestOpp; auto.

2758

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

2759

apply Algo1_correct_r2_aux1 with c' e; auto.

2760

apply FcanonicFopp; auto.

2761

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2762

replace (FtoRradix (Fopp c)) with (Rabs c); auto.

2763

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2764

rewrite Rabs_left; auto with real.

2765

replace (FtoRradix (Fopp c)) with (Rabs c); auto.

2766

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2767

rewrite Rabs_left; auto with real.

2768

replace (Fopp c -e)%R with (-(c+e))%R.

2769

apply ClosestOpp; auto.

2770

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

2771

replace (Fopp c +e)%R with (-(c-e))%R.

2772

apply ClosestOpp; auto.

2773

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

2774

intros; case MM; auto; intros.

2775

left; replace (FtoRradix (Fopp c)) with (Rabs c); auto.

2776

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2777

rewrite Rabs_left; auto with real.

2778

elim H2; intros.

2779

right; replace (Fopp c -e)%R with (-(c+e))%R.

2780

apply AFZClosestSymmetric; auto.

2781

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith; ring.

2782

elim H0; intros L1 L2; clear H0; split; apply Ropp_le_cancel.

2783

rewrite FPredFopFSucc; auto with zarith.

2784

apply Rle_trans with (FSucc b radix prec (Fopp c)).

2785

apply Rle_trans with (2:=L2).

2786

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2787

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2788

apply Rle_trans with (Fopp csup).

2789

2: unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2790

apply Rle_trans with (2:=L1).

2791

rewrite FPredFopFSucc; auto with zarith.

2792

rewrite Fopp_Fopp.

2793

unfold FtoRradix; rewrite Fopp_correct; auto with real zarith.

2794

Qed.

2795

2796

2797

2798

2799

Lemma PredSucc_Algo1_correct_r2: forall (c c' e cinf csup:float),

2800

(radix=2)%Z ->

2801

Fcanonic radix b c ->

2802

(Rabs c < powerRZ radix (prec-dExp b-1))%R

2803

\/ (powerRZ radix (prec+1-dExp b) < Rabs c)%R ->

2804

Closest b radix (phi*(Rabs c)) c' ->

2805

Closest b radix (c'+eta) e ->

2806

Closest b radix (c-e) cinf ->

2807

Closest b radix (c+e) csup ->

2808

(prec=4 -> EvenClosest b radix prec (phi*Rabs c)%R c'

2809

\/ (AFZClosest b radix (c-e) cinf

2810

/\ AFZClosest b radix (c+e) csup)) ->

2811

(FtoRradix (FPred b radix prec c) = cinf)%R

2812

/\ (FtoRradix csup = FSucc b radix prec c)%R.

2813

intros.

2814

assert ((FtoRradix (FPred b radix prec c) <= cinf)%R

2815

/\ (FtoRradix csup <= FSucc b radix prec c)%R).

2816

apply Algo1_correct_r2_aux3 with c' e; auto.

2817

assert ((FtoRradix cinf<= (FPred b radix prec c))%R

2818

/\ (FtoRradix (FSucc b radix prec c) <= csup)%R).

2819

apply PredSucc_Algo1_correct with c' e; auto.

2820

elim H7; elim H8; intros; split; auto with real.

2821

Qed.

2822

2823

End PredComput.