## Stream: jsCoq

### Topic: jsCoq website showcase

#### 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?

#### 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):

let me try to minimize it

#### 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):

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

#### 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):

sure, works on 8.13.2 and 8.14+rc1

#### 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?

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

Sure np! Thanks a bunch!

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

#### Karl Palmskog (Sep 19 2021 at 11:24):

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

Last updated: Sep 09 2024 at 06:02 UTC