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