Stream: jsCoq

Topic: jsCoq website showcase


view this post on Zulip Karl Palmskog (Sep 18 2021 at 15:49):

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?

view this post on Zulip Karl Palmskog (Sep 18 2021 at 15:50):

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.

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 15:53):

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.

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 15:55):

sqrt2_not_rational is perhaps a bit long for our landing page. Is everything that's there needed?

view this post on Zulip Karl Palmskog (Sep 18 2021 at 15:55):

let me try to minimize it

view this post on Zulip Karl Palmskog (Sep 18 2021 at 16:03):

hmm, I can probably get it down to 100 lines, would that be enough? But it looks very hard to go below that.

view this post on Zulip Karl Palmskog (Sep 18 2021 at 16:28):

96 lines and it looks pretty decent: https://gist.github.com/palmskog/f5c0a97c1aad151056cb8bfc9bb0b3ef

view this post on Zulip Karl Palmskog (Sep 18 2021 at 16:43):

now it at least shows a collection of very basic features of Coq: lia arithmetic solver, sections, custom tactics, induction, ...

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 18:27):

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).

view this post on Zulip Karl Palmskog (Sep 18 2021 at 18:32):

@Shachar Itzhaky maybe easiest if I make a PR to put this in the examples dir then? Should I target the v8.13 or v8.14 branch?

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 18:33):

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?

view this post on Zulip Karl Palmskog (Sep 18 2021 at 18:34):

sure, works on 8.13.2 and 8.14+rc1

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 18:35):

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?

view this post on Zulip Karl Palmskog (Sep 18 2021 at 18:36):

that sounds nice. I will open a draft PR right away, but it will take a little while to add comments.

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 18:38):

Sure np! Thanks a bunch!

view this post on Zulip Shachar Itzhaky (Sep 18 2021 at 18:39):

probably these lemmas don't need too much explanation, maybe just a nice rendition of them in math above the snippet.

view this post on Zulip Karl Palmskog (Sep 19 2021 at 11:24):

PR ready for review now: https://github.com/jscoq/jscoq/pull/253


Last updated: Jan 31 2023 at 11:01 UTC