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/Bool/Bool.v             |  7 +++++++
 theories/Numbers/DecimalString.v | 20 ++++++++++----------
 theories/Strings/Ascii.v         | 19 +++++++++++++++++++
 theories/Strings/String.v        | 19 +++++++++++++++++++
 4 files changed, 55 insertions(+), 10 deletions(-)

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index edf78ed52d..66a82008d8 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -814,3 +814,10 @@ Defined.
 
 (** Reciprocally, from a decidability, we could state a
     [reflect] as soon as we have a [bool_of_sumbool]. *)
+
+(** For instance, we could state the correctness of [Bool.eqb] via [reflect]: *)
+
+Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b').
+Proof.
+ destruct b, b'; now constructor.
+Qed.
diff --git a/theories/Numbers/DecimalString.v b/theories/Numbers/DecimalString.v
index 1a3220f63a..591024baec 100644
--- a/theories/Numbers/DecimalString.v
+++ b/theories/Numbers/DecimalString.v
@@ -94,7 +94,7 @@ Definition int_of_string s :=
  match s with
  | EmptyString => Some (Pos Nil)
  | String a s' =>
-   if ascii_dec a "-" then option_map Neg (uint_of_string s')
+   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
    else option_map Pos (uint_of_string s)
  end.
 
@@ -131,8 +131,8 @@ Proof.
  - unfold int_of_string.
    destruct (string_of_uint d) eqn:Hd.
    + now destruct d.
-   + destruct ascii_dec; subst.
-     * now destruct d.
+   + case Ascii.eqb_spec.
+     * intros ->. now destruct d.
      * rewrite <- Hd, usu; auto.
  - rewrite usu; auto.
 Qed.
@@ -141,8 +141,8 @@ Lemma sis s d :
  int_of_string s = Some d -> string_of_int d = s.
 Proof.
  destruct s; [intros [= <-]| ]; simpl; trivial.
- destruct ascii_dec; subst; simpl.
- - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ case Ascii.eqb_spec.
+ - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
    simpl; f_equal. now apply sus.
  - destruct d; [ | now destruct uint_of_char].
    simpl string_of_int.
@@ -178,7 +178,7 @@ Definition int_of_string s :=
  match s with
  | EmptyString => None
  | String a s' =>
-   if ascii_dec a "-" then option_map Neg (uint_of_string s')
+   if Ascii.eqb a "-" then option_map Neg (uint_of_string s')
    else option_map Pos (uint_of_string s)
  end.
 
@@ -228,8 +228,8 @@ Proof.
    unfold int_of_string.
    destruct (string_of_uint d) eqn:Hd.
    + now destruct d.
-   + destruct ascii_dec; subst.
-     * now destruct d.
+   + case Ascii.eqb_spec.
+     * intros ->. now destruct d.
      * rewrite <- Hd, usu; auto. now intros ->.
  - intros _ H.
    rewrite usu; auto. now intros ->.
@@ -253,8 +253,8 @@ Lemma sis s d :
  int_of_string s = Some d -> string_of_int d = s.
 Proof.
  destruct s; [intros [=]| ]; simpl.
- destruct ascii_dec; subst; simpl.
- - destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
+ case Ascii.eqb_spec.
+ - intros ->. destruct (uint_of_string s) eqn:Hs; simpl; intros [= <-].
    simpl; f_equal. now apply sus.
  - destruct d; [ | now destruct uint_of_char].
    simpl string_of_int.
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).
-- 
cgit v1.2.3


From 8458615318b2b67a38e356d68926a0838b908fe6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 11 Jul 2018 04:14:59 -0400
Subject: Add Extract Inlined Constant directives for {String,Ascii}.eqb

---
 plugins/extraction/ExtrHaskellString.v | 2 ++
 plugins/extraction/ExtrOcamlString.v   | 1 +
 2 files changed, 3 insertions(+)

diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index ac1f6f9130..a4a40d3c5a 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -35,6 +35,8 @@ Extract Inductive ascii => "Prelude.Char"
               (Data.Bits.testBit (Data.Char.ord a) 6)
               (Data.Bits.testBit (Data.Char.ord a) 7))".
 Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)".
+Extract Inlined Constant Ascii.eqb => "(Prelude.==)".
 
 Extract Inductive string => "Prelude.String" [ "([])" "(:)" ].
 Extract Inlined Constant String.string_dec => "(Prelude.==)".
+Extract Inlined Constant String.eqb => "(Prelude.==)".
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 030b486b26..a2a6a8fe67 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -33,6 +33,7 @@ Extract Constant shift =>
  "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
 
 Extract Inlined Constant ascii_dec => "(=)".
+Extract Inlined Constant Ascii.eqb => "(=)".
 
 Extract Inductive string => "char list" [ "[]" "(::)" ].
 
-- 
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/Ascii.v  | 15 +++++++++++++++
 theories/Strings/String.v | 15 +++++++++++++++
 2 files changed, 30 insertions(+)

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


From 7f7e567188ea40fb396c1802224b7290b9e873a3 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 13 Jul 2018 19:11:13 -0400
Subject: Update CHANGES

---
 CHANGES | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index fdd4feb598..9957ad17f7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,15 @@ Tactics
 
 - Tactics and tactic notations now understand the `deprecated` attribute.
 
+Standard Library
+
+- Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,
+  and proved some lemmas about them.  Note that this might cause
+  incompatibilities if you have, e.g., string_scope and Z_scope both
+  open with string_scope on top, and expect `=?` to refer to `Z.eqb`.
+  Solution: wrap `_ =? _` in `(_ =? _)%Z` (or whichever scope you
+  want).
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
@@ -99,7 +108,7 @@ SSReflect
   In particular rule 3 lets one write {x}/v even if v uses the variable x:
   indeed the view is executed before the renaming.
 
-- An empty clear switch is now accepted in intro patterns before a 
+- An empty clear switch is now accepted in intro patterns before a
   view application whenever the view is a variable.
   One can now write {}/v to mean {v}/v.  Remark that {}/x is very similar
   to the idiom {}e for the rewrite tactic (the equation e is used for
-- 
cgit v1.2.3


From 2c96888bd26c293832f442680561fb72f9dc82f5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 16 Jul 2018 09:50:50 -0400
Subject: Add overlay for QuickChick

---
 dev/ci/user-overlays/08063-jasongross-string-eqb.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/08063-jasongross-string-eqb.sh

diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
new file mode 100644
index 0000000000..99a11b9fbf
--- /dev/null
+++ b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then
+    quickchick_CI_BRANCH=fix-for-pr-8063
+    quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick
+fi
-- 
cgit v1.2.3