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?
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.
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?
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
.
Ok, thank you! :)
What about intro f. specialize (stupid f) as H.
(if you don't mind introducing a new hypothesis) ?
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...
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).
@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: Oct 13 2024 at 01:02 UTC