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.
What does Arguments thm.
output?
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?
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.
BTW, eapply thm
will let you omit more arguments — they'll be replaced by evars, to be instantiated later.
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
what about refine (@thm id id _ _ _ tu _).
?
But looking at the Arguments
part of Print thm.
could indeed help
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.
sorry, I meant About thm.
not Arguments thm.
— brain fart on my part
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
.
in fact, if you know which arguments must be passed explicitly, you could make them all explicit arguments.
Other times I make everything implicit so I can pass everything as named arguments without using with
(since with
only works in some scenarios)
Sorry it it wasn't clear : none of the three arguments I want to pass unnamed are implicit in thm
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.
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
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: Oct 13 2024 at 01:02 UTC