blob: 0f49052777610ab6f7f115820a2e85bf510041f4 (
plain)
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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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) *)
(************************************************************************)
(** * DecimalFacts : some facts about Decimal numbers *)
Require Import Decimal.
Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.
Proof.
decide equality.
Defined.
Lemma rev_revapp d d' :
rev (revapp d d') = revapp d' d.
Proof.
revert d'. induction d; simpl; intros; now rewrite ?IHd.
Qed.
Lemma rev_rev d : rev (rev d) = d.
Proof.
apply rev_revapp.
Qed.
(** Normalization on little-endian numbers *)
Fixpoint nztail d :=
match d with
| Nil => Nil
| D0 d => match nztail d with Nil => Nil | d' => D0 d' end
| D1 d => D1 (nztail d)
| D2 d => D2 (nztail d)
| D3 d => D3 (nztail d)
| D4 d => D4 (nztail d)
| D5 d => D5 (nztail d)
| D6 d => D6 (nztail d)
| D7 d => D7 (nztail d)
| D8 d => D8 (nztail d)
| D9 d => D9 (nztail d)
end.
Definition lnorm d :=
match nztail d with
| Nil => zero
| d => d
end.
Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
nzhead (revapp d d') = nzhead d'.
Proof.
revert d'. induction d; intros d' [=]; simpl; trivial.
destruct (nztail d); now rewrite IHd.
Qed.
Lemma nzhead_revapp d d' : nztail d <> Nil ->
nzhead (revapp d d') = revapp (nztail d) d'.
Proof.
revert d'.
induction d; intros d' H; simpl in *;
try destruct (nztail d) eqn:E;
(now rewrite ?nzhead_revapp_0) || (now rewrite IHd).
Qed.
Lemma nzhead_rev d : nztail d <> Nil ->
nzhead (rev d) = rev (nztail d).
Proof.
apply nzhead_revapp.
Qed.
Lemma rev_nztail_rev d :
rev (nztail (rev d)) = nzhead d.
Proof.
destruct (uint_dec (nztail (rev d)) Nil) as [H|H].
- rewrite H. unfold rev; simpl.
rewrite <- (rev_rev d). symmetry.
now apply nzhead_revapp_0.
- now rewrite <- nzhead_rev, rev_rev.
Qed.
Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.
Proof.
revert d'.
induction d; simpl; intros d' H; auto; now apply IHd in H.
Qed.
Lemma rev_nil_inv d : rev d = Nil -> d = Nil.
Proof.
apply revapp_nil_inv.
Qed.
Lemma rev_lnorm_rev d :
rev (lnorm (rev d)) = unorm d.
Proof.
unfold unorm, lnorm.
rewrite <- rev_nztail_rev.
destruct nztail; simpl; trivial;
destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
Qed.
Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.
Proof.
induction d; easy.
Qed.
Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.
Proof.
unfold unorm. split.
- generalize (nzhead_nonzero d).
destruct nzhead; intros H [=]; trivial. now destruct (H u).
- now intros ->.
Qed.
Lemma unorm_nonnil d : unorm d <> Nil.
Proof.
unfold unorm. now destruct nzhead.
Qed.
Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.
Proof.
now induction d.
Qed.
Lemma unorm_invol d : unorm (unorm d) = unorm d.
Proof.
unfold unorm.
destruct (nzhead d) eqn:E; trivial.
destruct (nzhead_nonzero _ _ E).
Qed.
Lemma norm_invol d : norm (norm d) = norm d.
Proof.
unfold norm.
destruct d.
- f_equal. apply unorm_invol.
- destruct (nzhead d) eqn:E; auto.
destruct (nzhead_nonzero _ _ E).
Qed.
|
