Ascii.eqb and String.eqb

2 files changed, 38 insertions, 0 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 5154b75b3f..51da2cc61b 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -40,6 +40,25 @@ 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.
+
 (** * Conversion between natural numbers modulo 256 and ascii characters *)
 
 (** Auxiliary function that turns a positive into an ascii by
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 2be6618ad6..78268eeed8 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,24 @@ 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.
+
 (** *** Concatenation of strings *)
 
 Reserved Notation "x ++ y" (right associativity, at level 60).