one smallest partial equivalence relation for each type

[andres-erbsen]

I wish all types (type families) in the standard library came with a distinguished notions of validity and equivalence, ideally expressed using a partial equivalence relations. For example

nat_per := Logic.eq
prod_per {A B} A_per B_per := fun '(x1, y1) '(x2, y2) => A_per x2 x2 /\ B_per y1 y2
Q_per := fun '(n1, d1) '(n2, d2) => d1 <> 0 /\ d2 <> 0 /\ n1*d2 /\ n2*d1
option_per {T} T_per := fun a b => match a, b with Some x, Some y => T_per x y | None, None => True | _ => False end.
Prop_per := iff
proof_per (P : Prop) := fun pf1 pf2 : P => True
int_per := fun a b => pair_per _ _ (nat_and_sign_of_int a) (nat_and_sign_of_int b)

All this would be proven symmetric and transitive, and also reflexive if they are.

[maximedenes]

Isn't this just a parametricity translation? In any case, I don't think this should be included in the stdlib. We should rather provide a tool that generates such relations. I believe it is being done with Elpi, Mtac2, Ltac2, maybe Template-Coq and others already.

[andres-erbsen]

I think there is value in having these included even if they are auto-generated for some types. I am guessing that if we counted the uses of eqListA from current stdlib, we would find it is rather popular. The most compelling use case IMO is lifting equivalence relations on user-defined types to standard-library containers of these types, for use in specifications of procedures that operate on the elements in the container. If different developments make different variants of these definitions, they will need to be translated between manually.

[gmalecha]

Personally, I'm in favor of this. I'm wondering about the logical conclusion of this though. If you pick an equivalence relation that isn't the same (provably) as libniz equality, then you are going to end up with setoids everywhere in your formalization. I embarked on a deep dive around this in grad school and came up with the realization that it gets really verbose pretty quickly. MathClasses (@spitters and @mattam82) achieves this.

Another way (as far as I understand) is using HITs. Sadly, I haven't heard much clamoring for them lately.

[spitters]

Perhaps the real question here is what should be the intended semantics of stdlib2?
Should it be vanille type theory, HoTT, or perhaps HoTT with classical axioms.

@SkySkimmer is working on an extension of Coq with proof irrelevance, I could imagine that similar techniques would allow an extension of Coq with quotient types.

[maximedenes]

Stdlib2 will be using Coq's theory (not extending it). Of course, some facts about axioms (like the paradoxes in Logic today) will be relevant.

I see work on extensions of the theory (like sProp) as orthogonal, but of course they could lead to some simplifications in the library.

[spitters]

If one is serious about this semantics one should use setoids throughout, at least for structures with possibly non-decidable equality. When the equality can be assumed to be decidable the ssr quotients probably work well.

…

On Sun, Jul 29, 2018 at 2:09 PM, Maxime Dénès ***@***.***> wrote: Stdlib2 will be using Coq's theory (not extending it). Of course, some facts about axioms (like the paradoxes in Logic today) will be relevant. I see work on extensions of the theory (like sProp) as orthogonal, but of course they could lead to some simplifications in the library. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAM2znz6Q_RzporN_PKVm2lAmZY4nkF2ks5uLaYEgaJpZM4UbtPK> .

[maximedenes]

I've heard many reports that setoids don't scale well in terms of performance, so I'm not sure about using them. But we could easily specialize to structures with decidable equality as a first step (which is almost what the current stdlib targets if you exclude real numbers).

[spitters]

I think as long as there is a unified view of what the intended semantics is, that could be a reasonable choice. It would be interesting to see what can be done in practice with the various parametricity, and other translation mechanism. I.e. how much of corn, math classes could be obtained automatically from such a translation. from my phone

…

On Sun, 29 Jul 2018, 14:32 Maxime Dénès, ***@***.***> wrote: I've heard many reports that setoids don't scale well in terms of performance, so I'm not sure about using them. But we could easily specialize to structures with decidable equality as a first step (which is almost what the current stdlib targets if you exclude real numbers). — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#4 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAM2znfWdRJmT7-Uv9RLTnM2oWCHsK1Kks5uLatagaJpZM4UbtPK> .

[gmalecha]

It is essential for stdlib2 to work now, on current versions of Coq (e.g. 8.9+), that isn't a contentious point. I think the question that I am getting at is whether stdlib2 should take current Coq as gospel truth and be implemented with it in mind, or if it should rather be implemented with the spirit of Gallina/Coq in mind. (Currently, my personal answer to this question is the later).

I see HITs as one question around this (though it is a non-issue in the immediate future given the working on 8.9 requirement). There are things that they (to my understanding) simplify dramatically, e.g. quotient types, but Gallina doesn't have them now. Should we (as library writers) say "there would be substantial benefit in adding them" and push for them or should we say "they don't exist now and we're weary to of evolving Gallina". @spitters given your work with them, what are your feelings about them? (though that is a little bit off topic)

Another (more immediate since there are alternatives) instance of this similar question is canonical structures vs type classes. Canonical structures are faster and more precisely defined (big plus there) and type classes (I and others) would argue are substantially easier to use (big plus there). So what is the right way to go? Performance dictates that we go with canonical structures, but type classes provide a simple interface and performance and inference might be able to be improved over time.

[maximedenes]

IMHO the two questions are not really of the same nature: there are no HITs in Coq today, and given the amount of implementation work it represents, and AFAIK has not started (only theory and prototypes are being developed, I believe), it won't be for tomorrow. So stdlib2 has no real choice there.

On the question of canonical structures vs typeclasses, on the other hand, the two options are there, and have been carried out in large libraries. So I think it is one of the missions of stdlib2 to study the pros and cons of each solution, and understand when we want to use each, at least in the scope of stdlib2 itself.

whether stdlib2 should take current Coq as gospel truth and be implemented with it in mind, or if it should rather be implemented with the spirit of Gallina/Coq in mind

Probably something in-between. Like the spirit of Coq in mind, but with a strong sense of reality ;) I want stdlib2 to be well suited for the system as it is (modulo some changes, see the work on plugins and rebindable tactics), even if it's surely not taken as gospel truth :) Of course, the library is expected to evolve with the system...

[gmalecha]

@maximedenes I agree about HITs. They don't exist now, and so there's not really any choice in the matter. stdlib2 will not use them (until they exist, if they ever do).

On the broader aspect, you have good insight into what is feasible for "some changes". At the moment, these changes are at the level of engineering, not at the level of the theory. However, this isn't always the case. One might argue that with some amount of work type classes could be strictly better than canonical structures (or vice versa) does that fit within the scope of "some changes"? Probably not given that the answer is not known, but it might be known to someone.

With setoids (as you pointed out) there is a non-trivial relationship between the theory and the performance. In my past experience with monads, the abstraction (of monads) is amazingly powerful, but the reasoning is crippled without setoids. I would claim (perhaps aggressively) that a monad library without support for setoids is essentially useless. If setoids are expensive, this begs the question about performance vs completeness. Do we include monads because they are so useful and accept slow reasoning about them? Do we exclude monads (leaving them to other libraries) because we can't make them fast? What impact would the later choice have? Would it mean we end up with 3 different (incompatible) definitions of Monad (e.g. what we have now with ExtLib, coq-haskell, etc.)? That seems like it would fracture the libraries, is avoiding that a motivation of stdlib2? If not, why make it standard?

So, this has evolved into a more meta discussion, but it is a discussion worth having if we opt for a monolithic standard library vs a minimal prelude and smaller libraries. Both have benefits and drawbacks.

[Zimmi48]

@gmalecha Coordination efforts to have a shared definition can happen out of the standard library if for some reason it is considered that this definition doesn't have its place in the standard library (either because it is not yet clear what is the right choice, or because it is not of general enough interest, etc). We could aim to have such community-maintained standard library extensions (and then we go back to the question discussed in rocq-community/manifesto#15).