Stream: Ltac2

Topic: apply with implicit arguments

Michael Soegtrop (Feb 15 2022 at 17:48):

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.

Paolo Giarrusso (Feb 15 2022 at 18:32):

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

Paolo Giarrusso (Feb 15 2022 at 18:33):

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

Gaëtan Gilbert (Feb 15 2022 at 18:38):

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

Michael Soegtrop (Feb 16 2022 at 10:02):

@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.

Michael Soegtrop (Feb 16 2022 at 10:10):

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

Gaëtan Gilbert (Feb 16 2022 at 10:10):

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?

Michael Soegtrop (Feb 16 2022 at 10:15):

Makes sense - I move this topic to Ltac2.

Notification Bot (Feb 16 2022 at 10:18):

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

Michael Soegtrop (Feb 16 2022 at 10:19):

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

Last updated: Oct 08 2024 at 15:02 UTC