Stream: math-comp users

Topic: Second Mathcomp sharing day


view this post on Zulip Cyril Cohen (May 22 2024 at 09:54):

Discourse Bot said:

@CohenCyril (Cyril Cohen) posted in Second Mathcomp sharing day

Dear Rocq/Coq and Mathematical components library users, we are pleased to announce our first "Mathcomp sharing day". On May 29th 2024, From 9am to 5pm Paris time, mathcomp users, from enthusiasts to experts, are welcome to casually meetup online and engage in various activity from contributing to mathcomp (fixing bugs, solving issues, adding features, integrating external developments to mathcomp, etc) to discussions on future directions of mathcomp.
More information here: https://github.com/math-comp/math-comp/wiki/MathcompSharingDays.

view this post on Zulip Cyril Cohen (May 28 2024 at 15:22):

Reminder: this is tomorrow.

view this post on Zulip Reynald Affeldt (May 29 2024 at 10:53):

Is it ok to force push on forms ?

view this post on Zulip Reynald Affeldt (May 29 2024 at 12:02):

We will resume work in one hour (that was commute time and dinner in Japan).

view this post on Zulip Reynald Affeldt (May 29 2024 at 14:44):

@Cyril Cohen Georges gave me a hand to make some progress on rebasing the forms PR but I stopped at the definition of Hermitian forms where the file in MathComp using packed classes and the file in MathComp-Analysis using the [equalify _] machinery seem to diverge.
https://github.com/math-comp/math-comp/pull/207

view this post on Zulip Cyril Cohen (May 29 2024 at 14:52):

Can you point to a specific location (file + line of code)?

view this post on Zulip Reynald Affeldt (May 29 2024 at 15:24):

yes, maybe look at forms.v:440

view this post on Zulip Cyril Cohen (May 30 2024 at 12:42):

What is the problem exactly?

view this post on Zulip Reynald Affeldt (May 30 2024 at 13:14):

Not a really a problem:we were running out of time and the fact that the two forms.v files are taking apparently different formalization strategies prompted a break. We can maybe have a quick chat next week about how to proceed from there if you do not mind.

view this post on Zulip grianneau (May 31 2024 at 10:39):

Thank you for the Mathcomp sharing day!

Some use of ChatGPT was mentioned. It was said that one can get some key steps for a proof by providing well-crafted prompts to ChatGPT.
Can you share an example of good prompt (or sequence of prompts?) that let you get discover some key steps to kill a goal?
(I tried a prompt which I shared in the Webex chat, asking for ways to improve it, it would be nice to get some feedback!)

view this post on Zulip grianneau (May 31 2024 at 10:53):

Concerning the question about the goal:

(K : choiceType) (A : {fset K}) (B : {fset K}) : #|` A `*` B| = #|` A | * #|` B |.

thank you for your hint about using cardsX!
I can get an alternate proof by exploiting this result, however I provide a bijection and it it more complicated that my original proof script.
Maybe there is a better way to use cardsX?
Was there any other question about finmap?


Last updated: Jul 25 2024 at 16:02 UTC