What does the tactic constructor do?

Using Coq
1

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 :slight_smile:

2

Hi. I think it is simply synonym to first apply one, and if it fails apply two, and so on until one constructor works. They will be applied in order of definition.
You can already use constructor 2 to mean apply two in this case.

The variant econstructor is the same but it will use eapply.

3

What you said does sound right, but constructor does slightly more in the sense that before trying the apply tactic with the possible terms, saves us the trouble of even finding the type. Would you know of where I can find more details of the constructor tactic? Thanks!

4

Yeah I think it merely looks up the head of the goal and checks it’s an inductive then applies successively the different constructors.
But I don’t know much more than what the doc says, maybe then you would have to look at the ocaml code.