jsCoq website showcase · jsCoq · Zulip Chat Archive

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?

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.

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.

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?

Karl Palmskog (Sep 18 2021 at 15:55):

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.

Karl Palmskog (Sep 18 2021 at 16:28):

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

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

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?

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?

Karl Palmskog (Sep 18 2021 at 18:34):

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?

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.

Shachar Itzhaky (Sep 18 2021 at 18:38):

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.

Stream: jsCoq

Topic: jsCoq website showcase

Karl Palmskog (Sep 18 2021 at 15:49):