Single-constructor inductive properties vs. definitions

Using Coq
1

Suppose that we have a simple “compound” proposition, being in fact a conjunction of several other propositions (think, e.g. of being a non-trivial divisor of n). I can see at least two different methods of formalizing it in Coq. Either we use a direct Definition or we use an inductive proposition with a single constructor.

Are there “best practices” regarding when to use what definition? Are there any notable differences, except perhaps in formalization style? In my experience, it seems that one tends to require inversion quite a lot, and the other unfolding. Otherwise, they are essentially much the same. I have not encountered a good example where I might want to choose one over the other. Is there one?

2

I agree there doesn’t seem to be a significant difference, so it’s really a matter of style. Both styles can be encoded in terms of each other in a straightforward and mechanical way, so the differences can be smoothed out by proper automation.

3

Using inductive types for suitable predicates enables leveraging unification-based automation during rewriting. See the example in section 4.3 in the PnP book.

Another reason some projects use inductive types for properties is to avoid implicit unfolding of definitions, which can make certain tactics perform worse or unpredictably.

2 Likes