Andrés Goens (Aug 09 2021 at 12:18): 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
Ali Caglayan (Aug 09 2021 at 12:44):if they are not then it should contradict your hypothesis H
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: Oct 13 2024 at 01:02 UTC