ilyasergey / pnp Goto Github PK
View Code? Open in Web Editor NEWLecture notes for a short course on proving/programming in Coq via SSReflect.
Home Page: https://ilyasergey.net/pnp
License: BSD 2-Clause "Simplified" License
Lecture notes for a short course on proving/programming in Coq via SSReflect.
Home Page: https://ilyasergey.net/pnp
License: BSD 2-Clause "Simplified" License
This should increase discoverability on Github. (I can't add it)
Oh, boy, time flies!
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
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:
elimTF
View-Hint for user-defined reflect
.andP'
instead of andP
, and refer to ssrbool's andP
during proof of andb_orb
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?
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|]
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
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.
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
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.
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.