Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   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)         *)
(************************************************************************)

Require Import Decimal Ascii String.

Conversion between decimal numbers and Coq strings

Pretty straightforward, which is precisely the point of the Decimal.int datatype. The only catch is Decimal.Nil : we could choose to convert it as "" or as "0". In the first case, it is awkward to consider "" (or "-") as a number, while in the second case we don't have a perfect bijection. Since the second variant is implemented thanks to the first one, we provide both.

Local Open Scope string_scope.

Parsing one char

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

Lemma uint_of_char_spec c d d' :
  uint_of_char c (Some d) = Some d' ->
  (c = "0" /\ d' = D0 d \/
  c = "1" /\ d' = D1 d \/
  c = "2" /\ d' = D2 d \/
  c = "3" /\ d' = D3 d \/
  c = "4" /\ d' = D4 d \/
  c = "5" /\ d' = D5 d \/
  c = "6" /\ d' = D6 d \/
  c = "7" /\ d' = D7 d \/
  c = "8" /\ d' = D8 d \/
  c = "9" /\ d' = D9 d)%char.c:ascii
d, d':uint
uint_of_char c (Some d) = Some d' ->
c = "0"%char /\ d' = D0 d \/
c = "1"%char /\ d' = D1 d \/
c = "2"%char /\ d' = D2 d \/
c = "3"%char /\ d' = D3 d \/
c = "4"%char /\ d' = D4 d \/
c = "5"%char /\ d' = D5 d \/
c = "6"%char /\ d' = D6 d \/
c = "7"%char /\ d' = D7 d \/
c = "8"%char /\ d' = D8 d \/ c = "9"%char /\ d' = D9 d
Proof.c:ascii
d, d':uint
uint_of_char c (Some d) = Some d' ->
c = "0"%char /\ d' = D0 d \/
c = "1"%char /\ d' = D1 d \/
c = "2"%char /\ d' = D2 d \/
c = "3"%char /\ d' = D3 d \/
c = "4"%char /\ d' = D4 d \/
c = "5"%char /\ d' = D5 d \/
c = "6"%char /\ d' = D6 d \/
c = "7"%char /\ d' = D7 d \/
c = "8"%char /\ d' = D8 d \/ c = "9"%char /\ d' = D9 d
 destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]];
 intros [= <-]; intuition.
Qed.

Decimal/String conversion where Nil is ""

Module NilEmpty.

Fixpoint string_of_uint (d:uint) :=
 match d with
 | Nil => EmptyString
 | D0 d => String "0" (string_of_uint d)
 | D1 d => String "1" (string_of_uint d)
 | D2 d => String "2" (string_of_uint d)
 | D3 d => String "3" (string_of_uint d)
 | D4 d => String "4" (string_of_uint d)
 | D5 d => String "5" (string_of_uint d)
 | D6 d => String "6" (string_of_uint d)
 | D7 d => String "7" (string_of_uint d)
 | D8 d => String "8" (string_of_uint d)
 | D9 d => String "9" (string_of_uint d)
 end.

Fixpoint uint_of_string s :=
 match s with
 | EmptyString => Some Nil
 | String a s => uint_of_char a (uint_of_string s)
 end.

Definition string_of_int (d:int) :=
 match d with
 | Pos d => string_of_uint d
 | Neg d => String "-" (string_of_uint d)
 end.

Definition int_of_string s :=
 match s with
 | EmptyString => Some (Pos Nil)
 | String a s' =>
   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
   else option_map Pos (uint_of_string s)
 end.

(* NB: For the moment whitespace between - and digits are not accepted.
   And in this variant [int_of_string "-" = Some (Neg Nil)].

Compute int_of_string "-123456890123456890123456890123456890".
Compute string_of_int (-123456890123456890123456890123456890).
*)

Corresponding proofs

Lemma usu d :
  uint_of_string (string_of_uint d) = Some d.d:uint
uint_of_string (string_of_uint d) = Some d
Proof.d:uint
uint_of_string (string_of_uint d) = Some d
 induction d; simpl; rewrite ?IHd; simpl; auto.
Qed.

Lemma sus s d :
  uint_of_string s = Some d -> string_of_uint d = s.s:string
d:uint
uint_of_string s = Some d -> string_of_uint d = s
Proof.s:string
d:uint
uint_of_string s = Some d -> string_of_uint d = s
 revert d.s:string
forall d : uint,
uint_of_string s = Some d -> string_of_uint d = s
 induction s; simpl.forall d : uint,
Some Nil = Some d -> string_of_uint d = ""
a:ascii
s:string
IHs:forall d : uint, uint_of_string s = Some d -> string_of_uint d = s
forall d : uint,
uint_of_char a (uint_of_string s) = Some d ->
string_of_uint d = String a s
 -forall d : uint,
Some Nil = Some d -> string_of_uint d = "" now intros d [= <-].
 -a:ascii
s:string
IHs:forall d : uint, uint_of_string s = Some d -> string_of_uint d = s
forall d : uint,
uint_of_char a (uint_of_string s) = Some d ->
string_of_uint d = String a s intros d.a:ascii
s:string
IHs:forall d0 : uint, uint_of_string s = Some d0 -> string_of_uint d0 = s
d:uint
uint_of_char a (uint_of_string s) = Some d ->
string_of_uint d = String a s
   destruct (uint_of_string s); [intros H | intros [=]].a:ascii
s:string
u:uint
IHs:forall d0 : uint, Some u = Some d0 -> string_of_uint d0 = s
d:uint
H:uint_of_char a (Some u) = Some d
string_of_uint d = String a s
   apply uint_of_char_spec in H.a:ascii
s:string
u:uint
IHs:forall d0 : uint, Some u = Some d0 -> string_of_uint d0 = s
d:uint
H:a = "0"%char /\ d = D0 u \/
a = "1"%char /\ d = D1 u \/
a = "2"%char /\ d = D2 u \/
a = "3"%char /\ d = D3 u \/
a = "4"%char /\ d = D4 u \/
a = "5"%char /\ d = D5 u \/
a = "6"%char /\ d = D6 u \/
a = "7"%char /\ d = D7 u \/
a = "8"%char /\ d = D8 u \/
a = "9"%char /\ d = D9 u
string_of_uint d = String a s
   intuition subst; simpl; f_equal; auto.
Qed.

Lemma isi d : int_of_string (string_of_int d) = Some d.d:int
int_of_string (string_of_int d) = Some d
Proof.d:int
int_of_string (string_of_int d) = Some d
 destruct d; simpl.d:uint
int_of_string (string_of_uint d) = Some (Pos d)
d:uint
option_map Neg (uint_of_string (string_of_uint d)) =
Some (Neg d)
 -d:uint
int_of_string (string_of_uint d) = Some (Pos d) unfold int_of_string.d:uint
match string_of_uint d with
| "" => Some (Pos Nil)
| String a s' =>
    if (a =? "-")%char
    then option_map Neg (uint_of_string s')
    else
     option_map Pos
       (uint_of_string (string_of_uint d))
end = Some (Pos d)
   destruct (string_of_uint d) eqn:Hd.d:uint
Hd:string_of_uint d = ""
Some (Pos Nil) = Some (Pos d)
d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else option_map Pos (uint_of_string (String a s))) =
Some (Pos d)
   +d:uint
Hd:string_of_uint d = ""
Some (Pos Nil) = Some (Pos d) now destruct d.
   +d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else option_map Pos (uint_of_string (String a s))) =
Some (Pos d) case Ascii.eqb_spec.d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
a = "-"%char ->
option_map Neg (uint_of_string s) = Some (Pos d)
d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
a <> "-"%char ->
option_map Pos (uint_of_string (String a s)) =
Some (Pos d)
     *d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
a = "-"%char ->
option_map Neg (uint_of_string s) = Some (Pos d) intros ->.d:uint
s:string
Hd:string_of_uint d = String "-" s
option_map Neg (uint_of_string s) = Some (Pos d) now destruct d.
     *d:uint
a:ascii
s:string
Hd:string_of_uint d = String a s
a <> "-"%char ->
option_map Pos (uint_of_string (String a s)) =
Some (Pos d) rewrite <- Hd, usu; auto.
 -d:uint
option_map Neg (uint_of_string (string_of_uint d)) =
Some (Neg d) rewrite usu; auto.
Qed.

Lemma sis s d :
 int_of_string s = Some d -> string_of_int d = s.s:string
d:int
int_of_string s = Some d -> string_of_int d = s
Proof.s:string
d:int
int_of_string s = Some d -> string_of_int d = s
 destruct s; [intros [= <-]| ]; simpl; trivial.a:ascii
s:string
d:int
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else
  option_map Pos (uint_of_char a (uint_of_string s))) =
Some d -> string_of_int d = String a s
 case Ascii.eqb_spec.a:ascii
s:string
d:int
a = "-"%char ->
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String a s
a:ascii
s:string
d:int
a <> "-"%char ->
option_map Pos (uint_of_char a (uint_of_string s)) =
Some d -> string_of_int d = String a s
 -a:ascii
s:string
d:int
a = "-"%char ->
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String a s intros ->.s:string
d:int
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String "-" s destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].s:string
u:uint
Hs:uint_of_string s = Some u
string_of_int (Neg u) = String "-" s
   simpl; f_equal.s:string
u:uint
Hs:uint_of_string s = Some u
string_of_uint u = s now apply sus.
 -a:ascii
s:string
d:int
a <> "-"%char ->
option_map Pos (uint_of_char a (uint_of_string s)) =
Some d -> string_of_int d = String a s destruct d; [ | now destruct uint_of_char].a:ascii
s:string
d:uint
a <> "-"%char ->
option_map Pos (uint_of_char a (uint_of_string s)) =
Some (Pos d) -> string_of_int (Pos d) = String a s
   simpl string_of_int.a:ascii
s:string
d:uint
a <> "-"%char ->
option_map Pos (uint_of_char a (uint_of_string s)) =
Some (Pos d) -> string_of_uint d = String a s
   intros.a:ascii
s:string
d:uint
n:a <> "-"%char
H:option_map Pos (uint_of_char a (uint_of_string s)) =
Some (Pos d)
string_of_uint d = String a s apply sus; simpl.a:ascii
s:string
d:uint
n:a <> "-"%char
H:option_map Pos (uint_of_char a (uint_of_string s)) =
Some (Pos d)
uint_of_char a (uint_of_string s) = Some d
   destruct uint_of_char; simpl in *; congruence.
Qed.

End NilEmpty.

Decimal/String conversions where Nil is "0"

Module NilZero.

Definition string_of_uint (d:uint) :=
 match d with
 | Nil => "0"
 | _ => NilEmpty.string_of_uint d
 end.

Definition uint_of_string s :=
 match s with
 | EmptyString => None
 | _ => NilEmpty.uint_of_string s
 end.

Definition string_of_int (d:int) :=
 match d with
 | Pos d => string_of_uint d
 | Neg d => String "-" (string_of_uint d)
 end.

Definition int_of_string s :=
 match s with
 | EmptyString => None
 | String a s' =>
   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
   else option_map Pos (uint_of_string s)
 end.

Corresponding proofs

Lemma uint_of_string_nonnil s : uint_of_string s <> Some Nil.s:string
uint_of_string s <> Some Nil
Proof.s:string
uint_of_string s <> Some Nil
 destruct s; simpl.None <> Some Nil
a:ascii
s:string
uint_of_char a (NilEmpty.uint_of_string s) <> Some Nil
 -None <> Some Nil easy.
 -a:ascii
s:string
uint_of_char a (NilEmpty.uint_of_string s) <> Some Nil destruct (NilEmpty.uint_of_string s); [intros H | intros [=]].a:ascii
s:string
u:uint
H:uint_of_char a (Some u) = Some Nil
False
   apply uint_of_char_spec in H.a:ascii
s:string
u:uint
H:a = "0"%char /\ Nil = D0 u \/
a = "1"%char /\ Nil = D1 u \/
a = "2"%char /\ Nil = D2 u \/
a = "3"%char /\ Nil = D3 u \/
a = "4"%char /\ Nil = D4 u \/
a = "5"%char /\ Nil = D5 u \/
a = "6"%char /\ Nil = D6 u \/
a = "7"%char /\ Nil = D7 u \/
a = "8"%char /\ Nil = D8 u \/
a = "9"%char /\ Nil = D9 u
False
   now intuition subst.
Qed.

Lemma sus s d :
  uint_of_string s = Some d -> string_of_uint d = s.s:string
d:uint
uint_of_string s = Some d -> string_of_uint d = s
Proof.s:string
d:uint
uint_of_string s = Some d -> string_of_uint d = s
 destruct s; [intros [=] | intros H].a:ascii
s:string
d:uint
H:uint_of_string (String a s) = Some d
string_of_uint d = String a s
 apply NilEmpty.sus in H.a:ascii
s:string
d:uint
H:NilEmpty.string_of_uint d = String a s
string_of_uint d = String a s now destruct d.
Qed.

Lemma usu d :
  d<>Nil -> uint_of_string (string_of_uint d) = Some d.d:uint
d <> Nil -> uint_of_string (string_of_uint d) = Some d
Proof.d:uint
d <> Nil -> uint_of_string (string_of_uint d) = Some d
 destruct d; (now destruct 1) || (intros _; apply NilEmpty.usu).
Qed.

Lemma usu_nil :
  uint_of_string (string_of_uint Nil) = Some Decimal.zero.uint_of_string (string_of_uint Nil) = Some 0%uint
Proof.uint_of_string (string_of_uint Nil) = Some 0%uint
 reflexivity.
Qed.

Lemma usu_gen d :
  uint_of_string (string_of_uint d) = Some d \/
  uint_of_string (string_of_uint d) = Some Decimal.zero.d:uint
uint_of_string (string_of_uint d) = Some d \/
uint_of_string (string_of_uint d) = Some 0%uint
Proof.d:uint
uint_of_string (string_of_uint d) = Some d \/
uint_of_string (string_of_uint d) = Some 0%uint
 destruct d; (now right) || (left; now apply usu).
Qed.

Lemma isi d :
  d<>Pos Nil -> d<>Neg Nil ->
  int_of_string (string_of_int d) = Some d.d:int
d <> Pos Nil ->
d <> Neg Nil ->
int_of_string (string_of_int d) = Some d
Proof.d:int
d <> Pos Nil ->
d <> Neg Nil ->
int_of_string (string_of_int d) = Some d
 destruct d; simpl.d:uint
Pos d <> Pos Nil ->
Pos d <> Neg Nil ->
int_of_string (string_of_uint d) = Some (Pos d)
d:uint
Neg d <> Pos Nil ->
Neg d <> Neg Nil ->
option_map Neg (uint_of_string (string_of_uint d)) =
Some (Neg d)
 -d:uint
Pos d <> Pos Nil ->
Pos d <> Neg Nil ->
int_of_string (string_of_uint d) = Some (Pos d) intros H _.d:uint
H:Pos d <> Pos Nil
int_of_string (string_of_uint d) = Some (Pos d)
   unfold int_of_string.d:uint
H:Pos d <> Pos Nil
match string_of_uint d with
| "" => None
| String a s' =>
    if (a =? "-")%char
    then option_map Neg (uint_of_string s')
    else
     option_map Pos
       (uint_of_string (string_of_uint d))
end = Some (Pos d)
   destruct (string_of_uint d) eqn:Hd.d:uint
H:Pos d <> Pos Nil
Hd:string_of_uint d = ""
None = Some (Pos d)
d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else option_map Pos (uint_of_string (String a s))) =
Some (Pos d)
   +d:uint
H:Pos d <> Pos Nil
Hd:string_of_uint d = ""
None = Some (Pos d) now destruct d.
   +d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else option_map Pos (uint_of_string (String a s))) =
Some (Pos d) case Ascii.eqb_spec.d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
a = "-"%char ->
option_map Neg (uint_of_string s) = Some (Pos d)
d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
a <> "-"%char ->
option_map Pos (uint_of_string (String a s)) =
Some (Pos d)
     *d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
a = "-"%char ->
option_map Neg (uint_of_string s) = Some (Pos d) intros ->.d:uint
H:Pos d <> Pos Nil
s:string
Hd:string_of_uint d = String "-" s
option_map Neg (uint_of_string s) = Some (Pos d) now destruct d.
     *d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
a <> "-"%char ->
option_map Pos (uint_of_string (String a s)) =
Some (Pos d) rewrite <- Hd, usu; auto.d:uint
H:Pos d <> Pos Nil
a:ascii
s:string
Hd:string_of_uint d = String a s
d <> Nil now intros ->.
 -d:uint
Neg d <> Pos Nil ->
Neg d <> Neg Nil ->
option_map Neg (uint_of_string (string_of_uint d)) =
Some (Neg d) intros _ H.d:uint
H:Neg d <> Neg Nil
option_map Neg (uint_of_string (string_of_uint d)) =
Some (Neg d)
   rewrite usu; auto.d:uint
H:Neg d <> Neg Nil
d <> Nil now intros ->.
Qed.

Lemma isi_posnil :
 int_of_string (string_of_int (Pos Nil)) = Some (Pos Decimal.zero).int_of_string (string_of_int (Pos Nil)) = Some 0%int
Proof.int_of_string (string_of_int (Pos Nil)) = Some 0%int
 reflexivity.
Qed.

Warning! (-0) won't parse (compatibility with the behavior of Z).

Lemma isi_negnil :
 int_of_string (string_of_int (Neg Nil)) = Some (Neg (D0 Nil)).int_of_string (string_of_int (Neg Nil)) =
Some (-0)%int
Proof.int_of_string (string_of_int (Neg Nil)) =
Some (-0)%int
 reflexivity.
Qed.

Lemma sis s d :
 int_of_string s = Some d -> string_of_int d = s.s:string
d:int
int_of_string s = Some d -> string_of_int d = s
Proof.s:string
d:int
int_of_string s = Some d -> string_of_int d = s
 destruct s; [intros [=]| ]; simpl.a:ascii
s:string
d:int
(if (a =? "-")%char
 then option_map Neg (uint_of_string s)
 else
  option_map Pos
    (uint_of_char a (NilEmpty.uint_of_string s))) =
Some d -> string_of_int d = String a s
 case Ascii.eqb_spec.a:ascii
s:string
d:int
a = "-"%char ->
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String a s
a:ascii
s:string
d:int
a <> "-"%char ->
option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some d -> string_of_int d = String a s
 -a:ascii
s:string
d:int
a = "-"%char ->
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String a s intros ->.s:string
d:int
option_map Neg (uint_of_string s) = Some d ->
string_of_int d = String "-" s destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].s:string
u:uint
Hs:uint_of_string s = Some u
string_of_int (Neg u) = String "-" s
   simpl; f_equal.s:string
u:uint
Hs:uint_of_string s = Some u
string_of_uint u = s now apply sus.
 -a:ascii
s:string
d:int
a <> "-"%char ->
option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some d -> string_of_int d = String a s destruct d; [ | now destruct uint_of_char].a:ascii
s:string
d:uint
a <> "-"%char ->
option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some (Pos d) -> string_of_int (Pos d) = String a s
   simpl string_of_int.a:ascii
s:string
d:uint
a <> "-"%char ->
option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some (Pos d) -> string_of_uint d = String a s
   intros.a:ascii
s:string
d:uint
n:a <> "-"%char
H:option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some (Pos d)
string_of_uint d = String a s apply sus; simpl.a:ascii
s:string
d:uint
n:a <> "-"%char
H:option_map Pos
  (uint_of_char a (NilEmpty.uint_of_string s)) =
Some (Pos d)
uint_of_char a (NilEmpty.uint_of_string s) = Some d
   destruct uint_of_char; simpl in *; congruence.
Qed.

End NilZero.