search

coq / stdlib2

GNU Lesser General Public License v2.1
39 stars 9 forks source link

What should go in the prelude? #3

Open maximedenes opened 6 years ago

maximedenes commented 6 years ago

The prelude is the set of definitions / plugins loaded as soon as Coq starts. I would like to keep it minimal.

I imagine we would like to get at least the -> notation, and maybe a definition of equality.

Should it load ltac? @ppedrot, is Ltac2 meant to become independent of Ltac1? If so, can you say when that is expected to happen?

Zimmi48 commented 6 years ago

I find it interesting that you would prefer a minimal prelude. I think this would also have my preference for teaching purposes. What are your reasons for wanting this?

BTW I believe that most langages have no prelude at all, but of course they have more basic stuff built in.

ppedrot commented 6 years ago

@maximedenes Ltac2 exports a backwards compatibility layer with Ltac1. I guess this could be shipped separately, but for the time being I don't see it making full secession.

andres-erbsen commented 6 years ago

I would like = not to be bound to Logic.eq in prelude, and perhaps not have Logic.eq in prelude at all. Having = picked up as Logic.eq in files where only custom equivalence relations are used (perhaps in type_scope) has been rather annoying to debug. Would it available as Import LeibnizEquality be too much work in cases where Logic.eq is used intentionally?

maximedenes commented 6 years ago

Ltac2 exports a backwards compatibility layer with Ltac1. I guess this could be shipped separately, but for the time being I don't see it making full secession.

@ppedrot I'm not sure I understand the transition strategy you have, then. Wasn't the plan to remove Ltac1 from the codebase at some point? If not, then maybe at least separate the parts on which Ltac2 depends (Ltac1 core or something like that) so that we could remove the rest. And make sure stdlib2 doesn't introduce new dependencies on the part that is not meant to stay.

maximedenes commented 6 years ago

I would like = not to be bound to Logic.eq in prelude, and perhaps not have Logic.eq in prelude at all. Having = picked up as Logic.eq in files where only custom equivalence relations are used (perhaps in type_scope) has been rather annoying to debug. Would it available as Import LeibnizEquality be too much work in cases where Logic.eq is used intentionally?

I haven't made up my mind about eq and =, but I don't find it very wise to reuse the equality symbol for "custom equivalence relations". I rather had in mind examples like HoTT, which interpret equality differently.

andres-erbsen commented 6 years ago

I think = is the natural choice for equality even if it does not coincide with Logic.eq. I agree that one shouldn't define multiple relations on a type and then bind something other than the smallest relation to =. The use case where I would like to have = for is when quantifying over a record that contains a type and an equivalence relation for that type along with a bunch of operations that respect that relation. The relation may not be Logic.eq just for technical reasons, e.g. the type will be instantiated with a sig whose second component is not hprop. Using anything other than = for equality of values of that type seems like needless bloat to me.