From a697b20f5013abb834cd9dca3fdef2bee53221ad Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Thu, 8 Mar 2018 18:00:47 +0100
Subject: Ascii.eqb and String.eqb

---
 theories/Strings/String.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

(limited to 'theories/Strings/String.v')

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).
-- 
cgit v1.2.3


From 78f59f94975bcf1ca72110415b741369eb812975 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 11 Jul 2018 04:29:19 -0400
Subject: Add additional lemmas about {String,Ascii}.eqb

Lemma types and names coppied from [Search Z.eqb].
---
 theories/Strings/String.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'theories/Strings/String.v')

diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 78268eeed8..be9a10c6dc 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -54,6 +54,21 @@ Proof.
  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).
-- 
cgit v1.2.3