The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Le jeudi 24 février 2005 à 23:53 +0100, Roland Zumkeller a écrit :
> >   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)"

[...]

> > - Is there another tactic I could use instead of "apply"?
> 
> Not a different tactic, but inference of implicit arguments:
> 
> apply(T _ _ K).

Thanks a lot for this suggestion. It indeed works, without having to
supply all the arguments as in "K: P (f a b)".

> "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).

I'm not sure to understand why "apply T with (1:=K)" could not work like
"apply (T _ _ K)". Or maybe you are talking about a situation a lot more
general than just "apply something with (1:=first) (2:=second) ..."?

I was also suggested off-list to use "Notation" instead of "Definition".
It also works just fine and doesn't require me to always know the number
of "_" I have to put before each theorem in the script. I was wondering
about the complexity of such a change for Coq though. For example,

 -tion b := (f a a).
 -tion c := (f b b).
 -tion d := (f c c).
 -tion e := (f d d).

Does anybody know what the space and time complexities are, depending on
whether "Definition" or "Notation" is used? My non-educated guess would
be that "Definition" leads to a linear behavior, while "Notation" is
exponential. But maybe I'm just overly pessimistic and "Notation" also
has a linear behavior. Which one is it?

Best regards,

Guillaume