I have a lemma that needs two variables. If I do

```
apply myLemma.
```

I get

Error: Unable to find an instance for the variables

n, tail.

If I do:

```
apply myLemma with (n:=n).
```

I get:

Error: Unable to find an instance for the variable tail.

Is it possible to bind several variables? I have read https://coq.inria.fr/refman/proof-engine/tactics.html#bindings but still it is not clear to me.

What about `apply (myLemma a b)`

?

it says `bindings::=( (ident | natural) := term ) +`

, the `+`

means it can be repeated

I get the following error:

The term "n" has type "Node"

while it is expected to have type

"?n.(children) = ?head :: ?tail /\

is_debugging_tree ?n".

The lemma I want to apply is this:

```
Lemma children_head_of_debugging_tree_are_all_idk: forall (n head:Node) (tail: list Node), children n = head::tail /\ is_debugging_tree n -> are_all_idk head.
```

I guess Coq wants a proof of the hypothesis of the lemma I want to apply?

ohh I see. I did not know how to interpret that plus sign.

The following works:

```
apply myLemma with (n := n) (tail := tail).
```

Thank you @Ana de Almeida Borges @Gaëtan Gilbert !

Roland Coeurjoly Lechuga has marked this topic as resolved.

Just FTR, you can also proceed via `eapply myLemma`

.

Roland Coeurjoly Lechuga said:

I get the following error:

The term "n" has type "Node"

while it is expected to have type

"?n.(children) = ?head :: ?tail /\

is_debugging_tree ?n".The lemma I want to apply is this:

`Lemma children_head_of_debugging_tree_are_all_idk: forall (n head:Node) (tail: list Node), children n = head::tail /\ is_debugging_tree n -> are_all_idk head.`

I guess Coq wants a proof of the hypothesis of the lemma I want to apply?

Yes, it does. If you do `About children_head_of_debugging_tree_are_all_idk`

you will likely see that the first two arguments are implicit (they appear between `[...]`

or between `{...}`

). This is possible because Coq can infer both those arguments from a proof of `children n = head::tail /\ is_debugging_tree n`

and it is often useful because it allows you to be less verbose when providing arguments. In order to make my suggestion work, you would have had to temporarily disable the implicit arguments with an `@`

, so it would be `apply (@children_head_of_debugging_tree_are_all_idk n _ tail)`

. Anyway, this is only one option; as you can see there are alternatives.

Last updated: Jun 14 2024 at 18:01 UTC