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 ?

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.

@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

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

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?

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?

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.

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)

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?

many people state `Proper`

instances, without the wrapping vernacular

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

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

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:`

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

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.

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.

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.

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

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)

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.

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

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)

The goal was the experiment

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.

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.

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

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?

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

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

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

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

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.

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

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

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"

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

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

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.

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