Kazuhiko Sakaguchi

icon indicating an email [email protected]

icon location Lyon, France icon location Postdoc in the Plume team at CNRS, ENS de Lyon, UCBL, LIP | Interests: interactive theorem proving, formalization of mathematics, and proof by reflection

Results 306 comments of Kazuhiko Sakaguchi

Please keep around old versions of dune

> > Should we announce such archivals elsewhere (for example on the caml-list?)? > > If you want the announcements to be noticed by the Rocq community, the best choice...

Introduce proper (semi)vector space structures to fix the ring and algebra instances on `'End(vT)`

During the MathComp meeting, we agreed that this PR implements the right solution in principle. So, I will add the changelog entry, and then, we need a proper review before...

Generalize the `SemiGroup` instances on `*%g` and `+%R` to `semigroupType` and `addSemigroupType`

This PR breaks infotheo, but I'm not willing to fix it since I recently spent a few hours fixing SSProve and infotheo and I had to compile Rocq, MC, and...

Generalize the `SemiGroup` instances on `*%g` and `+%R` to `semigroupType` and `addSemigroupType`

Thanks @t6s for the overlay.

More Archimedan lemmas

MCA still uses `Num.floor`/`Num.ceil`/`Num.truncn` with `Num.normr` or `absz` in a few places. If `Num.truncn` does not subsume them, we should try to use `Num.bound`. It's defined in `archimedean.v` but currently...

Replace `HB.lock` with `Elpi mlock`

You are right. I checked that HB exports `Elpi mlock` as `HB.lock`. So, my second point does not apply.

Split order.v

Spreading the instance declaration over these files is probably not a good idea from a maintenance perspective. What about introducing new files dedicated to instance declarations? For example, if we...

Split order.v

(Also, these lexicographic and pointwise orders are probably not at all used in MathComp. Isolating them enables more parallel compilation.)

rename `GRing.exp` to `pown`

> I refrained from removing too quickly the `n` in `pown` despite simplifications suggested by positional notations because maybe we do not want to use the shortest notation now in...

rename `GRing.exp` to `pown`

IIRC, the motivation of this change is a name conflict with an `exp` function of type `R -> R -> R` in MCA. ~What about renaming `GRing.exp` (resp. `exprz`) to...