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!

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

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

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

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

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

if they are not then it should contradict your hypothesis H

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.

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?

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:

Andrés Goens has marked this topic as resolved.

Last updated: Jun 15 2024 at 05:01 UTC