In Rocq, we can define aliases for types or other elements using Definition.

Unfortunately, these aliases often break typeclass resolution and require explicit unfolding within proofs.

In some cases, Notation is an option, but this cannot give non-symbolic names.

Is there a way to give something another name such that it expands trivially within proofs and instance resolution?

In Rocq, we can define aliases for types or other elements using Definition.

Unfortunately, these aliases often break typeclass resolution and require explicit unfolding within proofs.

In some cases, Notation is an option, but this cannot give non-symbolic names.

Is there a way to give something another name such that it expands trivially within proofs and instance resolution?

• coq

• 1 What do you mean by "cannot give non-symbolic names"? – Li-yao Xia Commented Feb 7 at 23:09
• Meaning if you were to write: Notation "foo" := bar (at level 60). you would get the error A notation must include at least one symbol – Jason Carr Commented 2 days ago

2 Answers 2

There is a restricted form of notations, called abbreviations, which don't create new tokens, but are instead parsed as regular names.

Notation new_constant := a_term.
Notation f x y z := (g z x y).

You can also configure typeclass resolution to see through definitions using Typeclasses Transparent foo

https://rocq-prover.org/doc/V8.20.1/refman/addendum/type-classes.html#typeclasses-transparent-typeclasses-opaque