Stream: Coq users

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


view this post on Zulip 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!

view this post on Zulip Ali Caglayan (Aug 09 2021 at 12:37):

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

view this post on Zulip Ali Caglayan (Aug 09 2021 at 12:38):

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

view this post on Zulip Ali Caglayan (Aug 09 2021 at 12:41):

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

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Aug 09 2021 at 12:44):

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

view this post on Zulip Ali Caglayan (Aug 09 2021 at 12:44):

if they are not then it should contradict your hypothesis H

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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:

view this post on Zulip 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