Hi, I am currently learning MetaCoq, and I was looking at the `constructor_tac`

example available on the repo https://github.com/MetaCoq/metacoq/blob/coq-8.16/examples/constructor_tac.v .

The tactic `constructor_tac`

does not behave as the usual `constructor`

, as there is no backtracking, typically, it can not solve the following goal that `contructor`

can :

```
Goal {x : bool | x = false }.
unshelve eapply exist.
Fail all: constructor_tac.
all: constructor.
Qed.
```

How could one account for backtracking ?

Also, I was trying to modify the tactic to get not the first constructor of an inductive type but the second one.

So I modified the code by changing a 0 to a 1 as bellow

```
let term := Ast.tApp (Ast.tConstruct ind **1** u) args in
```

Yet, surprisingly, doing so works only for some types. For instance, in the following, it works on sum but not on nat, and I don't really get why

```
Goal False + True + nat.
constructor_tac.
Fail constructor_tac.
Admitted.
```

in

```
let cstrs := Ast.Env.ind_ctors oib in
match cstrs with
| [] => tmFail "no constructor in this inductive type"
| hd :: _ =>
```

`hd`

is the data for the 1st constructor, so the code using only works to build the 1st constructor (and sometimes to build other constructors if their data is similar enough, in this case the code only cares about the number of arguments)

Ha yes right, I forgot to account for that thanks

I have modified the tactic to get the second constructor as follows

```
match cstrs with
| [] => tmFail "no constructor in this inductive type"
| [qh] => tmFail "not enough constructors in this inductive type"
| qd :: hd :: _ =>
let args := cstr_args hd in
let params := firstn qi.(ind_npars) iargs in
let args := (params ++ map (fun _ => Ast.hole) args)%list in
let term := Ast.tApp (Ast.tConstruct ind 1 u) args in
term' <- tmEval all term ;;
tmPrint term' ;;
tmUnquote term'
```

It works perfectly fine for `true + false`

, `bool`

or `list nat`

but for a reason or another, it still does not work `nat`

where it does nothing. (do not bug or fail, just does nothing)

I have tried to print the terms to inspect them, but I can't notice any issue reading them and comparing them.

For `nat`

I get the following, which is basically what I expected :

```
(tApp
(tConstruct
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0
|} 1 []) [tEvar fresh_evar_id []])
```

Are you sure it does nothing? The second constructor of `nat`

is `S : nat -> nat`

so applying it produces the same goal, you can only see the effect with Show Proof or if some other goal depends on the one you're working on

yeah you are completely right, I just wasn't thinking about that

Last updated: Jul 23 2024 at 20:01 UTC