1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** * HexadecimalQ
Proofs that conversions between hexadecimal numbers and [Q]
are bijections. *)
Require Import Decimal DecimalFacts DecimalPos DecimalN DecimalZ.
Require Import Hexadecimal HexadecimalFacts HexadecimalPos HexadecimalN HexadecimalZ QArith.
Lemma of_IQmake_to_hexadecimal num den :
match IQmake_to_hexadecimal num den with
| None => True
| Some (HexadecimalExp _ _ _) => False
| Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake (IZ_of_Z num) den
end.
Proof.
unfold IQmake_to_hexadecimal.
generalize (Unsigned.nztail_to_hex_uint den).
case Hexadecimal.nztail; intros den' e_den'.
case den'; [now simpl|now simpl| |now simpl..]; clear den'; intro den'.
case den'; [ |now simpl..]; clear den'.
case e_den' as [|e_den']; simpl; injection 1 as ->.
{ now unfold of_hexadecimal; simpl; rewrite app_int_nil_r, HexadecimalZ.of_to. }
replace (16 ^ _)%positive with (Nat.iter (S e_den') (Pos.mul 16) 1%positive).
2:{ induction e_den' as [|n IHn]; [now simpl| ].
now rewrite SuccNat2Pos.inj_succ, Pos.pow_succ_r, <-IHn. }
case Nat.ltb_spec; intro He_den'.
- unfold of_hexadecimal; simpl.
rewrite app_int_del_tail_head; [|now apply Nat.lt_le_incl].
rewrite HexadecimalZ.of_to.
now rewrite nb_digits_del_head_sub; [|now apply Nat.lt_le_incl].
- unfold of_hexadecimal; simpl.
rewrite nb_digits_iter_D0.
apply f_equal2.
+ apply f_equal, HexadecimalZ.to_int_inj.
rewrite HexadecimalZ.to_of.
rewrite <-(HexadecimalZ.of_to num), HexadecimalZ.to_of.
case (Z.to_hex_int num); clear He_den' num; intro num; simpl.
* unfold app; simpl.
now rewrite unorm_D0, unorm_iter_D0, unorm_involutive.
* case (uint_eq_dec (nzhead num) Nil); [|intro Hn].
{ intros->; simpl; unfold app; simpl.
now rewrite unorm_D0, unorm_iter_D0. }
replace (match nzhead num with Nil => _ | _ => _ end)
with (Neg (nzhead num)); [|now revert Hn; case nzhead].
simpl.
rewrite nzhead_iter_D0, nzhead_involutive.
now revert Hn; case nzhead.
+ revert He_den'; case nb_digits as [|n]; [now simpl; rewrite Nat.add_0_r|].
intro Hn.
rewrite Nat.add_succ_r, Nat.sub_add; [|apply le_S_n]; auto.
Qed.
Lemma IZ_of_Z_IZ_to_Z z z' : IZ_to_Z z = Some z' -> IZ_of_Z z' = z.
Proof. now case z as [| |p|p]; [| injection 1 as <- ..]. Qed.
Lemma of_IQmake_to_hexadecimal' num den :
match IQmake_to_hexadecimal' num den with
| None => True
| Some (HexadecimalExp _ _ _) => False
| Some (Hexadecimal i f) => of_hexadecimal (Hexadecimal i f) = IQmake num den
end.
Proof.
unfold IQmake_to_hexadecimal'.
case_eq (IZ_to_Z num); [intros num' Hnum'|now simpl].
generalize (of_IQmake_to_hexadecimal num' den).
case IQmake_to_hexadecimal as [d|]; [|now simpl].
case d as [i f|]; [|now simpl].
now rewrite (IZ_of_Z_IZ_to_Z _ _ Hnum').
Qed.
Lemma of_to (q:IQ) : forall d, to_hexadecimal q = Some d -> of_hexadecimal d = q.
Proof.
intro d.
case q as [num den|q q'|q q']; simpl.
- generalize (of_IQmake_to_hexadecimal' num den).
case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
case d' as [i f|]; [|now simpl].
now intros H; injection 1 as <-.
- case q as [num den| |]; [|now simpl..].
case q' as [num' den'| |]; [|now simpl..].
case num' as [z p| | |]; [|now simpl..].
case (Z.eq_dec z 2); [intros->|].
2:{ case z; [now simpl| |now simpl]; intro pz'.
case pz'; [intros d0..| ]; [now simpl| |now simpl].
now case d0. }
case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
generalize (of_IQmake_to_hexadecimal' num den).
case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
case d' as [i f|]; [|now simpl].
intros <-; clear num den.
injection 1 as <-.
unfold of_hexadecimal; simpl.
now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
- case q as [num den| |]; [|now simpl..].
case q' as [num' den'| |]; [|now simpl..].
case num' as [z p| | |]; [|now simpl..].
case (Z.eq_dec z 2); [intros->|].
2:{ case z; [now simpl| |now simpl]; intro pz'.
case pz'; [intros d0..| ]; [now simpl| |now simpl].
now case d0. }
case (Pos.eq_dec den' 1%positive); [intros->|now case den'].
generalize (of_IQmake_to_hexadecimal' num den).
case IQmake_to_hexadecimal' as [d'|]; [|now simpl].
case d' as [i f|]; [|now simpl].
intros <-; clear num den.
injection 1 as <-.
unfold of_hexadecimal; simpl.
now unfold Z.of_uint; rewrite DecimalPos.Unsigned.of_to; simpl.
Qed.
Definition dnorm (d:hexadecimal) : hexadecimal :=
let norm_i i f :=
match i with
| Pos i => Pos (unorm i)
| Neg i => match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end
end in
match d with
| Hexadecimal i f => Hexadecimal (norm_i i f) f
| HexadecimalExp i f e =>
match Decimal.norm e with
| Decimal.Pos Decimal.zero => Hexadecimal (norm_i i f) f
| e => HexadecimalExp (norm_i i f) f e
end
end.
Lemma dnorm_spec_i d :
let (i, f) :=
match d with Hexadecimal i f => (i, f) | HexadecimalExp i f _ => (i, f) end in
let i' := match dnorm d with Hexadecimal i _ => i | HexadecimalExp i _ _ => i end in
match i with
| Pos i => i' = Pos (unorm i)
| Neg i =>
(i' = Neg (unorm i) /\ (nzhead i <> Nil \/ nzhead f <> Nil))
\/ (i' = Pos zero /\ (nzhead i = Nil /\ nzhead f = Nil))
end.
Proof.
case d as [i f|i f e]; case i as [i|i].
- now simpl.
- simpl; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+ rewrite Ha; right; split; [now simpl|split].
* now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
* now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+ left; split; [now revert Ha; case nzhead|].
case (uint_eq_dec (nzhead i) Nil).
* intro Hi; right; intro Hf; apply Ha.
now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
* now intro H; left.
- simpl; case (Decimal.norm e); clear e; intro e; [|now simpl].
now case e; clear e; [|intro e..]; [|case e|..].
- simpl.
set (m := match nzhead _ with Nil => _ | _ => _ end).
set (m' := match _ with Hexadecimal _ _ => _ | _ => _ end).
replace m' with m.
2:{ unfold m'; case (Decimal.norm e); clear m' e; intro e; [|now simpl].
now case e; clear e; [|intro e..]; [|case e|..]. }
unfold m; case (uint_eq_dec (nzhead (app i f)) Nil); intro Ha.
+ rewrite Ha; right; split; [now simpl|split].
* now unfold unorm; rewrite (nzhead_app_nil_l _ _ Ha).
* now unfold unorm; rewrite (nzhead_app_nil_r _ _ Ha).
+ left; split; [now revert Ha; case nzhead|].
case (uint_eq_dec (nzhead i) Nil).
* intro Hi; right; intro Hf; apply Ha.
now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
* now intro H; left.
Qed.
Lemma dnorm_spec_f d :
let f := match d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in
let f' := match dnorm d with Hexadecimal _ f => f | HexadecimalExp _ f _ => f end in
f' = f.
Proof.
case d as [i f|i f e]; [now simpl|].
simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He].
set (i' := match i with Pos _ => _ | _ => _ end).
set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|].
unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..].
Qed.
Lemma dnorm_spec_e d :
match d, dnorm d with
| Hexadecimal _ _, Hexadecimal _ _ => True
| HexadecimalExp _ _ e, Hexadecimal _ _ =>
Decimal.norm e = Decimal.Pos Decimal.zero
| HexadecimalExp _ _ e, HexadecimalExp _ _ e' =>
e' = Decimal.norm e /\ e' <> Decimal.Pos Decimal.zero
| Hexadecimal _ _, HexadecimalExp _ _ _ => False
end.
Proof.
case d as [i f|i f e]; [now simpl|].
simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); [now intros->|intro He].
set (i' := match i with Pos _ => _ | _ => _ end).
set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
replace m with (HexadecimalExp i' f (Decimal.norm e)); [now simpl|].
unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..].
Qed.
Lemma dnorm_involutive d : dnorm (dnorm d) = dnorm d.
Proof.
case d as [i f|i f e]; case i as [i|i].
- now simpl; rewrite unorm_involutive.
- simpl; case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
set (m := match nzhead _ with Nil =>_ | _ => _ end).
replace m with (Neg (unorm i)).
2:{ now unfold m; revert Ha; case nzhead. }
case (uint_eq_dec (nzhead i) Nil); intro Hi.
+ unfold unorm; rewrite Hi; simpl.
case (uint_eq_dec (nzhead f) Nil).
* intro Hf; exfalso; apply Ha.
now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
* now case nzhead.
+ rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
now revert Ha; case nzhead.
- simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He.
+ now rewrite He; simpl; rewrite unorm_involutive.
+ set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
replace m with (HexadecimalExp (Pos (unorm i)) f (Decimal.norm e)).
2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..]. }
simpl; rewrite DecimalFacts.norm_involutive, unorm_involutive.
revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..].
- simpl; case (Decimal.int_eq_dec (Decimal.norm e) (Decimal.Pos Decimal.zero)); intro He.
+ rewrite He; simpl.
case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
set (m := match nzhead _ with Nil =>_ | _ => _ end).
replace m with (Neg (unorm i)).
2:{ now unfold m; revert Ha; case nzhead. }
case (uint_eq_dec (nzhead i) Nil); intro Hi.
* unfold unorm; rewrite Hi; simpl.
case (uint_eq_dec (nzhead f) Nil).
-- intro Hf; exfalso; apply Ha.
now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
-- now case nzhead.
* rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
now revert Ha; case nzhead.
+ set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
pose (i' := match nzhead (app i f) with Nil => Pos zero | _ => Neg (unorm i) end).
replace m with (HexadecimalExp i' f (Decimal.norm e)).
2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..]. }
simpl; rewrite DecimalFacts.norm_involutive.
set (i'' := match i' with Pos _ => _ | _ => _ end).
clear m; set (m := match Decimal.norm e with Decimal.Pos _ => _ | _ => _ end).
replace m with (HexadecimalExp i'' f (Decimal.norm e)).
2:{ unfold m; revert He; case (Decimal.norm e); clear m e; intro e; [|now simpl].
now case e; clear e; [|intro e; case e|..]. }
unfold i'', i'.
case (uint_eq_dec (nzhead (app i f)) Nil); [now intros->|intro Ha].
fold i'; replace i' with (Neg (unorm i)).
2:{ now unfold i'; revert Ha; case nzhead. }
case (uint_eq_dec (nzhead i) Nil); intro Hi.
* unfold unorm; rewrite Hi; simpl.
case (uint_eq_dec (nzhead f) Nil).
-- intro Hf; exfalso; apply Ha.
now rewrite <-nzhead_app_nzhead, Hi, app_nil_l.
-- now case nzhead.
* rewrite unorm_involutive, (unorm_nzhead _ Hi), nzhead_app_nzhead.
now revert Ha; case nzhead.
Qed.
Lemma IZ_to_Z_IZ_of_Z z : IZ_to_Z (IZ_of_Z z) = Some z.
Proof. now case z. Qed.
Lemma dnorm_i_exact i f :
(nb_digits f < nb_digits (unorm (app (abs i) f)))%nat ->
match i with
| Pos i => Pos (unorm i)
| Neg i =>
match nzhead (app i f) with
| Nil => Pos zero
| _ => Neg (unorm i)
end
end = norm i.
Proof.
case i as [ni|ni]; [now simpl|]; simpl.
case (uint_eq_dec (nzhead (app ni f)) Nil); intro Ha.
{ now rewrite Ha, (nzhead_app_nil_l _ _ Ha). }
rewrite (unorm_nzhead _ Ha).
set (m := match nzhead _ with Nil => _ | _ => _ end).
replace m with (Neg (unorm ni)); [|now unfold m; revert Ha; case nzhead].
case (uint_eq_dec (nzhead ni) Nil); intro Hni.
{ rewrite <-nzhead_app_nzhead, Hni, app_nil_l.
intro H; exfalso; revert H; apply Nat.le_ngt, nb_digits_nzhead. }
clear m; set (m := match nzhead ni with Nil => _ | _ => _ end).
replace m with (Neg (nzhead ni)); [|now unfold m; revert Hni; case nzhead].
now rewrite (unorm_nzhead _ Hni).
Qed.
Lemma dnorm_i_exact' i f :
(nb_digits (unorm (app (abs i) f)) <= nb_digits f)%nat ->
match i with
| Pos i => Pos (unorm i)
| Neg i =>
match nzhead (app i f) with
| Nil => Pos zero
| _ => Neg (unorm i)
end
end =
match norm (app_int i f) with
| Pos _ => Pos zero
| Neg _ => Neg zero
end.
Proof.
case i as [ni|ni]; simpl.
{ now intro Hnb; rewrite (unorm_app_zero _ _ Hnb). }
unfold unorm.
case (uint_eq_dec (nzhead (app ni f)) Nil); intro Hn.
{ now rewrite Hn. }
set (m := match nzhead _ with Nil => _ | _ => _ end).
replace m with (nzhead (app ni f)).
2:{ now unfold m; revert Hn; case nzhead. }
clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
replace m with (Neg (unorm ni)).
2:{ now unfold m, unorm; revert Hn; case nzhead. }
clear m; set (m := match nzhead _ with Nil => _ | _ => _ end).
replace m with (Neg (nzhead (app ni f))).
2:{ now unfold m; revert Hn; case nzhead. }
rewrite <-(unorm_nzhead _ Hn).
now intro H; rewrite (unorm_app_zero _ _ H).
Qed.
Lemma to_of (d:hexadecimal) : to_hexadecimal (of_hexadecimal d) = Some (dnorm d).
Proof.
case d as [i f|i f e].
- unfold of_hexadecimal; simpl; unfold IQmake_to_hexadecimal'.
rewrite IZ_to_Z_IZ_of_Z.
unfold IQmake_to_hexadecimal; simpl.
change (fun _ : positive => _) with (Pos.mul 16).
rewrite nztail_to_hex_uint_pow16, to_of.
case_eq (nb_digits f); [|intro nb]; intro Hnb.
+ rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
case i as [ni|ni]; [now simpl|].
rewrite app_nil_r; simpl; unfold unorm.
now case (nzhead ni).
+ rewrite <-Hnb.
rewrite abs_norm, abs_app_int.
case Nat.ltb_spec; intro Hnb'.
* rewrite (del_tail_app_int_exact _ _ Hnb').
rewrite (del_head_app_int_exact _ _ Hnb').
now rewrite (dnorm_i_exact _ _ Hnb').
* rewrite (unorm_app_r _ _ Hnb').
rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
now rewrite dnorm_i_exact'.
- unfold of_hexadecimal; simpl.
rewrite <-DecimalZ.to_of.
case (Z.of_int e); clear e; [|intro e..]; simpl.
+ unfold IQmake_to_hexadecimal'.
rewrite IZ_to_Z_IZ_of_Z.
unfold IQmake_to_hexadecimal; simpl.
change (fun _ : positive => _) with (Pos.mul 16).
rewrite nztail_to_hex_uint_pow16, to_of.
case_eq (nb_digits f); [|intro nb]; intro Hnb.
* rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
case i as [ni|ni]; [now simpl|].
rewrite app_nil_r; simpl; unfold unorm.
now case (nzhead ni).
* rewrite <-Hnb.
rewrite abs_norm, abs_app_int.
case Nat.ltb_spec; intro Hnb'.
-- rewrite (del_tail_app_int_exact _ _ Hnb').
rewrite (del_head_app_int_exact _ _ Hnb').
now rewrite (dnorm_i_exact _ _ Hnb').
-- rewrite (unorm_app_r _ _ Hnb').
rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
now rewrite dnorm_i_exact'.
+ unfold IQmake_to_hexadecimal'.
rewrite IZ_to_Z_IZ_of_Z.
unfold IQmake_to_hexadecimal; simpl.
change (fun _ : positive => _) with (Pos.mul 16).
rewrite nztail_to_hex_uint_pow16, to_of.
generalize (DecimalPos.Unsigned.to_uint_nonzero e); intro He.
set (dnorm_i := match i with Pos _ => _ | _ => _ end).
set (m := match Pos.to_uint e with Decimal.Nil => _ | _ => _ end).
replace m with (HexadecimalExp dnorm_i f (Decimal.Pos (Pos.to_uint e))).
2:{ now unfold m; revert He; case (Pos.to_uint e); [|intro u; case u|..]. }
clear m; unfold dnorm_i.
case_eq (nb_digits f); [|intro nb]; intro Hnb.
* rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
case i as [ni|ni]; [now simpl|].
rewrite app_nil_r; simpl; unfold unorm.
now case (nzhead ni).
* rewrite <-Hnb.
rewrite abs_norm, abs_app_int.
case Nat.ltb_spec; intro Hnb'.
-- rewrite (del_tail_app_int_exact _ _ Hnb').
rewrite (del_head_app_int_exact _ _ Hnb').
now rewrite (dnorm_i_exact _ _ Hnb').
-- rewrite (unorm_app_r _ _ Hnb').
rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
now rewrite dnorm_i_exact'.
+ unfold IQmake_to_hexadecimal'.
rewrite IZ_to_Z_IZ_of_Z.
unfold IQmake_to_hexadecimal; simpl.
change (fun _ : positive => _) with (Pos.mul 16).
rewrite nztail_to_hex_uint_pow16, to_of.
case_eq (nb_digits f); [|intro nb]; intro Hnb.
* rewrite (nb_digits_0 _ Hnb), app_int_nil_r.
case i as [ni|ni]; [now simpl|].
rewrite app_nil_r; simpl; unfold unorm.
now case (nzhead ni).
* rewrite <-Hnb.
rewrite abs_norm, abs_app_int.
case Nat.ltb_spec; intro Hnb'.
-- rewrite (del_tail_app_int_exact _ _ Hnb').
rewrite (del_head_app_int_exact _ _ Hnb').
now rewrite (dnorm_i_exact _ _ Hnb').
-- rewrite (unorm_app_r _ _ Hnb').
rewrite iter_D0_unorm; [|now apply nb_digits_n0; rewrite Hnb].
now rewrite dnorm_i_exact'.
Qed.
(** Some consequences *)
Lemma to_hexadecimal_inj q q' :
to_hexadecimal q <> None -> to_hexadecimal q = to_hexadecimal q' -> q = q'.
Proof.
intros Hnone EQ.
generalize (of_to q) (of_to q').
rewrite <-EQ.
revert Hnone; case to_hexadecimal; [|now simpl].
now intros d _ H1 H2; rewrite <-(H1 d eq_refl), <-(H2 d eq_refl).
Qed.
Lemma to_hexadecimal_surj d : exists q, to_hexadecimal q = Some (dnorm d).
Proof.
exists (of_hexadecimal d). apply to_of.
Qed.
Lemma of_hexadecimal_dnorm d : of_hexadecimal (dnorm d) = of_hexadecimal d.
Proof. now apply to_hexadecimal_inj; rewrite !to_of; [|rewrite dnorm_involutive]. Qed.
Lemma of_inj d d' : of_hexadecimal d = of_hexadecimal d' -> dnorm d = dnorm d'.
Proof.
intro H.
apply (@f_equal _ _ (fun x => match x with Some x => x | _ => d end)
(Some (dnorm d)) (Some (dnorm d'))).
now rewrite <- !to_of, H.
Qed.
Lemma of_iff d d' : of_hexadecimal d = of_hexadecimal d' <-> dnorm d = dnorm d'.
Proof.
split. apply of_inj. intros E. rewrite <- of_hexadecimal_dnorm, E.
apply of_hexadecimal_dnorm.
Qed.
|
