## Stream: Coq users

### Topic: ✔ Using the standard library's reflection (Bool.reflect)

#### Andrés Goens (Aug 09 2021 at 12:18):

I'm having trouble understanding the `Bool.reflect` class. I understand the concept of reflection as explained in Logic Foundations (e.g. in https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html), but I'm confused about the typeclass implementation in the standard library. How can I take a boolean equality for something that is an instance of `Bool.reflect` and lift it to a proposition?

Perhaps more concretely. Say for strings in the standard library, which are an instance of `Bool.reflect`. How could I prove something like this?

``````Lemma reflect_equality_string (x y : string) (H: String.eqb x y = true) : x = y.
``````

It seems like the two lemmata `Bool.reflect_iff` or `Bool.iff_reflect` should be what allows me to do this, but they don't seem to work and I don't understand why. Can someone help me out here? Thanks!

#### Ali Caglayan (Aug 09 2021 at 12:37):

https://coq.inria.fr/library/Coq.Structures.Equalities.html#EqbSpec

#### Ali Caglayan (Aug 09 2021 at 12:38):

So for strings: https://coq.inria.fr/library/Coq.Strings.String.html#eqb_eq

#### Ali Caglayan (Aug 09 2021 at 12:41):

reflect_iff are specific cases of reflect for the iff boolean operator `<->`

#### Ali Caglayan (Aug 09 2021 at 12:44):

The way the equality lemma for strings work is that they do a `destruct (eqb_spec s1 s2)` leading to two cases. https://github.com/coq/coq/blob/master/theories/Strings/String.v#L73

#### Ali Caglayan (Aug 09 2021 at 12:44):

if they are equal, the the hypothesis proves what you want

#### Andrés Goens (Aug 09 2021 at 13:31):

Thanks for the pointer! So it's not really using the `Bool.reflect` typeclass? Because those (`String.eqb_eq` and `String.eqb_neq` are defined and proved directly for `String.eqb`). I thought somehow that you would get those "automatically" from the typeclass.

#### Paolo Giarrusso (Aug 10 2021 at 00:48):

https://coq.inria.fr/library/Coq.Bool.Bool.html#reflect is not declared as a typeclass. Have you (or the stdlib) made it into one via Existing Class and Existing Instances?

#### Andrés Goens (Aug 10 2021 at 07:42):

you're absolutely right, it's not. I have no idea why I thought it was, I guess I assumed it and didn't really notice it was not the case. Then that settles my confusion, thanks :sweat_smile:

#### Notification Bot (Aug 10 2021 at 07:43):

Andrés Goens has marked this topic as resolved.

Last updated: Feb 08 2023 at 23:03 UTC