blob: 955c6c8f6ac68e997cfe85480a65cbef76bdcef9 (
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
|
Require Import Coq.Strings.Ascii Coq.Strings.String.
Require Import Coq.Numbers.BinNums.
Require Import Crypto.Util.Strings.Equality.
Require Crypto.Util.Pos.
Import BinPosDef.
Local Open Scope positive_scope.
Local Open Scope string_scope.
Fixpoint bin_string_of_pos' (p : positive) (rest : string) : string
:= match p with
| 1 => String "1" rest
| p'~0 => bin_string_of_pos' p' (String "0" rest)
| p'~1 => bin_string_of_pos' p' (String "1" rest)
end.
Definition bin_string_of_pos (p : positive) : string
:= String "0" (String "b" (bin_string_of_pos' p "")).
Local Notation default := 1.
Fixpoint pos_of_bin_string' (s : string) (rest : option positive)
: option positive
:= match s with
| "" => rest
| String ch s'
=> pos_of_bin_string'
s'
(if ascii_beq ch "0"
then option_map xO rest
else if ascii_beq ch "1"
then match rest with
| Some p => Some (xI p)
| None => Some xH
end
else None)
end.
Definition pos_of_bin_string (s : string) : positive
:= match s with
| String s0 (String sb s)
=> if ascii_beq s0 "0"
then if ascii_beq sb "b"
then match pos_of_bin_string' s None with
| Some p => p
| None => default
end
else default
else default
| _ => default
end.
Lemma pos_of_bin_string_of_pos' (p : positive)
(base : option positive)
(rest : string)
: pos_of_bin_string' (bin_string_of_pos' p rest) base
= pos_of_bin_string' rest (match base with
| None => Some p
| Some v => Some (Pos.app v p)
end).
Proof.
revert base rest; induction p, base; intros; try reflexivity;
cbn; rewrite IHp; reflexivity.
Qed.
Lemma pos_of_bin_string_of_pos (p : positive)
: pos_of_bin_string (bin_string_of_pos p) = p.
Proof.
cbn; rewrite pos_of_bin_string_of_pos'; reflexivity.
Qed.
Example bin_string_of_pos_1 : bin_string_of_pos 1 = "0b1" := eq_refl.
Example bin_string_of_pos_2 : bin_string_of_pos 2 = "0b10" := eq_refl.
Example bin_string_of_pos_3 : bin_string_of_pos 3 = "0b11" := eq_refl.
|
