This is quickly getting above my head…

- would a constructor for an inductive data type

automatically be recognized as injective like it is

when writing e.g. [injection H0]?

Yes, as in your initial example with `VInt`

. The fact is in Coq *inductive constructors* are not functions, they don’t evaluate to some value, they are rather *term builders*, in that they literally belong to / constitute the representation of a term: and destruction works by pattern matching on (to begin with) the constructor literal name. – IOW, these are *constructors* in the functional programming sense, so lexical constructs, as opposed to *constructors* as operations in the imperative (OO) programming sense.

For more and possibly better explanations, here are a couple of links:

https://stackoverflow.com/questions/32662889/how-do-we-know-all-coq-constructors-are-injective-and-disjoint

https://stackoverflow.com/questions/43762312/are-constructors-in-the-plain-calculus-of-constructions-disjoint-and-injective

More formally: I cannot find a piece of documentation that explicitly says that inductive constructors are “injective and disjoint”, I take it to be sort of inscribed in the details of the calculus, and I suppose this would be the starting point (not for the fainthearted):

https://coq.inria.fr/refman/language/core/inductive.html#inductive-definitions

- would injective things be compatible with the injection tactic?

No, the `injection`

tactic only applies with inductive constructors, as documented here:

https://coq.inria.fr/refman/proofs/writing-proofs/reasoning-inductives.html#coq:tacn.injection

OTOH, I suppose you could write your own tactic, e.g. in **Ltac**, that leverages an available injectivity hypothesis. (Maybe `congruence`

is already it? I am not sure: my point here just is that you can even write your own tactics…)

The reason I was anticipating a specific type-oriented annotation

There are several ways in Coq to approach what I’d lump under “sub-typing”, as well as quite some literature/articles on just that problem: from the top of my head, beside explicit assumptions, some kind of “sigma types” (maybe), modules, records, type classes… and I am far from an expert on any of that, so I’ll just leave it at some keywords.

But if you are new to Coq, IMHO you might be looking too far ahead already, especially considering that (with no exception, as far as I know) whatever more concise there is to express a concept, that concept can always be expressed using / be unfold back to the basic calculus, where its “ultimate meaning” really resides… whence also IMO the importance of not skipping that step in one’s learning.

I’ll close here by mentioning what I believe is a great resource for the practitioner beginning with Coq, the Software Foundations series, I’d say the first book at least:

https://softwarefoundations.cis.upenn.edu

And, for an even gentler introduction, here is a (relatively recent) series of videos that goes with the first chapters of that first book, by Prof. Michael Clarkson:

https://youtube.com/playlist?list=PLre5AT9JnKShFK9l9HYzkZugkJSsXioFs&si=xq6h9cqETxzB2aJe