Add additional lemmas about {String,Ascii}.eqb

Lemma types and names coppied from [Search Z.eqb].

2 files changed, 30 insertions, 0 deletions

diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 51da2cc61b..31a7fb8ad6 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -59,6 +59,21 @@ Proof.
  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/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).