ilyasergey / pnp Goto Github PK

There is a bunch of ssr-search-moved warnings:

File "./coq/HTT.v", line 1465, characters 0-18:
Warning: SSReflect's Search command has been moved to the ssrsearch module;
please Require that module if you still want to use SSReflect's Search
command [ssr-search-moved,deprecated]

I guess this is better fixed when there is a Coq release actually disabling the SSReflect style search utility.

COQC solutions/SsrStyle_solutions.v
File "./solutions/SsrStyle_solutions.v", line 170, characters 0-90:
Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
     = true
     : bool
     = false
     : bool

And indeed gorgeous_b is defined using Fixpoint vernacular but it's not recursive:

Fixpoint gorgeous_b n : bool := match n with
 | 1 | 2 | 4 | 7 => false
 | _ => true
 end.

A quick search did not reveal if this was intentional, so feel free to close.

The opam file is supposed to fix the dependencies more formally. And the installation instructions are supposed to look like

opam install ./

We don't have to publish the opam file.

Related issue: #20

Oh, boy, time flies!

It would be really helpful if there was a comparison of PnP with the MathComp book (MCB). Should readers first work through PnP and then move on to MCB, or read them side by side? What material is complementary and what is in both books?

For coq-fcsl-pcm package release v1.3 breaks compatibility with the lower 1.x versions, but there is a workaround:

opam install coq-fcsl-pcm.1.2.0

For coq-htt (the master version builds fine with Coq 8.12, but the opam file does not allow it):

opam install coq-htt --ignore-constraints-on=coq

This should increase discoverability on Github. (I can't add it)

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 redefines andP (original code uses the o ssrbool.reflect, while a reader likely uses his own version of reflect):
https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L728
then the book defines andb_orb, which relies on elimTF View-Hint, which is absent from reader-defined reflect (therefore type-checking fails):
https://github.com/ilyasergey/pnp/blob/master/coq/BoolReflect.v#L777
then the book explains that elimTF 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#L815

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

make clean; make produces the following error message:

Runaway argument?
{y\_'' automatically gives us a way to replace \textit {y} by \textit \ETC.
! File ended while scanning use of \textit .
<inserted text>
                \par
l.94 \include{Rewriting.v}

?

I'm using macOS 10.15.6 Catalina and the following version of pdflatex:

$ pdflatex -v
pdfTeX 3.14159265-2.6-1.40.21 (TeX Live 2020)
kpathsea version 6.3.2
Copyright 2020 Han The Thanh (pdfTeX) et al.
There is NO warranty.  Redistribution of this software is
covered by the terms of both the pdfTeX copyright and
the Lesser GNU General Public License.
For more information about these matters, see the file
named COPYING and the pdfTeX source.
Primary author of pdfTeX: Han The Thanh (pdfTeX) et al.
Compiled with libpng 1.6.37; using libpng 1.6.37
Compiled with zlib 1.2.11; using zlib 1.2.11
Compiled with xpdf version 4.02

There is a bunch of warnings like this one:

COQC solutions/SsrStyle_solutions.v
File "./solutions/SsrStyle_solutions.v", line 1, characters 0-65:
Warning: Notation "[ rel _ _ : _ | _ ]" was already defined with a different
format in scope fun_scope. [notation-incompatible-format,parsing]

Looks like for Coq 8.12 there is no other solution but disable this warning.

The error is

File "./htt/array.v", line 151, characters 0-59:
Error:
In nested Ltac calls to "by (ssrhintarg)" and "done", last call failed.
No applicable tactic.

If I remove by on that line, the proof state is:

1 subgoal
I : finType
T : Type
a : {array I -> T}
f : {ffun I -> T}
V : valid (updi a (fgraph f))
______________________________________(1/1)
[/\ updi a [seq f i | i <- enum I] = updi a [seq f i | i <- enum I], true & #|I| + 0 = #|I|]