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