Stream: Coq users

Topic: ✔ Bind several variables before applying a lemma


view this post on Zulip Roland Coeurjoly Lechuga (Jun 18 2022 at 15:50):

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.

view this post on Zulip Ana de Almeida Borges (Jun 18 2022 at 15:52):

What about apply (myLemma a b)?

view this post on Zulip Gaëtan Gilbert (Jun 18 2022 at 15:58):

it says bindings::=( (ident​ | natural) := term ) +, the + means it can be repeated

view this post on Zulip Roland Coeurjoly Lechuga (Jun 18 2022 at 15:59):

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?

view this post on Zulip Roland Coeurjoly Lechuga (Jun 18 2022 at 16:02):

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 !

view this post on Zulip Notification Bot (Jun 18 2022 at 16:02):

Roland Coeurjoly Lechuga has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Jun 18 2022 at 16:11):

Just FTR, you can also proceed via eapply myLemma.

view this post on Zulip Ana de Almeida Borges (Jun 18 2022 at 16:15):

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: Feb 01 2023 at 12:30 UTC