From 711c020174dc922d0f45ae7afe28e1c7ea8c9168 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 11 Feb 2018 16:41:03 -0500 Subject: Add string conversions --- _CoqProject | 7 ++ src/Util/Bool/Equality.v | 3 + src/Util/Pos.v | 11 +++ src/Util/Strings/Binary.v | 72 +++++++++++++++ src/Util/Strings/Decimal.v | 219 ++++++++++++++++++++++++++++++++++++++++++++ src/Util/Strings/Equality.v | 5 + src/Util/Strings/Hex.v | 219 ++++++++++++++++++++++++++++++++++++++++++++ src/Util/Strings/Octal.v | 138 ++++++++++++++++++++++++++++ 8 files changed, 674 insertions(+) create mode 100644 src/Util/Bool/Equality.v create mode 100644 src/Util/Pos.v create mode 100644 src/Util/Strings/Binary.v create mode 100644 src/Util/Strings/Decimal.v create mode 100644 src/Util/Strings/Equality.v create mode 100644 src/Util/Strings/Hex.v create mode 100644 src/Util/Strings/Octal.v diff --git a/_CoqProject b/_CoqProject index 41790980e..3af6c47ed 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6466,6 +6466,7 @@ src/Util/NumTheoryUtil.v src/Util/Option.v src/Util/PartiallyReifiedProp.v src/Util/PointedProp.v +src/Util/Pos.v src/Util/Prod.v src/Util/QUtil.v src/Util/Relations.v @@ -6481,6 +6482,7 @@ src/Util/WordUtil.v src/Util/ZBounded.v src/Util/ZRange.v src/Util/ZUtil.v +src/Util/Bool/Equality.v src/Util/Bool/IsTrue.v src/Util/Decidable/Bool2Prop.v src/Util/Decidable/Decidable2Bool.v @@ -6500,6 +6502,11 @@ src/Util/SideConditions/RingPackage.v src/Util/Sigma/Associativity.v src/Util/Sigma/Lift.v src/Util/Sigma/MapProjections.v +src/Util/Strings/Binary.v +src/Util/Strings/Decimal.v +src/Util/Strings/Equality.v +src/Util/Strings/Hex.v +src/Util/Strings/Octal.v src/Util/Tactics/BreakMatch.v src/Util/Tactics/CacheTerm.v src/Util/Tactics/ChangeInAll.v diff --git a/src/Util/Bool/Equality.v b/src/Util/Bool/Equality.v new file mode 100644 index 000000000..217b512b0 --- /dev/null +++ b/src/Util/Bool/Equality.v @@ -0,0 +1,3 @@ +Require Import Coq.Bool.Bool. + +Scheme Equality for bool. diff --git a/src/Util/Pos.v b/src/Util/Pos.v new file mode 100644 index 000000000..67c7cfa35 --- /dev/null +++ b/src/Util/Pos.v @@ -0,0 +1,11 @@ +Require Import Coq.PArith.BinPosDef. + +Local Open Scope positive_scope. +(** Append two sequences *) + +Fixpoint app (p q:positive) : positive := + match q with + | q~0 => (app p q)~0 + | q~1 => (app p q)~1 + | 1 => p~1 + end. 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. -- cgit v1.2.3