Stream: Coq users

Topic: Can we distinguish constructors from functions?


view this post on Zulip Julio Di Egidio (Jan 11 2024 at 10:39):

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?

view this post on Zulip Gaëtan Gilbert (Jan 11 2024 at 10:52):

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

view this post on Zulip Meven Lennon-Bertrand (Jan 11 2024 at 11:39):

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