Yann Leray (Jun 30 2022 at 15:57): 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
fas 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 thmwill 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):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.
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).
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: Apr 19 2024 at 22:01 UTC