Stream: Coq users

Topic: Binders in theorems


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 17:06):

What does Arguments thm. output?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kenji Maillard (Jun 30 2022 at 17:51):

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

view this post on Zulip Kenji Maillard (Jun 30 2022 at 17:52):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 18:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 30 2022 at 18:20):

Hmmm let's see: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.apply

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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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