summaryrefslogtreecommitdiff
path: root/theories/Strings
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Strings')
-rw-r--r--theories/Strings/Ascii.v34
-rw-r--r--theories/Strings/BinaryString.v147
-rw-r--r--theories/Strings/HexString.v229
-rw-r--r--theories/Strings/OctalString.v179
-rw-r--r--theories/Strings/String.v34
5 files changed, 623 insertions, 0 deletions
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 5154b75b..31a7fb8a 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -40,6 +40,40 @@ Proof.
decide equality; apply bool_dec.
Defined.
+Local Open Scope lazy_bool_scope.
+
+Definition eqb (a b : ascii) : bool :=
+ match a, b with
+ | Ascii a0 a1 a2 a3 a4 a5 a6 a7,
+ Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
+ Bool.eqb a0 b0 &&& Bool.eqb a1 b1 &&& Bool.eqb a2 b2 &&& Bool.eqb a3 b3
+ &&& Bool.eqb a4 b4 &&& Bool.eqb a5 b5 &&& Bool.eqb a6 b6 &&& Bool.eqb a7 b7
+ end.
+
+Infix "=?" := eqb : char_scope.
+
+Lemma eqb_spec (a b : ascii) : reflect (a = b) (a =? b)%char.
+Proof.
+ destruct a, b; simpl.
+ do 8 (case Bool.eqb_spec; [ intros -> | constructor; now intros [= ] ]).
+ now constructor.
+Qed.
+
+Local Ltac t_eqb :=
+ repeat first [ congruence
+ | progress subst
+ | apply conj
+ | match goal with
+ | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y)
+ end
+ | intro ].
+Lemma eqb_refl x : (x =? x)%char = true. Proof. t_eqb. Qed.
+Lemma eqb_sym x y : (x =? y)%char = (y =? x)%char. Proof. t_eqb. Qed.
+Lemma eqb_eq n m : (n =? m)%char = true <-> n = m. Proof. t_eqb. Qed.
+Lemma eqb_neq x y : (x =? y)%char = false <-> x <> y. Proof. t_eqb. Qed.
+Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb.
+Proof. t_eqb. Qed.
+
(** * Conversion between natural numbers modulo 256 and ascii characters *)
(** Auxiliary function that turns a positive into an ascii by
diff --git a/theories/Strings/BinaryString.v b/theories/Strings/BinaryString.v
new file mode 100644
index 00000000..6df0a917
--- /dev/null
+++ b/theories/Strings/BinaryString.v
@@ -0,0 +1,147 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ascii String.
+Require Import BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Definition ascii_to_digit (ch : ascii) : option N
+ := (if ascii_dec ch "0" then Some 0
+ else if ascii_dec ch "1" then Some 1
+ else None)%N.
+
+Fixpoint pos_bin_app (p q:positive) : positive :=
+ match q with
+ | q~0 => (pos_bin_app p q)~0
+ | q~1 => (pos_bin_app p q)~1
+ | 1 => p~1
+ end.
+
+Module Raw.
+ Fixpoint of_pos (p : positive) (rest : string) : string
+ := match p with
+ | 1 => String "1" rest
+ | p'~0 => of_pos p' (String "0" rest)
+ | p'~1 => of_pos p' (String "1" rest)
+ end.
+
+ Fixpoint to_N (s : string) (rest : N)
+ : N
+ := match s with
+ | "" => rest
+ | String ch s'
+ => to_N
+ s'
+ match ascii_to_digit ch with
+ | Some v => N.add v (N.double rest)
+ | None => N0
+ end
+ end.
+
+ Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+ : to_N (of_pos p rest) base
+ = to_N rest match base with
+ | N0 => N.pos p
+ | Npos v => Npos (pos_bin_app v p)
+ end.
+ Proof.
+ destruct p as [p|p|]; destruct base; try reflexivity;
+ cbn; rewrite to_N_of_pos; reflexivity.
+ Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+ := String "0" (String "b" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+ := match n with
+ | N0 => "0b0"
+ | Npos p => of_pos p
+ end.
+Definition of_Z (z : Z) : string
+ := match z with
+ | Zneg p => String "-" (of_pos p)
+ | Z0 => "0b0"
+ | Zpos p => of_pos p
+ end.
+Definition of_nat (n : nat) : string
+ := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+ := match s with
+ | String s0 (String sb s)
+ => if ascii_dec s0 "0"
+ then if ascii_dec sb "b"
+ then Raw.to_N s N0
+ else N0
+ else N0
+ | _ => N0
+ end.
+Definition to_pos (s : string) : positive
+ := match to_N s with
+ | N0 => 1
+ | Npos p => p
+ end.
+Definition to_Z (s : string) : Z
+ := let '(is_neg, n) := match s with
+ | String s0 s'
+ => if ascii_dec s0 "-"
+ then (true, to_N s')
+ else (false, to_N s)
+ | EmptyString => (false, to_N s)
+ end in
+ match n with
+ | N0 => Z0
+ | Npos p => if is_neg then Zneg p else Zpos p
+ end.
+Definition to_nat (s : string) : nat
+ := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+ : to_N (of_N n)
+ = n.
+Proof.
+ destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma Z_of_of_Z (z : Z)
+ : to_Z (of_Z z)
+ = z.
+Proof.
+ cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+ try reflexivity;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+ : to_nat (of_nat n)
+ = n.
+Proof.
+ cbv [to_nat of_nat];
+ rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+ : to_pos (of_pos p)
+ = p.
+Proof.
+ cbv [of_pos to_pos to_N]; cbn;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0b1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0b10" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0b11" := eq_refl.
+Example of_N_0 : of_N 0 = "0b0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0b0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0b1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0b0" := eq_refl.
diff --git a/theories/Strings/HexString.v b/theories/Strings/HexString.v
new file mode 100644
index 00000000..9ea93c90
--- /dev/null
+++ b/theories/Strings/HexString.v
@@ -0,0 +1,229 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ascii String.
+Require Import BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Local Notation "a || b"
+ := (if a then true else if b then true else false).
+Definition ascii_to_digit (ch : ascii) : option N
+ := (if ascii_dec ch "0" then Some 0
+ else if ascii_dec ch "1" then Some 1
+ else if ascii_dec ch "2" then Some 2
+ else if ascii_dec ch "3" then Some 3
+ else if ascii_dec ch "4" then Some 4
+ else if ascii_dec ch "5" then Some 5
+ else if ascii_dec ch "6" then Some 6
+ else if ascii_dec ch "7" then Some 7
+ else if ascii_dec ch "8" then Some 8
+ else if ascii_dec ch "9" then Some 9
+ else if ascii_dec ch "a" || ascii_dec ch "A" then Some 10
+ else if ascii_dec ch "b" || ascii_dec ch "B" then Some 11
+ else if ascii_dec ch "c" || ascii_dec ch "C" then Some 12
+ else if ascii_dec ch "d" || ascii_dec ch "D" then Some 13
+ else if ascii_dec ch "e" || ascii_dec ch "E" then Some 14
+ else if ascii_dec ch "f" || ascii_dec ch "F" then Some 15
+ else None)%N.
+
+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.
+
+Module Raw.
+ Fixpoint 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 => of_pos p' (String "0" rest)
+ | p'~0~0~0~1 => of_pos p' (String "1" rest)
+ | p'~0~0~1~0 => of_pos p' (String "2" rest)
+ | p'~0~0~1~1 => of_pos p' (String "3" rest)
+ | p'~0~1~0~0 => of_pos p' (String "4" rest)
+ | p'~0~1~0~1 => of_pos p' (String "5" rest)
+ | p'~0~1~1~0 => of_pos p' (String "6" rest)
+ | p'~0~1~1~1 => of_pos p' (String "7" rest)
+ | p'~1~0~0~0 => of_pos p' (String "8" rest)
+ | p'~1~0~0~1 => of_pos p' (String "9" rest)
+ | p'~1~0~1~0 => of_pos p' (String "a" rest)
+ | p'~1~0~1~1 => of_pos p' (String "b" rest)
+ | p'~1~1~0~0 => of_pos p' (String "c" rest)
+ | p'~1~1~0~1 => of_pos p' (String "d" rest)
+ | p'~1~1~1~0 => of_pos p' (String "e" rest)
+ | p'~1~1~1~1 => of_pos p' (String "f" rest)
+ end.
+
+ Fixpoint to_N (s : string) (rest : N)
+ : N
+ := match s with
+ | "" => rest
+ | String ch s'
+ => to_N
+ s'
+ match ascii_to_digit ch with
+ | Some v => N.add v (N.mul 16 rest)
+ | None => N0
+ end
+ end.
+
+ Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+ : to_N (of_pos p rest) base
+ = to_N rest match base with
+ | N0 => N.pos p
+ | Npos v => Npos (pos_hex_app v p)
+ end.
+ Proof.
+ do 4 try destruct p as [p|p|]; destruct base; try reflexivity;
+ cbn; rewrite to_N_of_pos; reflexivity.
+ Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+ := String "0" (String "x" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+ := match n with
+ | N0 => "0x0"
+ | Npos p => of_pos p
+ end.
+Definition of_Z (z : Z) : string
+ := match z with
+ | Zneg p => String "-" (of_pos p)
+ | Z0 => "0x0"
+ | Zpos p => of_pos p
+ end.
+Definition of_nat (n : nat) : string
+ := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+ := match s with
+ | String s0 (String so s)
+ => if ascii_dec s0 "0"
+ then if ascii_dec so "x"
+ then Raw.to_N s N0
+ else N0
+ else N0
+ | _ => N0
+ end.
+Definition to_pos (s : string) : positive
+ := match to_N s with
+ | N0 => 1
+ | Npos p => p
+ end.
+Definition to_Z (s : string) : Z
+ := let '(is_neg, n) := match s with
+ | String s0 s'
+ => if ascii_dec s0 "-"
+ then (true, to_N s')
+ else (false, to_N s)
+ | EmptyString => (false, to_N s)
+ end in
+ match n with
+ | N0 => Z0
+ | Npos p => if is_neg then Zneg p else Zpos p
+ end.
+Definition to_nat (s : string) : nat
+ := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+ : to_N (of_N n)
+ = n.
+Proof.
+ destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma to_Z_of_Z (z : Z)
+ : to_Z (of_Z z)
+ = z.
+Proof.
+ cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+ try reflexivity;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+ : to_nat (of_nat n)
+ = n.
+Proof.
+ cbv [to_nat of_nat];
+ rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+ : to_pos (of_pos p)
+ = p.
+Proof.
+ cbv [of_pos to_pos to_N]; cbn;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0x1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0x2" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0x3" := eq_refl.
+Example of_pos_7 : of_pos 7 = "0x7" := eq_refl.
+Example of_pos_8 : of_pos 8 = "0x8" := eq_refl.
+Example of_pos_9 : of_pos 9 = "0x9" := eq_refl.
+Example of_pos_10 : of_pos 10 = "0xa" := eq_refl.
+Example of_pos_11 : of_pos 11 = "0xb" := eq_refl.
+Example of_pos_12 : of_pos 12 = "0xc" := eq_refl.
+Example of_pos_13 : of_pos 13 = "0xd" := eq_refl.
+Example of_pos_14 : of_pos 14 = "0xe" := eq_refl.
+Example of_pos_15 : of_pos 15 = "0xf" := eq_refl.
+Example of_pos_16 : of_pos 16 = "0x10" := eq_refl.
+Example of_N_0 : of_N 0 = "0x0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0x0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0x1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0x0" := eq_refl.
diff --git a/theories/Strings/OctalString.v b/theories/Strings/OctalString.v
new file mode 100644
index 00000000..fe8cc9aa
--- /dev/null
+++ b/theories/Strings/OctalString.v
@@ -0,0 +1,179 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Import Ascii String.
+Require Import BinNums.
+Import BinNatDef.
+Import BinIntDef.
+Import BinPosDef.
+
+Local Open Scope positive_scope.
+Local Open Scope string_scope.
+
+Definition ascii_to_digit (ch : ascii) : option N
+ := (if ascii_dec ch "0" then Some 0
+ else if ascii_dec ch "1" then Some 1
+ else if ascii_dec ch "2" then Some 2
+ else if ascii_dec ch "3" then Some 3
+ else if ascii_dec ch "4" then Some 4
+ else if ascii_dec ch "5" then Some 5
+ else if ascii_dec ch "6" then Some 6
+ else if ascii_dec ch "7" then Some 7
+ else None)%N.
+
+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.
+
+Module Raw.
+ Fixpoint 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 => of_pos p' (String "0" rest)
+ | p'~0~0~1 => of_pos p' (String "1" rest)
+ | p'~0~1~0 => of_pos p' (String "2" rest)
+ | p'~0~1~1 => of_pos p' (String "3" rest)
+ | p'~1~0~0 => of_pos p' (String "4" rest)
+ | p'~1~0~1 => of_pos p' (String "5" rest)
+ | p'~1~1~0 => of_pos p' (String "6" rest)
+ | p'~1~1~1 => of_pos p' (String "7" rest)
+ end.
+
+ Fixpoint to_N (s : string) (rest : N)
+ : N
+ := match s with
+ | "" => rest
+ | String ch s'
+ => to_N
+ s'
+ match ascii_to_digit ch with
+ | Some v => N.add v (N.mul 8 rest)
+ | None => N0
+ end
+ end.
+
+ Fixpoint to_N_of_pos (p : positive) (rest : string) (base : N)
+ : to_N (of_pos p rest) base
+ = to_N rest match base with
+ | N0 => N.pos p
+ | Npos v => Npos (pos_oct_app v p)
+ end.
+ Proof.
+ do 3 try destruct p as [p|p|]; destruct base; try reflexivity;
+ cbn; rewrite to_N_of_pos; reflexivity.
+ Qed.
+End Raw.
+
+Definition of_pos (p : positive) : string
+ := String "0" (String "o" (Raw.of_pos p "")).
+Definition of_N (n : N) : string
+ := match n with
+ | N0 => "0o0"
+ | Npos p => of_pos p
+ end.
+Definition of_Z (z : Z) : string
+ := match z with
+ | Zneg p => String "-" (of_pos p)
+ | Z0 => "0o0"
+ | Zpos p => of_pos p
+ end.
+Definition of_nat (n : nat) : string
+ := of_N (N.of_nat n).
+
+Definition to_N (s : string) : N
+ := match s with
+ | String s0 (String so s)
+ => if ascii_dec s0 "0"
+ then if ascii_dec so "o"
+ then Raw.to_N s N0
+ else N0
+ else N0
+ | _ => N0
+ end.
+Definition to_pos (s : string) : positive
+ := match to_N s with
+ | N0 => 1
+ | Npos p => p
+ end.
+Definition to_Z (s : string) : Z
+ := let '(is_neg, n) := match s with
+ | String s0 s'
+ => if ascii_dec s0 "-"
+ then (true, to_N s')
+ else (false, to_N s)
+ | EmptyString => (false, to_N s)
+ end in
+ match n with
+ | N0 => Z0
+ | Npos p => if is_neg then Zneg p else Zpos p
+ end.
+Definition to_nat (s : string) : nat
+ := N.to_nat (to_N s).
+
+Lemma to_N_of_N (n : N)
+ : to_N (of_N n)
+ = n.
+Proof.
+ destruct n; [ reflexivity | apply Raw.to_N_of_pos ].
+Qed.
+
+Lemma to_Z_of_Z (z : Z)
+ : to_Z (of_Z z)
+ = z.
+Proof.
+ cbv [of_Z to_Z]; destruct z as [|z|z]; cbn;
+ try reflexivity;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Lemma to_nat_of_nat (n : nat)
+ : to_nat (of_nat n)
+ = n.
+Proof.
+ cbv [to_nat of_nat];
+ rewrite to_N_of_N, Nnat.Nat2N.id; reflexivity.
+Qed.
+
+Lemma to_pos_of_pos (p : positive)
+ : to_pos (of_pos p)
+ = p.
+Proof.
+ cbv [of_pos to_pos to_N]; cbn;
+ rewrite Raw.to_N_of_pos; cbn; reflexivity.
+Qed.
+
+Example of_pos_1 : of_pos 1 = "0o1" := eq_refl.
+Example of_pos_2 : of_pos 2 = "0o2" := eq_refl.
+Example of_pos_3 : of_pos 3 = "0o3" := eq_refl.
+Example of_pos_7 : of_pos 7 = "0o7" := eq_refl.
+Example of_pos_8 : of_pos 8 = "0o10" := eq_refl.
+Example of_N_0 : of_N 0 = "0o0" := eq_refl.
+Example of_Z_0 : of_Z 0 = "0o0" := eq_refl.
+Example of_Z_m1 : of_Z (-1) = "-0o1" := eq_refl.
+Example of_nat_0 : of_nat 0 = "0o0" := eq_refl.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 2be6618a..be9a10c6 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -14,6 +14,7 @@
Require Import Arith.
Require Import Ascii.
+Require Import Bool.
Declare ML Module "string_syntax_plugin".
(** *** Definition of strings *)
@@ -35,6 +36,39 @@ Proof.
decide equality; apply ascii_dec.
Defined.
+Local Open Scope lazy_bool_scope.
+
+Fixpoint eqb s1 s2 : bool :=
+ match s1, s2 with
+ | EmptyString, EmptyString => true
+ | String c1 s1', String c2 s2' => Ascii.eqb c1 c2 &&& eqb s1' s2'
+ | _,_ => false
+ end.
+
+Infix "=?" := eqb : string_scope.
+
+Lemma eqb_spec s1 s2 : Bool.reflect (s1 = s2) (s1 =? s2)%string.
+Proof.
+ revert s2. induction s1; destruct s2; try (constructor; easy); simpl.
+ case Ascii.eqb_spec; simpl; [intros -> | constructor; now intros [= ]].
+ case IHs1; [intros ->; now constructor | constructor; now intros [= ]].
+Qed.
+
+Local Ltac t_eqb :=
+ repeat first [ congruence
+ | progress subst
+ | apply conj
+ | match goal with
+ | [ |- context[eqb ?x ?y] ] => destruct (eqb_spec x y)
+ end
+ | intro ].
+Lemma eqb_refl x : (x =? x)%string = true. Proof. t_eqb. Qed.
+Lemma eqb_sym x y : (x =? y)%string = (y =? x)%string. Proof. t_eqb. Qed.
+Lemma eqb_eq n m : (n =? m)%string = true <-> n = m. Proof. t_eqb. Qed.
+Lemma eqb_neq x y : (x =? y)%string = false <-> x <> y. Proof. t_eqb. Qed.
+Lemma eqb_compat: Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) eqb.
+Proof. t_eqb. Qed.
+
(** *** Concatenation of strings *)
Reserved Notation "x ++ y" (right associativity, at level 60).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 07:17:20 +0000