search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.83k stars 646 forks source link

Marking record constructor as canonical doesn't work without auxillary definition #15898

Open Alizter opened 2 years ago

Alizter commented 2 years ago

The following record constructor for some reason cannot be declared as Canonical even though an auxiliary definition can.

Record A := Build_A {
  a : nat ;
}.

Fail Canonical Build_A.

Definition Build_A' a := Build_A a.

Canonical Build_A'.

Version

master

gares commented 2 years ago

Being able to define the constructor as canonical covers a very remote use case, which I don't think deserves a shortcut in the syntax. In particular most of the times, it is not what you want, since it corresponds to eta expansion for records, which is another feature.

Alizter commented 2 years ago

The issue here is that the constructor case gets discarded entirely:

https://github.com/coq/coq/blob/b015303103bc1fd3d74bb1bb2c05def91d98b08a/pretyping/structures.ml#L279-L290

Do we not want to allow for constructors of records to become canonical at all? Could you elaborate why this is something we might not want?

gares commented 2 years ago

You should see a CS instance as a good value for a record instance. The value Build_A _ is not what you want. You want Build_A 0 or Build_A 46... The fact that the system errors if you just pass Build_A is a feature. If you really want a "default CS instance" (this is what it is called in the code), then you have to name it.

IMO this behavior saves mistakes. Why did you declare Build_A as canonical in the first place? Is it really what you wanted?