Hi guys,

I was wondering if there is any way to distinguish an inductive constructor from just a function, in particular to recover/leverage the *injectivity* of the constructor: e.g. if I Check `S`

, I simply get the function type `nat -> nat`

, and if I want to write a theorem specifically about constructors, the best I seem able to do is add the assumption that a function is injective.

My question here is actually inspired by some recent questions on Discord as well as PA. A slightly broader question is: does it even make sense to look for such a distinction? E.g. does it make sense to write theorems (unless in some meta-theory I guess) about constructors specifically?

the best I seem able to do is add the assumption that a function is injective.

pretty much yes, there is no internal way to say something is a constructor

But you can still make that distinction in the meta, though, and a library like Equations gives you tool to automatically derive the kind of injectivity-like properties for you:

```
From Equations Require Import Equations.
Derive NoConfusion for nat.
(* … NoConfusionPackage_nat is defined *)
(* NoConfusionPackage_nat : NoConfusionPackage nat *)
Print NoConfusionPackage.
(* Includes injectivity of constructors *)
```

Last updated: Jun 23 2024 at 04:03 UTC