Ascii.eqb and String.eqb

1 files changed, 19 insertions, 0 deletions

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).