baseconv/DeciString.v at master · letouzey/baseconv · GitHub

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

Require Import Deci Ascii String.

(** * Conversion between dec and string *)

(** Pretty straightforward, which is precisely the point of the
    [dec] datatype. The only catch is that [nil] means ["0"],
    not the empty string, so we don't have a perfect bijection. *)

Definition to_char (d:digit) :=
 match d with
 | D0 => "0"
 | D1 => "1"
 | D2 => "2"
 | D3 => "3"
 | D4 => "4"
 | D5 => "5"
 | D6 => "6"
 | D7 => "7"
 | D8 => "8"
 | D9 => "9"
 end%char.

Fixpoint to_string_rec (dl:dec) :=
 match dl with
 | nil => EmptyString
 | d::dl => String (to_char d) (to_string_rec dl)
 end.

Definition to_string (dl:dec) :=
 match dl with
 | nil => "0"%string
 | _ => to_string_rec dl
 end.

Definition of_char (a:ascii) :=
 match a with
 | "0" => Some D0
 | "1" => Some D1
 | "2" => Some D2
 | "3" => Some D3
 | "4" => Some D4
 | "5" => Some D5
 | "6" => Some D6
 | "7" => Some D7
 | "8" => Some D8
 | "9" => Some D9
 | _ => None
 end%char.

Definition ocons (od:option digit)(ol:option dec) :=
 match od, ol with
 | Some d, Some dl => Some (d::dl)
 | _,_ => None
 end.

Fixpoint of_string_rec s :=
 match s with
 | EmptyString => Some nil
 | String a s => ocons (of_char a) (of_string_rec s)
 end.

Definition of_string s :=
 match s with
 | EmptyString => None
 | _ => of_string_rec s
 end.

(* Compute of_string "123456890123456890123456890123456890". *)

Lemma of_to_char d : of_char (to_char d) = Some d.
Proof.
 now destruct d.
Qed.

Lemma of_to_rec d : of_string_rec (to_string_rec d) = Some d.
Proof.
 induction d; simpl; rewrite ?IHd, ?of_to_char; simpl; auto.
Qed.

Lemma of_to d : d<>nil -> of_string (to_string d) = Some d.
Proof.
 destruct d. now destruct 1. intros _. apply of_to_rec.
Qed.

Lemma of_to_nil : of_string (to_string nil) = Some (D0::nil).
Proof.
 reflexivity.
Qed.

Lemma of_to_gen d :
  of_string (to_string d) = Some d \/
  of_string (to_string d) = Some (D0::d).
Proof.
 destruct d.
 - now right.
 - left. now apply of_to.
Qed.

Lemma to_of_char c d : of_char c = Some d -> to_char d = c.
Proof.
 destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]];
  discriminate || injection 1 as <-; auto.
Qed.

Lemma to_of_rec s d : of_string_rec s = Some d -> to_string_rec d = s.
Proof.
 revert d.
 induction s; simpl.
 - now injection 1 as <-.
 - destruct (of_char a) eqn:Ha; try discriminate.
   destruct (of_string_rec s) eqn:Hs; try discriminate.
   simpl. injection 1 as <-. simpl. f_equal; auto using to_of_char.
Qed.

Lemma of_non_nil s : of_string s <> Some nil.
Proof.
 destruct s.
 - now simpl.
 - simpl.
   now destruct of_char, of_string_rec.
Qed.

Lemma to_of s d : of_string s = Some d -> to_string d = s.
Proof.
 destruct s; try discriminate.
 intros H.
 assert (d<>nil).
 { intros ->. apply (of_non_nil _ H). }
 apply to_of_rec in H.
 now destruct d.
Qed.