Redefining prod as a record?

Using Coq
1

In my code I enable primitive projections and redefine prod like the following:

Record prod A B := pair { fst: A ; snd: B }.

Full code theories/Defaults.v · master · Molly Stewart-Gallus / Category Fun · GitLab

I need this sort of weirdness because pattern matching on an inductive type has weird behavior. Without this change:

Definition tupleprod '(A, B): Type := A * B.

Has different inference than

Definition tupleprod X: Type := fst X * snd X.

I assume there are good reasons but Coq does not evaluate

let '(a, b) := ab in
a * b

to

(let '(a, b) := ab in a) * (let '(a, b) := ab in b)

Commonly this sort of thing is a problem with functors and heavily dependently typed code.

I assume similar issues might arise with existentials and the subset type but I haven’t run into any yet. Also if I redefine those then I break use of the Program plugin.

Anyhow I just wanted to ask if there was a nicer way of doing this sort of thing and if anyone else has encountered similar issues.

I was also curious exactly how backwards incompatible such a change would be. I know I ran into a few minor issues already.

1 Like
2

Try making a pull request to the Coq standard library. The CI tells you what projects would be broken by this change.

3

All right.

4

Danhit