The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If your inductive type has one constructor, and you know it has [n] arguments, then you can write [let (a1, a2, ..., an) as x' return P x' := x in f a1 a2 ... an] as syntax sugar for [match x as x' return P x' with constructor_name a1 a2 ... an => f a1 a2 ... an end].  If your inductive type has two constructors and you don't care about the arguments to the constructor, you can write [if x then f1 else f2], or [if x as x' return P x' then f1 else f2].  One could imagine generalizations of this syntactic sugar.  Is this what you're looking for?  (In 8.5, you'll be able to use the tactic language to write notations / syntactic sugar.  Combined with dependent subgoals, this will let you run [induction] and extract the induction principle from the resulting proof term.)

Note that having a function [is_inductive : Type -> bool] is already, I think, parametricity-breaking (and it certainly contradicts univalence).

On 7:44am, Tue, Nov 18, 2014 Adam Chlipala <adamc AT csail.mit.edu> wrote:

If you were asking about the tactic language, then we could come up with Ltac wishlist items to pass on to the Coq team.  However, since you're asking about Gallina features, then let me say that I hope core Coq never supports any feature like you suggest, which would be a rather jarring departure from the parametricity features of the logic!

(See http://en.wikipedia.org/wiki/Parametricity .)

However, you can probably use type classes, which aren't part of the core formalized logic, to achieve the effect you're after.  I haven't worked out the details.

On 11/18/2014 07:04 AM, michael.soegtrop AT intel.com wrote:

Dear Coq users,

when I define an inductive type, a set of induction principles is created
automatically by Coq. When I have some term for an inductive type, is there a
way to access its default induction principles from the type term? I am
looking for somethign which works in the term language, not in the tactics
language.

Thanks & best regards,

Michael