Add string conversions

5 files changed, 653 insertions, 0 deletions

diff --git a/src/Util/Strings/Binary.v b/src/Util/Strings/Binary.v
new file mode 100644
index 000000000..955c6c8f6
--- /dev/null
+++ b/src/Util/Strings/Binary.v
@@ -0,0 +1,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.
diff --git a/src/Util/Strings/Decimal.v b/src/Util/Strings/Decimal.v
new file mode 100644
index 000000000..1a3c276e0
--- /dev/null
+++ b/src/Util/Strings/Decimal.v
@@ -0,0 +1,219 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Coq.Numbers.BinNums.
+Require Import Crypto.Util.Strings.Equality.
+Import BinPosDef.
+
+Module Import DecimalHelpers. (* mostly from the decimal plugin, see https://github.com/coq/coq/pull/6599/files *)
+  Inductive uint :=
+  | Nil
+  | D0 (_:uint)
+  | D1 (_:uint)
+  | D2 (_:uint)
+  | D3 (_:uint)
+  | D4 (_:uint)
+  | D5 (_:uint)
+  | D6 (_:uint)
+  | D7 (_:uint)
+  | D8 (_:uint)
+  | D9 (_:uint).
+
+  Notation zero := (D0 Nil).
+
+  (** For conversions with binary numbers, it is easier to operate
+    on little-endian numbers. *)
+
+  Fixpoint revapp (d d' : uint) :=
+    match d with
+    | Nil => d'
+    | D0 d => revapp d (D0 d')
+    | D1 d => revapp d (D1 d')
+    | D2 d => revapp d (D2 d')
+    | D3 d => revapp d (D3 d')
+    | D4 d => revapp d (D4 d')
+    | D5 d => revapp d (D5 d')
+    | D6 d => revapp d (D6 d')
+    | D7 d => revapp d (D7 d')
+    | D8 d => revapp d (D8 d')
+    | D9 d => revapp d (D9 d')
+    end.
+
+  Definition rev d := revapp d Nil.
+
+  Module Little.
+    (** Successor of little-endian numbers *)
+    Fixpoint succ d :=
+      match d with
+      | Nil => D1 Nil
+      | D0 d => D1 d
+      | D1 d => D2 d
+      | D2 d => D3 d
+      | D3 d => D4 d
+      | D4 d => D5 d
+      | D5 d => D6 d
+      | D6 d => D7 d
+      | D7 d => D8 d
+      | D8 d => D9 d
+      | D9 d => D0 (succ d)
+      end.
+
+    Fixpoint double d :=
+      match d with
+      | Nil => Nil
+      | D0 d => D0 (double d)
+      | D1 d => D2 (double d)
+      | D2 d => D4 (double d)
+      | D3 d => D6 (double d)
+      | D4 d => D8 (double d)
+      | D5 d => D0 (succ_double d)
+      | D6 d => D2 (succ_double d)
+      | D7 d => D4 (succ_double d)
+      | D8 d => D6 (succ_double d)
+      | D9 d => D8 (succ_double d)
+      end
+
+    with succ_double d :=
+           match d with
+           | Nil => D1 Nil
+           | D0 d => D1 (double d)
+           | D1 d => D3 (double d)
+           | D2 d => D5 (double d)
+           | D3 d => D7 (double d)
+           | D4 d => D9 (double d)
+           | D5 d => D1 (succ_double d)
+           | D6 d => D3 (succ_double d)
+           | D7 d => D5 (succ_double d)
+           | D8 d => D7 (succ_double d)
+           | D9 d => D9 (succ_double d)
+           end.
+  End Little.
+
+
+  Module Pos.
+    Local Open Scope positive_scope.
+    Fixpoint to_little_uint p :=
+      match p with
+      | 1 => D1 Nil
+      | p~1 => Little.succ_double (to_little_uint p)
+      | p~0 => Little.double (to_little_uint p)
+      end.
+
+    Definition to_uint p := rev (to_little_uint p).
+
+    Local Notation ten := 1~0~1~0.
+
+    Fixpoint of_uint_acc (d:uint)(acc:positive) :=
+      match d with
+      | Nil => acc
+      | D0 l => of_uint_acc l (Pos.mul ten acc)
+      | D1 l => of_uint_acc l (Pos.add 1 (Pos.mul ten acc))
+      | D2 l => of_uint_acc l (Pos.add 1~0 (Pos.mul ten acc))
+      | D3 l => of_uint_acc l (Pos.add 1~1 (Pos.mul ten acc))
+      | D4 l => of_uint_acc l (Pos.add 1~0~0 (Pos.mul ten acc))
+      | D5 l => of_uint_acc l (Pos.add 1~0~1 (Pos.mul ten acc))
+      | D6 l => of_uint_acc l (Pos.add 1~1~0 (Pos.mul ten acc))
+      | D7 l => of_uint_acc l (Pos.add 1~1~1 (Pos.mul ten acc))
+      | D8 l => of_uint_acc l (Pos.add 1~0~0~0 (Pos.mul ten acc))
+      | D9 l => of_uint_acc l (Pos.add 1~0~0~1 (Pos.mul ten acc))
+      end.
+  End Pos.
+
+  Module N.
+    Fixpoint of_uint (d:uint) : N :=
+      match d with
+      | Nil => N0
+      | D0 l => of_uint l
+      | D1 l => Npos (Pos.of_uint_acc l 1)
+      | D2 l => Npos (Pos.of_uint_acc l 1~0)
+      | D3 l => Npos (Pos.of_uint_acc l 1~1)
+      | D4 l => Npos (Pos.of_uint_acc l 1~0~0)
+      | D5 l => Npos (Pos.of_uint_acc l 1~0~1)
+      | D6 l => Npos (Pos.of_uint_acc l 1~1~0)
+      | D7 l => Npos (Pos.of_uint_acc l 1~1~1)
+      | D8 l => Npos (Pos.of_uint_acc l 1~0~0~0)
+      | D9 l => Npos (Pos.of_uint_acc l 1~0~0~1)
+      end.
+  End N.
+
+  Module String.
+    Local Open Scope string_scope.
+    Fixpoint of_uint (v : uint) : string
+      := match v with
+         | Nil => ""
+         | D0 x => String "0" (of_uint x)
+         | D1 x => String "1" (of_uint x)
+         | D2 x => String "2" (of_uint x)
+         | D3 x => String "3" (of_uint x)
+         | D4 x => String "4" (of_uint x)
+         | D5 x => String "5" (of_uint x)
+         | D6 x => String "6" (of_uint x)
+         | D7 x => String "7" (of_uint x)
+         | D8 x => String "8" (of_uint x)
+         | D9 x => String "9" (of_uint x)
+         end.
+
+    Fixpoint to_uint (v : string) : uint
+      := match v with
+         | EmptyString => Nil
+         | String ch v
+           => let rest := to_uint v in
+              (if ascii_beq ch "0"
+               then D0 rest
+               else if ascii_beq ch "1"
+               then D1 rest
+               else if ascii_beq ch "2"
+               then D2 rest
+               else if ascii_beq ch "3"
+               then D3 rest
+               else if ascii_beq ch "4"
+               then D4 rest
+               else if ascii_beq ch "5"
+               then D5 rest
+               else if ascii_beq ch "6"
+               then D6 rest
+               else if ascii_beq ch "7"
+               then D7 rest
+               else if ascii_beq ch "8"
+               then D8 rest
+               else if ascii_beq ch "9"
+               then D9 rest
+               else Nil)
+         end.
+
+    Lemma to_of v : String.to_uint (String.of_uint v) = v.
+    Proof. induction v; cbn; f_equal; trivial. Qed.
+  End String.
+End DecimalHelpers.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Definition decimal_string_of_pos (p : positive) : string
+  := String.of_uint (Pos.to_uint p).
+
+Definition pos_of_decimal_string (s : string) : positive
+  := match N.of_uint (String.to_uint s) with
+     | N0 => 1
+     | Npos p => p
+     end.
+
+(*Lemma pos_of_decimal_string_of_pos (p : positive)
+  : pos_of_decimal_string (decimal_string_of_pos p) = p.
+Proof.
+  cbv [pos_of_decimal_string decimal_string_of_pos].
+  rewrite String.to_of.
+ ...
+Qed.*)
+
+Example decimal_string_of_pos_1 : decimal_string_of_pos 1 = "1" := eq_refl.
+Example decimal_string_of_pos_2 : decimal_string_of_pos 2 = "2" := eq_refl.
+Example decimal_string_of_pos_3 : decimal_string_of_pos 3 = "3" := eq_refl.
+Example decimal_string_of_pos_7 : decimal_string_of_pos 7 = "7" := eq_refl.
+Example decimal_string_of_pos_8 : decimal_string_of_pos 8 = "8" := eq_refl.
+Example decimal_string_of_pos_9 : decimal_string_of_pos 9 = "9" := eq_refl.
+Example decimal_string_of_pos_10 : decimal_string_of_pos 10 = "10" := eq_refl.
+Example decimal_string_of_pos_11 : decimal_string_of_pos 11 = "11" := eq_refl.
+Example decimal_string_of_pos_12 : decimal_string_of_pos 12 = "12" := eq_refl.
+Example decimal_string_of_pos_13 : decimal_string_of_pos 13 = "13" := eq_refl.
+Example decimal_string_of_pos_14 : decimal_string_of_pos 14 = "14" := eq_refl.
+Example decimal_string_of_pos_15 : decimal_string_of_pos 15 = "15" := eq_refl.
+Example decimal_string_of_pos_16 : decimal_string_of_pos 16 = "16" := eq_refl.
diff --git a/src/Util/Strings/Equality.v b/src/Util/Strings/Equality.v
new file mode 100644
index 000000000..2b64c92d6
--- /dev/null
+++ b/src/Util/Strings/Equality.v
@@ -0,0 +1,5 @@
+Require Import Coq.Strings.Ascii Coq.Strings.String.
+Require Import Crypto.Util.Bool.Equality.
+
+Scheme Equality for ascii.
+Scheme Equality for string.
diff --git a/src/Util/Strings/Hex.v b/src/Util/Strings/Hex.v
new file mode 100644
index 000000000..62919901a
--- /dev/null
+++ b/src/Util/Strings/Hex.v
@@ -0,0 +1,219 @@
+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 bool_scope.
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Fixpoint hex_string_of_pos' (p : positive) (rest : string) : string
+  := match p with
+     | 1 => String "1" rest
+     | 2 => String "2" rest
+     | 3 => String "3" rest
+     | 4 => String "4" rest
+     | 5 => String "5" rest
+     | 6 => String "6" rest
+     | 7 => String "7" rest
+     | 8 => String "8" rest
+     | 9 => String "9" rest
+     | 10 => String "a" rest
+     | 11 => String "b" rest
+     | 12 => String "c" rest
+     | 13 => String "d" rest
+     | 14 => String "e" rest
+     | 15 => String "f" rest
+     | p'~0~0~0~0 => hex_string_of_pos' p' (String "0" rest)
+     | p'~0~0~0~1 => hex_string_of_pos' p' (String "1" rest)
+     | p'~0~0~1~0 => hex_string_of_pos' p' (String "2" rest)
+     | p'~0~0~1~1 => hex_string_of_pos' p' (String "3" rest)
+     | p'~0~1~0~0 => hex_string_of_pos' p' (String "4" rest)
+     | p'~0~1~0~1 => hex_string_of_pos' p' (String "5" rest)
+     | p'~0~1~1~0 => hex_string_of_pos' p' (String "6" rest)
+     | p'~0~1~1~1 => hex_string_of_pos' p' (String "7" rest)
+     | p'~1~0~0~0 => hex_string_of_pos' p' (String "8" rest)
+     | p'~1~0~0~1 => hex_string_of_pos' p' (String "9" rest)
+     | p'~1~0~1~0 => hex_string_of_pos' p' (String "a" rest)
+     | p'~1~0~1~1 => hex_string_of_pos' p' (String "b" rest)
+     | p'~1~1~0~0 => hex_string_of_pos' p' (String "c" rest)
+     | p'~1~1~0~1 => hex_string_of_pos' p' (String "d" rest)
+     | p'~1~1~1~0 => hex_string_of_pos' p' (String "e" rest)
+     | p'~1~1~1~1 => hex_string_of_pos' p' (String "f" rest)
+     end.
+Definition hex_string_of_pos (p : positive) : string
+  := String "0" (String "x" (hex_string_of_pos' p "")).
+
+Local Notation default := 1.
+
+Fixpoint pos_of_hex_string' (s : string) (rest : option positive)
+  : option positive
+  := match s with
+     | "" => rest
+     | String ch s'
+       => pos_of_hex_string'
+            s'
+            (if ascii_beq ch "0"
+             then match rest with
+                  | Some p => Some (p~0~0~0~0)
+                  | None => None
+                  end
+             else if ascii_beq ch "1"
+             then match rest with
+                  | Some p => Some (p~0~0~0~1)
+                  | None => Some 1
+                  end
+             else if ascii_beq ch "2"
+             then match rest with
+                  | Some p => Some (p~0~0~1~0)
+                  | None => Some 2
+                  end
+             else if ascii_beq ch "3"
+             then match rest with
+                  | Some p => Some (p~0~0~1~1)
+                  | None => Some 3
+                  end
+             else if ascii_beq ch "4"
+             then match rest with
+                  | Some p => Some (p~0~1~0~0)
+                  | None => Some 4
+                  end
+             else if ascii_beq ch "5"
+             then match rest with
+                  | Some p => Some (p~0~1~0~1)
+                  | None => Some 5
+                  end
+             else if ascii_beq ch "6"
+             then match rest with
+                  | Some p => Some (p~0~1~1~0)
+                  | None => Some 6
+                  end
+             else if ascii_beq ch "7"
+             then match rest with
+                  | Some p => Some (p~0~1~1~1)
+                  | None => Some 7
+                  end
+             else if ascii_beq ch "8"
+             then match rest with
+                  | Some p => Some (p~1~0~0~0)
+                  | None => Some 8
+                  end
+             else if ascii_beq ch "9"
+             then match rest with
+                  | Some p => Some (p~1~0~0~1)
+                  | None => Some 9
+                  end
+             else if ascii_beq ch "a" || ascii_beq ch "A"
+             then match rest with
+                  | Some p => Some (p~1~0~1~0)
+                  | None => Some 10
+                  end
+             else if ascii_beq ch "b" || ascii_beq ch "B"
+             then match rest with
+                  | Some p => Some (p~1~0~1~1)
+                  | None => Some 11
+                  end
+             else if ascii_beq ch "c" || ascii_beq ch "C"
+             then match rest with
+                  | Some p => Some (p~1~1~0~0)
+                  | None => Some 12
+                  end
+             else if ascii_beq ch "d" || ascii_beq ch "D"
+             then match rest with
+                  | Some p => Some (p~1~1~0~1)
+                  | None => Some 13
+                  end
+             else if ascii_beq ch "e" || ascii_beq ch "E"
+             then match rest with
+                  | Some p => Some (p~1~1~1~0)
+                  | None => Some 14
+                  end
+             else if ascii_beq ch "f" || ascii_beq ch "F"
+             then match rest with
+                  | Some p => Some (p~1~1~1~1)
+                  | None => Some 15
+                  end
+             else None)
+     end.
+Definition pos_of_hex_string (s : string) : positive
+  := match s with
+     | String s0 (String sb s)
+       => if ascii_beq s0 "0"
+          then if ascii_beq sb "x"
+               then match pos_of_hex_string' s None with
+                    | Some p => p
+                    | None => default
+                    end
+               else default
+          else default
+     | _ => default
+     end.
+
+Fixpoint pos_hex_app (p q:positive) : positive :=
+  match q with
+  | 1 => p~0~0~0~1
+  | 2 => p~0~0~1~0
+  | 3 => p~0~0~1~1
+  | 4 => p~0~1~0~0
+  | 5 => p~0~1~0~1
+  | 6 => p~0~1~1~0
+  | 7 => p~0~1~1~1
+  | 8 => p~1~0~0~0
+  | 9 => p~1~0~0~1
+  | 10 => p~1~0~1~0
+  | 11 => p~1~0~1~1
+  | 12 => p~1~1~0~0
+  | 13 => p~1~1~0~1
+  | 14 => p~1~1~1~0
+  | 15 => p~1~1~1~1
+  | q~0~0~0~0 => (pos_hex_app p q)~0~0~0~0
+  | q~0~0~0~1 => (pos_hex_app p q)~0~0~0~1
+  | q~0~0~1~0 => (pos_hex_app p q)~0~0~1~0
+  | q~0~0~1~1 => (pos_hex_app p q)~0~0~1~1
+  | q~0~1~0~0 => (pos_hex_app p q)~0~1~0~0
+  | q~0~1~0~1 => (pos_hex_app p q)~0~1~0~1
+  | q~0~1~1~0 => (pos_hex_app p q)~0~1~1~0
+  | q~0~1~1~1 => (pos_hex_app p q)~0~1~1~1
+  | q~1~0~0~0 => (pos_hex_app p q)~1~0~0~0
+  | q~1~0~0~1 => (pos_hex_app p q)~1~0~0~1
+  | q~1~0~1~0 => (pos_hex_app p q)~1~0~1~0
+  | q~1~0~1~1 => (pos_hex_app p q)~1~0~1~1
+  | q~1~1~0~0 => (pos_hex_app p q)~1~1~0~0
+  | q~1~1~0~1 => (pos_hex_app p q)~1~1~0~1
+  | q~1~1~1~0 => (pos_hex_app p q)~1~1~1~0
+  | q~1~1~1~1 => (pos_hex_app p q)~1~1~1~1
+  end.
+
+Fixpoint pos_of_hex_string_of_pos' (p : positive)
+      (base : option positive)
+      (rest : string)
+  : pos_of_hex_string' (hex_string_of_pos' p rest) base
+    = pos_of_hex_string' rest (match base with
+                               | None => Some p
+                               | Some v => Some (pos_hex_app v p)
+                               end).
+Proof.
+  do 4 try destruct p as [p|p|]; destruct base; try reflexivity;
+    cbn; rewrite pos_of_hex_string_of_pos'; reflexivity.
+Qed.
+
+Lemma pos_of_hex_string_of_pos (p : positive)
+  : pos_of_hex_string (hex_string_of_pos p) = p.
+Proof.
+  cbn; rewrite pos_of_hex_string_of_pos'; reflexivity.
+Qed.
+
+Example hex_string_of_pos_1 : hex_string_of_pos 1 = "0x1" := eq_refl.
+Example hex_string_of_pos_2 : hex_string_of_pos 2 = "0x2" := eq_refl.
+Example hex_string_of_pos_3 : hex_string_of_pos 3 = "0x3" := eq_refl.
+Example hex_string_of_pos_7 : hex_string_of_pos 7 = "0x7" := eq_refl.
+Example hex_string_of_pos_8 : hex_string_of_pos 8 = "0x8" := eq_refl.
+Example hex_string_of_pos_9 : hex_string_of_pos 9 = "0x9" := eq_refl.
+Example hex_string_of_pos_10 : hex_string_of_pos 10 = "0xa" := eq_refl.
+Example hex_string_of_pos_11 : hex_string_of_pos 11 = "0xb" := eq_refl.
+Example hex_string_of_pos_12 : hex_string_of_pos 12 = "0xc" := eq_refl.
+Example hex_string_of_pos_13 : hex_string_of_pos 13 = "0xd" := eq_refl.
+Example hex_string_of_pos_14 : hex_string_of_pos 14 = "0xe" := eq_refl.
+Example hex_string_of_pos_15 : hex_string_of_pos 15 = "0xf" := eq_refl.
+Example hex_string_of_pos_16 : hex_string_of_pos 16 = "0x10" := eq_refl.
diff --git a/src/Util/Strings/Octal.v b/src/Util/Strings/Octal.v
new file mode 100644
index 000000000..43f006008
--- /dev/null
+++ b/src/Util/Strings/Octal.v
@@ -0,0 +1,138 @@
+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 oct_string_of_pos' (p : positive) (rest : string) : string
+  := match p with
+     | 1 => String "1" rest
+     | 2 => String "2" rest
+     | 3 => String "3" rest
+     | 4 => String "4" rest
+     | 5 => String "5" rest
+     | 6 => String "6" rest
+     | 7 => String "7" rest
+     | p'~0~0~0 => oct_string_of_pos' p' (String "0" rest)
+     | p'~0~0~1 => oct_string_of_pos' p' (String "1" rest)
+     | p'~0~1~0 => oct_string_of_pos' p' (String "2" rest)
+     | p'~0~1~1 => oct_string_of_pos' p' (String "3" rest)
+     | p'~1~0~0 => oct_string_of_pos' p' (String "4" rest)
+     | p'~1~0~1 => oct_string_of_pos' p' (String "5" rest)
+     | p'~1~1~0 => oct_string_of_pos' p' (String "6" rest)
+     | p'~1~1~1 => oct_string_of_pos' p' (String "7" rest)
+     end.
+Definition oct_string_of_pos (p : positive) : string
+  := String "0" (String "o" (oct_string_of_pos' p "")).
+
+Local Notation default := 1.
+
+Fixpoint pos_of_oct_string' (s : string) (rest : option positive)
+  : option positive
+  := match s with
+     | "" => rest
+     | String ch s'
+       => pos_of_oct_string'
+            s'
+            (if ascii_beq ch "0"
+             then match rest with
+                  | Some p => Some (p~0~0~0)
+                  | None => None
+                  end
+             else if ascii_beq ch "1"
+             then match rest with
+                  | Some p => Some (p~0~0~1)
+                  | None => Some 1
+                  end
+             else if ascii_beq ch "2"
+             then match rest with
+                  | Some p => Some (p~0~1~0)
+                  | None => Some 2
+                  end
+             else if ascii_beq ch "3"
+             then match rest with
+                  | Some p => Some (p~0~1~1)
+                  | None => Some 3
+                  end
+             else if ascii_beq ch "4"
+             then match rest with
+                  | Some p => Some (p~1~0~0)
+                  | None => Some 4
+                  end
+             else if ascii_beq ch "5"
+             then match rest with
+                  | Some p => Some (p~1~0~1)
+                  | None => Some 5
+                  end
+             else if ascii_beq ch "6"
+             then match rest with
+                  | Some p => Some (p~1~1~0)
+                  | None => Some 6
+                  end
+             else if ascii_beq ch "7"
+             then match rest with
+                  | Some p => Some (p~1~1~1)
+                  | None => Some 7
+                  end
+             else None)
+     end.
+Definition pos_of_oct_string (s : string) : positive
+  := match s with
+     | String s0 (String sb s)
+       => if ascii_beq s0 "0"
+          then if ascii_beq sb "o"
+               then match pos_of_oct_string' s None with
+                    | Some p => p
+                    | None => default
+                    end
+               else default
+          else default
+     | _ => default
+     end.
+
+Fixpoint pos_oct_app (p q:positive) : positive :=
+  match q with
+  | 1 => p~0~0~1
+  | 2 => p~0~1~0
+  | 3 => p~0~1~1
+  | 4 => p~1~0~0
+  | 5 => p~1~0~1
+  | 6 => p~1~1~0
+  | 7 => p~1~1~1
+  | q~0~0~0 => (pos_oct_app p q)~0~0~0
+  | q~0~0~1 => (pos_oct_app p q)~0~0~1
+  | q~0~1~0 => (pos_oct_app p q)~0~1~0
+  | q~0~1~1 => (pos_oct_app p q)~0~1~1
+  | q~1~0~0 => (pos_oct_app p q)~1~0~0
+  | q~1~0~1 => (pos_oct_app p q)~1~0~1
+  | q~1~1~0 => (pos_oct_app p q)~1~1~0
+  | q~1~1~1 => (pos_oct_app p q)~1~1~1
+  end.
+
+Fixpoint pos_of_oct_string_of_pos' (p : positive)
+      (base : option positive)
+      (rest : string)
+  : pos_of_oct_string' (oct_string_of_pos' p rest) base
+    = pos_of_oct_string' rest (match base with
+                               | None => Some p
+                               | Some v => Some (pos_oct_app v p)
+                               end).
+Proof.
+  do 3 try destruct p as [p|p|]; destruct base; try reflexivity;
+    cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
+Qed.
+
+Lemma pos_of_oct_string_of_pos (p : positive)
+  : pos_of_oct_string (oct_string_of_pos p) = p.
+Proof.
+  cbn; rewrite pos_of_oct_string_of_pos'; reflexivity.
+Qed.
+
+Example oct_string_of_pos_1 : oct_string_of_pos 1 = "0o1" := eq_refl.
+Example oct_string_of_pos_2 : oct_string_of_pos 2 = "0o2" := eq_refl.
+Example oct_string_of_pos_3 : oct_string_of_pos 3 = "0o3" := eq_refl.
+Example oct_string_of_pos_7 : oct_string_of_pos 7 = "0o7" := eq_refl.
+Example oct_string_of_pos_8 : oct_string_of_pos 8 = "0o10" := eq_refl.