Vincent Moreau (Mar 09 2022 at 16:35): 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?
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.
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?
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.
Vincent Moreau (Mar 09 2022 at 16:49):Ok, thank you! :)
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) ?
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...
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).
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: Apr 16 2024 at 18:02 UTC