Stream: Coq users

Topic: Apply refuses to be applied


view this post on Zulip Vincent Moreau (Mar 09 2022 at 16:35):

Hello,
I do not know if it is the correct place to ask a question but I struggle with the following code. I have a lemma of the following form:

Lemma stupid : False -> forall x : nat, x = x.
Proof.
    intros. constructor.
Qed.

(which I simplified here with False instead of the hypothesis I am using).

Now, suppose I want to apply this stupid lemma in an hypothesis, just as in the following proof:

Lemma stupid_applied : False -> True.
Proof.
    intro f. apply stupid in f.

Then, Coq says "Unable to find an instance for the variable x." whereas I was expecting that it just replaces f of type False with a term of type forall x : nat, x = x.

Does anyone know why this behaviour happens?

view this post on Zulip Guillaume Melquiond (Mar 09 2022 at 16:41):

The implementation of apply uses a heuristic and here it tries too hard. Your stupid lemma is a function with two arguments, so apply tries to find both arguments and thus fails. It did not try to partially apply it to one argument only.

view this post on Zulip Vincent Moreau (Mar 09 2022 at 16:44):

Ok, thanks! Do you know if there is a tactic or a way to ask apply to behave in a way that only the first argument is used?

view this post on Zulip Guillaume Melquiond (Mar 09 2022 at 16:46):

I don't think there is any specific tactic. You might need to use low-level stuff, e.g., refine (_ (stupid f)) ; clear f ; intros f.

view this post on Zulip Vincent Moreau (Mar 09 2022 at 16:49):

Ok, thank you! :)

view this post on Zulip Pierre Castéran (Mar 09 2022 at 17:03):

What about intro f. specialize (stupid f) as H. (if you don't mind introducing a new hypothesis) ?

view this post on Zulip Kenji Maillard (Mar 09 2022 at 17:05):

I'm also surprised that intros f%stupid. fail whereas ssreflect counterpart move=> /stupid f. works perfectly. I guess both kind of application do not use the same heuristics...

view this post on Zulip Guillaume Melquiond (Mar 09 2022 at 17:07):

The main benefit of specialize is that it replaces an existing hypothesis. So, it might be better to directly use assert instead of specialize, e.g., assert (H := stupid f).

view this post on Zulip Paolo Giarrusso (Mar 09 2022 at 22:45):

@Kenji Maillard generally, intros etc use tactic unification while ssreflect uses evarconv, and that often causes differences; this case might have further ones :sweat_smile:


Last updated: Feb 01 2023 at 12:30 UTC