My problem is that reader fails to prove andb_orb when following the book.
I suggest changing the text so that there is no unexpected type-checking failure. For example, either:
Introduce elimTF View-Hint for user-defined reflect.
Define andP' instead of andP, and refer to ssrbool's andP during proof of andb_orb
Hi!
Thank you for writing the book, I enjoy learning from it!
In chapter 5 "Views and Boolean reflection", reader is encouraged to redefine
reflect
(note that in the actual code definition is wrapped in a module): https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L680 then the book redefinesandP
(original code uses the ossrbool.reflect
, while a reader likely uses his own version ofreflect
): https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L728 then the book definesandb_orb
, which relies onelimTF
View-Hint, which is absent from reader-definedreflect
(therefore type-checking fails): https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L777 then the book explains thatelimTF
is necessary (if it didn't, then I'd be totally in the dark about what went wrong :P): https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L815My problem is that reader fails to prove
andb_orb
when following the book. I suggest changing the text so that there is no unexpected type-checking failure. For example, either:elimTF
View-Hint for user-definedreflect
.andP'
instead ofandP
, and refer to ssrbool'sandP
during proof ofandb_orb