How can I "specialize" a polymorphic type in Coq?

user_1243445 0
Viewed 39

(Note, my goal is to learn more about Coq, not necessarily solve this particular problem. IRL, I expect I would just refactor to remove the offending type in that situation.)

I have a type defined this way:

Inductive natprod : Type := pair (n1 n2 nat).

I want to make my product type polymorphic, so I now defined

Inductive prod {X Y : Type} : Type := pair (x : X) (y : Y).

However, I can't have both prod and natprod defined in the same module because they both have a constructor pair. But I have a bunch of functions and theorems for natprod, so I don't want to throw away natprod. Instead, I'd like to basically say "When I write natprod, what I mean is prod nat nat."

So I tried this:

Definition natprod := prod nat nat.

However, I get the following error:

Illegal application (Non-functional construction): 
The expression "prod" of type "Type" cannot be applied to the term
 "nat" : "Set"

How can I do what I want to do?

coq
1 Answers

It turns out the issue was that X and Y were defined to be implicit arguments to prod. We can solve this issue by forcing them to be explicit:

Definition natprod := @prod nat nat.

Alternatively,

Notation natprod := (@prod nat nat).

is more like a macro and does not need to be unfolded in proofs.

user_12434450
Related