sig constructor should be called sig_intro and not exist

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#4110
From: @gares
Reported version: 8.5
CC: @amahboubi, @herbelin, @JasonGross

[coqbot]

Comment author: @gares

If one Prints ex and sig to explain the difference, students gets lost because the constructor of ex is called ex_intro while the one of sig is called exist (that is reminiscent of the notation "exists ..." for ex).

For consistency, I think we should rename the constructor of sig.

[coqbot]

Comment author: @herbelin

Indeed, it would be good to have some phase of uniformization of names in Specif.v. This is something we couldn't do in the cleaning phase from Coq 7.X to 8.0 and I will seize the opportunity of this report to list a few questions I have about Specif.v, in the hope to collect further feedback.

• Providing notations for the constructors and projections of sig.

• Similarly, notations for the constructors of projections of sigT are missing. Popular notations are "{{ x , y }}" (using "{" by analogy with the "{" in "{ x : A & P x }"), or "( x ; y )" (by analogy with the notation for prod), as well as ".1" and ".2".

• This raises the question: should we unify prod and sigT, the same way -> is just syntactic sugar for non-dependent forall? By doing so, we would be able to use the same notations for the constructors and projections of prod and sigT, and in particular reusing the notation (t1,...,tn) for sigT. On the opposite side, for the pedagogy of Coq, overloading prod and sigT might be difficult to explain (??). Also, it should be checked that unification will not fail more in practise in hypothetical situations where using prod instead of sigT enforce a non-dependency hint.

• Is sig the right name for what is currently sig? Shouldn't it be called instead "subset", with sigT being the proper notion of sigma-type?

• Shouldn't the second argument of (currently called) exist and existT be implicit too (and actually both arguments A and P be maximally implicit, like for prod)?

• As a start, for instance, what about a model with sig -> subset, exist -> subset_intro (with notation {{ x , y }}), proj1_sig -> wit (or witness), proj2_sig -> prf (or proof), prod identified with sigT with constructor pair (with recursive notation ( x , ... , y)) and projections fst and snd (or proj1 and proj2, with notations .1 and .2)?

One of the reasons these questions were not tackled while moving to 8.x is a lack of resources and consensus. But considering the current dynamic in reforming Coq, maybe something could be now attained.

[coqbot]

Comment author: @gares

I see, the constructor name of sig is not the only thing worth revising.

I'm not so sure such an ample discussion belongs here, maybe a GT session or a coding sprint project?

[coqbot]

Comment author: @herbelin

Either of them is fine to me (with maybe more time at the coding sprint).

One interesting thing to be tested is whether redefining prod as sigT would work smoothly in practice or not.

[By the way, "subtype" could be better than "subset", with possible alternative "specif" (with the intuition that subtype would drop any proof information, while here we just make the second component computationally-irrelevant)].

[coqbot]

Comment author: @JasonGross

Shouldn't the second argument of (currently called) exist and existT be implicit too (and actually both arguments A and P be maximally implicit, like for prod)?

I often find that I have to give the second argument explicitly, even when (anecdotally) it ought to be in the pattern fragment, especially when it involves dependent pattern matches. I can try to remember to post here the next instance of this that I encounter, if that'd be useful. (The first argument never has to be given explicitly.)