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.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!
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_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: Feb 08 2023 at 23:03 UTC