my opinion is that jsCoq needs a better "intro" than the MathComp+infprime one. MC/SSR is a lot to take in compared to vanilla Coq. Maybe something like a proof that the square root of two is irrational in plain Coq?
this is the classic formulation (taken from here) which is at least possible to explain in a few sentences:
Theorem sqrt2_not_rational : forall p q : nat, q <> 0 -> p * p = 2 * (q * q) -> False.
Yeah I tend to agree; the original mindset of jsCoq was to flaunt math-comp, but now we have several things going and that proof of infprime can be but one of them. I am in favor of showing some vanilla Coq first. To some people, there is no such thing as Coq without ssreflect... :clown: but definitely not to all people.
sqrt2_not_rational is perhaps a bit long for our landing page. Is everything that's there needed?
let me try to minimize it
hmm, I can probably get it down to 100 lines, would that be enough? But it looks very hard to go below that.
96 lines and it looks pretty decent: https://gist.github.com/palmskog/f5c0a97c1aad151056cb8bfc9bb0b3ef
now it at least shows a collection of very basic features of Coq:
lia arithmetic solver, sections, custom tactics, induction, ...
Cool! Do you want to write some interim explanation of the various lemmas and interesting tactics? You can write them as Coq comments and you can use LaTeX inside (I will convert it to HTML).
@Shachar Itzhaky maybe easiest if I make a PR to put this in the
examples dir then? Should I target the
oh wonderful! You can make the PR with the 8.14 branch, and I will backport it to 8.13 for the website if we see that 8.14 takes too long to get released. I assume the .v works for both versions right?
sure, works on 8.13.2 and 8.14+rc1
I am thinking maybe put the basic lemmas, the ones before the
Section, in a collapsible div that you can skip if you want to get to the core of the proof. Then if you're interested in them you can go back and expand the div. This could be a nice showcase of HTML authoring as well. WDYT?
that sounds nice. I will open a draft PR right away, but it will take a little while to add comments.
Sure np! Thanks a bunch!
probably these lemmas don't need too much explanation, maybe just a nice rendition of them in math above the snippet.
PR ready for review now: https://github.com/jscoq/jscoq/pull/253
Last updated: Feb 22 2024 at 05:02 UTC