Discourse Bot said:

@CohenCyril (Cyril Cohen)posted inSecond Mathcomp sharing dayDear 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.

Reminder: this is tomorrow.

Is it ok to force push on forms ?

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

@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

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

yes, maybe look at forms.v:440

What is the problem exactly?

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.

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

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