## Stream: Coq users

### Topic: Binders in theorems

#### Yann Leray (Jun 30 2022 at 15:57):

How do I know and control how many binders/arguments a theorem takes using `with` in an `apply` ?
In the following example (you can ignore the meaning of the capital letters),

``````Theorem thm :
forall f fs
(Hf : forall s, T (fs s) = f (T s)) (Hfs : forall s, Z s -> Z (fs s)) (Htr : forall t, Z' t -> Z' (f t)),
forall tu: PP t T, (P t T -> Q (f t) (f T)) ->
let s := tu.2.π1 in
(Ps T s -> Qs (f T) (fs s)) ->
QQ (f t) (f T).
``````

the theorem takes in 2 unnamed arguments (`fs` and `tu`) but I would like it to take in `f` as well. If I pass in the 3 arguments named, they are accepted.

#### Paolo Giarrusso (Jun 30 2022 at 17:06):

What does `Arguments thm.` output?

#### Paolo Giarrusso (Jun 30 2022 at 17:08):

If I pass in the 3 arguments named, they are accepted.

I'm not sure what that means, can you give concrete examples? If you are saying that you _can_ pass `f` as well, what is the problem?

#### Paolo Giarrusso (Jun 30 2022 at 17:12):

some info must be missing — `tu` is bound in `Htr` but appears free in `s`'s body — but AFAICT, `apply` will _demand_ `fs`, might demand `tu`, but it can deduce `f`. So `f` could either be optional, or (if `Set Implicit Arguments` is active) it will automatically become an implicit argument.

#### Paolo Giarrusso (Jun 30 2022 at 17:13):

BTW, `eapply thm` will let you omit more arguments — they'll be replaced by evars, to be instantiated later.

#### Yann Leray (Jun 30 2022 at 17:20):

What does `Arguments thm.` output?

It doesn't print anything, I'm not sure what you want.

I'm not sure what that means, can you give concrete examples? If you are saying that you _can_ pass `f` as well, what is the problem?

I want to write `apply thm with id id tu.` so that it works with my goal `QQ t T`, but I can't.
I can however `apply @thm with (f := id) (fs := id) (tu := tu).` (the `@` is just to avoid name collision, I think it's a bug in 8.14 that was since fixed).
Also, `apply @thm with id id tu.` doesn't really do it since it asks for too many arguments (at this point it's easier to name them).

BTW, `eapply thm` will let you omit more arguments — they'll be replaced by evars, to be instantiated later.

That won't work with my goal unfortunately

#### Kenji Maillard (Jun 30 2022 at 17:51):

what about `refine (@thm id id _ _ _ tu _).` ?

#### Kenji Maillard (Jun 30 2022 at 17:52):

But looking at the `Arguments` part of `Print thm.` could indeed help

#### Yann Leray (Jun 30 2022 at 18:07):

`Arguments thm {P Ps Q Qs}%function_scope {Σ Σ' Γ Γ' t T relopt} (_ _ _ _ _)%function_scope _ (_ _)%function_scope` There are quite a lot.
I think my `apply` still looks better than this `refine`, sorry.

#### Paolo Giarrusso (Jun 30 2022 at 18:11):

sorry, I meant `About thm.` not `Arguments thm.` — brain fart on my part

#### Paolo Giarrusso (Jun 30 2022 at 18:13):

instead of `apply @thm with (f := id) (fs := id) (tu := tu)` you can use `apply (thm (implicit_arg_name := argvalue)) with (explicit_arg_name := argvalue)` — basically, the _implicit_ arguments must be passed before `with` and the other ones after `with`.

#### Paolo Giarrusso (Jun 30 2022 at 18:15):

in fact, if you know which arguments must be passed explicitly, you could make them all explicit arguments.

#### Paolo Giarrusso (Jun 30 2022 at 18:15):

Other times I make everything implicit so I can pass everything as named arguments without using `with` (since `with` only works in some scenarios)

#### Yann Leray (Jun 30 2022 at 18:16):

Sorry it it wasn't clear : none of the three arguments I want to pass unnamed are implicit in `thm`

#### Paolo Giarrusso (Jun 30 2022 at 18:20):

Variant `apply term with term+`
Provides apply with explicit instantiations for all dependent premises of the type of term that do not occur in the conclusion and consequently cannot be found by unification. Notice that the collection term+ must be given according to the order of these dependent premises of the type of term.

So `f` cannot be passed with this syntax. Maybe make it implicit and call `apply (thm (f := id)) with id tu.`

#### Paolo Giarrusso (Jun 30 2022 at 18:21):

even better, use `apply (thm id id tu)` after reordering arguments, and just stop using `with`:

``````Theorem thm :
forall f fs (tu: PP t T)
(Hf : forall s, T (fs s) = f (T s)) (Hfs : forall s, Z s -> Z (fs s)) (Htr : forall t, Z' t -> Z' (f t)),
(P t T -> Q (f t) (f T)) ->
let s := tu.2.π1 in
(Ps T s -> Qs (f T) (fs s)) ->
QQ (f t) (f T).
``````

#### Paolo Giarrusso (Jun 30 2022 at 18:22):

that assumes all earlier arguments are implicit — if they aren't, you can force them to be implicit, or make them implicit after the fact with the `Arguments` command — I prefer the former since it's easier to maintain, but it can be inconvenient with section variables

#### Yann Leray (Jun 30 2022 at 18:26):

Thank you for the suggestions. Why did I think the manual didn't explain that, I wonder.
I'll keep this in mind, but since my only special case is with `id` I just made a specialised version.
Thank you all once more

Last updated: Feb 01 2023 at 13:03 UTC