I sometimes have issues applying lemmas with implicit arguments, e.g.

```
Lemma Z_add_bounds {amin a amax bmin b bmax : Z}:
amin <= a <= amax ->
bmin <= b <= bmax ->
amin+bmin <= a+b <= amax+bmax.
```

I want the Z arguments implicit, because I frequently use such lemmas in forward reasoning with existing range hypothesis. Now if I apply this lemma to a goal of the form `l1+l2 <= v1+v2 <= u1+u2`

I get the error `Cannot infer the implicit parameter amin of Z_add_bounds`

. But if I do `apply (@Z_add_bounds)`

, it works fine. I wonder why this is and how others handle implicit arguments for such forward reasoning lemmas.

Those arguments are maximal implicits, you could try non-maximal ones ( [] instead of {} )

Non-maximal means they're not filled in unless you have a subsequent argument

do you have a repro case?

```
Require Import ZArith.
Open Scope Z_scope.
Lemma Z_add_bounds {amin a amax bmin b bmax : Z}:
amin <= a <= amax ->
bmin <= b <= bmax ->
amin+bmin <= a+b <= amax+bmax.
Admitted.
Lemma foo l1 l2 v1 v2 u1 u2 : l1+l2 <= v1+v2 <= u1+u2.
Proof.
apply Z_add_bounds. (* success *)
```

works for me

@Gaëtan Gilbert : it appears to be an Ltac2 issue:

```
Require Import Ltac2.Ltac2.
Require Import ZArith.
Open Scope Z_scope.
Lemma Z_add_bounds {amin a amax bmin b bmax : Z}:
amin <= a <= amax ->
bmin <= b <= bmax ->
amin+bmin <= a+b <= amax+bmax.
Admitted.
Lemma foo l1 l2 v1 v2 u1 u2 : l1+l2 <= v1+v2 <= u1+u2.
Proof.
Fail apply Z_add_bounds.
```

I created https://github.com/coq/coq/issues/15691.

the `apply`

notation in Ltac2/Notations.v is doing `Std.apply true false [fun () => (constr:(Z_add_bounds), Std.NoBindings)] None.`

, I guess it should be `open_constr`

?

Makes sense - I move this topic to Ltac2.

This topic was moved here from #Coq users > apply with implicit arguments by Michael Soegtrop.

@Pierre-Marie Pédrot : what is your take on @Gaëtan Gilbert 's suggestion?

Last updated: Oct 08 2024 at 15:02 UTC