The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

>   Variable A : Set.
>   Variable f : A -> A -> A.
>   Variable P : A -> Prop.
>   Variable T : forall x y : A, P (f x y) -> P (f y x).
>   Variables a b : A.
>   Definition d := (f a b).
>   Definition e := (f b a).
>   Axiom K : P d.
>   Lemma L : P e.
>   apply T with (1 := K).

>   Error: The term "K" has type "P d" while it is expected to have type 
> "P (f ?7 ?8)"

> - Why does Coq not notice that "d" is "f a b" when trying to match "P 
> d"
> and "P (f ?7 ?8)"?

It seems that Coq translates "apply T with (1 := K)." to something like 
"apply (fun x y => T x y K)." (using meta-variables instead of "normal" 
ones).

> - Is there a way to convince Coq to work a bit harder when applying a
> theorem?

apply T with (1 := K : P (f a b)).

> - Is there another tactic I could use instead of "apply"?

Not a different tactic, but inference of implicit arguments:

apply(T _ _ K).

"apply ... with" cannot always be translated to (and thus not 
implemented by) this mechanism, since there might be arguments that 
cannot be derived, e.g. in apply T with (y := a).

Regards,

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/