Stream: math-comp users

Topic: Quotients

Bas Spitters (Jul 07 2022 at 09:10):

Did anyone port @Cyril Cohen 's quotients to a package for vanilla Coq?
https://perso.crans.org/cohen/work/quotients/
Or should the math-comp version work pleasantly already with something like stdpp/math-classes ?

Cyril Cohen (Jul 07 2022 at 12:29):

Bas Spitters said:

Did anyone port Cyril Cohen 's quotients to a package for vanilla Coq?
https://perso.crans.org/cohen/work/quotients/
Or should the math-comp version work pleasantly already with something like stdpp/math-classes ?

I assume you are talking about https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/generic_quotient.v ?
I do not think it is compatible as of today, because it's not the same inference mechanism and hierarchy to integrate with. I do not know whether anyone tried to port it to another general purpose library.

Paolo Giarrusso (Jul 07 2022 at 12:41):

@Bas Spitters https://gitlab.mpi-sws.org/iris/stdpp/-/issues/120#note_74224 seems relevant (but unfinished/not integrated); but I didn't port everything in the code/paper

Paolo Giarrusso (Jul 07 2022 at 12:43):

I recall on iris's mattermost that people have indeed tried to combine math-comp and stdpp, and indeed it didn't work

Bas Spitters (Jul 07 2022 at 12:49):

Thanks @Paolo Giarrusso
Do we even need to port it from canonical structures to type classes? The two should be compatible, at least according to Enrico and Assia's paper.
Do you know what didn't work?

Paolo Giarrusso (Jul 07 2022 at 13:36):

math-comp and stdpp make different choices on quite a few global settings, but here's a major one: typeclass search uses apply not apply:, and apply does not support canonical structures well, because it uses tactic unification not evarconv. And that's already a problem in Iris's (limited) use of canonical structures (and Robbert once explained he does _not_ follow the math-comp usage). Iris's wiki blames this on https://github.com/coq/coq/issues/6294 — which discusses potential fixes; @Matthieu Sozeau has tried hard to fix this discrepancy "transparently", in the "unifall" project, but it doesn't seem to be happening anytime soon?

Paolo Giarrusso (Jul 07 2022 at 13:56):

I've also heard rumors about failed attempts to use typeclasses in math-comp. The over: and under: tactic seem a response to those failures: they would be unnecessary if setoid rewriting worked, but it uses TC search to find properness proofs.

Pierre-Marie Pédrot (Jul 07 2022 at 13:57):

in theory we could port setoid rewrite to canonical structures, but that's a bit of work and I'm not sure we have a good design sheet (or a corpus of stuff that should work)

Paolo Giarrusso (Jul 07 2022 at 13:59):

do you mean _add_ CSes as a backend, rather than port? you'd either need both versions, or this would be a large breaking change?

Paolo Giarrusso (Jul 07 2022 at 13:59):

many people state Proper instances, without the wrapping vernacular

Pierre-Marie Pédrot (Jul 07 2022 at 14:03):

I mean have a new tactic that is based on CS rather than TC

Paolo Giarrusso (Jul 07 2022 at 14:06):

agreed; but beyond your concerns, this seems potentially questionable as long as unifall is considered on the horizon...

Matthieu Sozeau (Jul 07 2022 at 14:06):

Paolo Giarrusso said:

math-comp and stdpp make different choices on quite a few global settings, but here's a major one: typeclass search uses apply not apply:, and apply does not support canonical structures well, because it uses tactic unification not evarconv. And that's already a problem in Iris's (limited) use of canonical structures (and Robbert once explained he does _not_ follow the math-comp usage). Iris's wiki blames this on https://github.com/coq/coq/issues/6294 — which discusses potential fixes; Matthieu Sozeau has tried hard to fix this discrepancy "transparently", in the "unifall" project, but it doesn't seem to be happening anytime soon?

Indeed, currently unifall is stuck because it appears impossible to emulate the current behavior of apply unification on primitive projections in refine/apply:

Matthieu Sozeau (Jul 07 2022 at 14:10):

The plan is now rather to first fix primitive projections (rather, remove the hard to emulate compatibility layer) before unifall can continue

Pierre Roux (Jul 07 2022 at 14:20):

Paolo Giarrusso said:

I've also heard rumors about failed attempts to use typeclasses in math-comp. The over: and under: tactic seem a response to those failures: they would be unnecessary if setoid rewriting worked, but it uses TC search to find properness proofs.

My understanding is that porting the algebraic hierarchy of MathComp to typeclasses didn't work. Not sure this has anything to do with setoid_rewrite and the under tactic.

Paolo Giarrusso (Jul 07 2022 at 14:26):

that might be a different effort — I'd expect that to work (as shown by math-classes), but be slower in Coq. I thought there were attempts to use _also_ TCs in math-comp based developments, and they didn't work, and setoid rewriting seems an obvious use-case for TCs + CSs.

Pierre Roux (Jul 07 2022 at 14:32):

Well, it seems "slower" here means absolutely unusable for hierarchies with more than a few levels.
About under, I may be wrong but I think it comes more from a design choice than an impossibility to use setoid_rewrite.

Paolo Giarrusso (Jul 07 2022 at 15:50):

agree on performance. If it's a design choice, it might be fine for math-comp itself, but I can certainly think of applications where setoid rewriting is necessary. And I can't imagine that naming Proper instances is very useful for readers...

Cyril Cohen (Jul 07 2022 at 16:29):

The last problems we experienced with mathcomp on TCs experiments (with @Vincent Laporte) three years ago were 1. scheduling problems (which might have been solved meanwhile?) 2. missing keys for guided inference 3. efficiency related to cuts in proof search or in the size of terms (AFAICR)

Cyril Cohen (Jul 07 2022 at 16:30):

At the present time I think the best solution is to use HB which is a DSL which will hopefully allow to change the inference strategy transparently in the longer run.

Paolo Giarrusso (Jul 07 2022 at 17:14):

@Cyril Cohen what was the goal? TCs + CSs or TCs instead of CSs?

Cyril Cohen (Jul 07 2022 at 17:15):

Paolo Giarrusso said:

Cyril Cohen what was the goal? TCs + CSs or TCs instead of CSs?

Just TCs, (the TCs+CSs require both to work and we already know CS work, it could have been the next step)

Cyril Cohen (Jul 07 2022 at 17:16):

The goal was the experiment

Bas Spitters (Jul 08 2022 at 11:15):

Coming back to the original question about quotients. We can just use canonical structures in stdpp/math-classes.
How much interaction do we need between quotients, and say the algebraic hierarchy?
Alternatively, perhaps this should be part of a general redesign of the alg hierarchy based on the HB, but with a backend for type classes.

Cyril Cohen (Jul 08 2022 at 11:23):

Bas Spitters said:

Coming back to the original question about quotients. We can just use canonical structures in stdpp/math-classes.
How much interaction do we need between quotients, and say the algebraic hierarchy?
Alternatively, perhaps this should be part of a general redesign of the alg hierarchy based on the HB, but with a backend for type classes.

The latter is my intention. However a lot of other things need to be worked out before it happens.

Cyril Cohen (Jul 08 2022 at 11:24):

To answer the former question, the (unfortunate) interaction is with, eqtypes, choicetypes, predicates and subtypes from mathcomp.

Bas Spitters (Jul 08 2022 at 11:38):

Thanks @Cyril Cohen would those ( eqtypes, choicetypes, predicates and subtypes ) be isolated enough so that we can add them as CS to a library like stdpp/math-classes?

Cyril Cohen (Jul 08 2022 at 11:40):

Bas Spitters said:

Thanks Cyril Cohen would those ( eqtypes, choicetypes, predicates and subtypes ) be isolated enough so that we can add them as CS to a library like stdpp/math-classes?

I think that would amount to a full rewrite of the associated features, which is the biggest problem in the general redesign

Kazuhiko Sakaguchi (Jul 08 2022 at 11:42):

Cyril Cohen said:

The last problems we experienced with mathcomp on TCs experiments (with Vincent Laporte) three years ago were 1. scheduling problems (which might have been solved meanwhile?) 2. missing keys for guided inference 3. efficiency related to cuts in proof search or in the size of terms (AFAICR)

Some more details on that experiment can be found here: https://youtu.be/qoBC9Qo36FY?t=715

Paolo Giarrusso (Jul 08 2022 at 11:42):

You'd also have to rewrite stdpp, since it already has equivalents for all of those (Countable, Decision, EqDecision, ...)

Paolo Giarrusso (Jul 08 2022 at 11:46):

at least part of stdpp might be seen as a port of (parts of) math-comp to using typeclasses and with some different design choices — for instance, stdpp predicates are always P : A -> Prop, sometimes with proofs of forall x, Decision (P x)

Paolo Giarrusso (Jul 08 2022 at 11:50):

that is why I believe porting quotients might at least be quicker. If those hard problems are all solved, it might become redundant down the line, but that’s far from clear.

Karl Palmskog (Jul 08 2022 at 12:00):

to me the stdpp-MathComp gap seems pretty wide, partly due the predicates-are-not-always-decidable. But it would be nice with better interoperability and sharing nevertheless...

Cyril Cohen (Jul 08 2022 at 12:06):

Karl Palmskog said:

to me the stdpp-MathComp gap seems pretty wide, partly due the predicates-are-not-always-decidable. But it would be nice with better interoperability and sharing nevertheless...

This is the weirdest point of integration between mathcomp and mathcomp analysis btw...

Paolo Giarrusso (Jul 08 2022 at 13:42):

I'm not sure I understand the gap — there's I see the one in idioms but not "mathematically", since { P : A -> Prop | Decision (P x) } and P : A -> bool seem "isomorphic enough"

Paolo Giarrusso (Jul 08 2022 at 13:47):

(edited) AFAICT at least, but clearly I'm no math-comp expert :sweat_smile: , sorry for misphrasing

Cyril Cohen (Jul 08 2022 at 14:22):

Paolo Giarrusso said:

(edited) AFAICT at least, but clearly I'm no math-comp expert :sweat_smile: , sorry for misphrasing

Well they are not ... true || false and (True; inl foo) \/ (False; inr bar) do not behave the same computationally...

Paolo Giarrusso (Jul 08 2022 at 23:51):

I spoke loosely: what I meant that those are both decidable predicates. (And I never construct the sigma type, it’s always curried). bool_decide (P : Prop) {Decision P} : bool produces an actual boolean. and the bool -> Prop coercion goes the other way.

Paolo Giarrusso (Jul 08 2022 at 23:56):

the more interesting question is whether reducing bool_decide P will start reducing proofs — and it shouldn’t if the proofs are sealed in each Decision instance; I do not remember how good decide equality is here.

Last updated: Feb 08 2023 at 07:02 UTC