I’m trying to understand what does the `constructor`

tactic in Coq do. In the documentation, it says “this tactic applies to the goal such that its conclusion is an inductive type”, which I understand it as given the inductive type, the constructor tactic will look for its corresponding constructor to satisfy the goal. How does this work for dependent types? Using this example (which doesn’t make much sense but more to make my point):

`Inductive A : nat -> nat -> Type := | one : A 0 1 | two : A 0 2 | ... | ninetynine : A 9 9.`

and I define the record type:

`Structure foo (n : nat) := { n : nat; m : nat; _ : A n m}.`

and try to prove:

`Theorem p : foo 1.`

In this case `n`

is 1 and thus the subgoal will be `A 1 ?m`

. Thus any constructor from `ten`

to `nineteen`

will fit the bill. And depending on how I arrange my constructors above, the tactic `constructor`

pick the first one that fits the requirements.

Thus my question here is, what exactly is the tactic `constructor`

doing? Is it just merely searching for the constructor that fits the given type? Is there any documentation or OCaml code to explain what `constructor`

does?

Thanks