The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-11-04 5:17 GMT+01:00 Michael Shulman <shulman AT sandiego.edu>:

Is there any way to get Coq to display function applications using the
traditional mathematician's notation "f(x)", with parentheses around
the argument?  I would be satisfied with a solution that only applied
to functions with a particular domain and codomain.  Coq accepts this
notation, of course, since the parentheses just group the "x"
unnecessarily, but then it displays it as "f x" instead.  I've tried
wrapping both the function and the arguments in dummy inductive types
so that I could define a Notation for the application, but in both
cases I had to declare a Coercion to get the input notation to work,
and apparently the Coercion then overrides the Notation for display as
well.

Context: I'm using Coq to teach an introductory logic class for
mathematicians.  It would be nice if it used the same notation that
they'll see in their textbooks and everywhere else in mathematics.

Ironically, two-variable functions (or more) work fine, if I define
them uncurried (albeit with an extra space): the ordered pair (x,y)
always gets displayed with parentheses so that f applied to it looks
like "f (x,y)".  But I can't figure out any trick for one-variable
functions.

Mike

​I am not sure if this is relevant or not, but you could use some stuff like:

Inductive single (T : Type) := Single : T -> single T.

Inductive pair (T U : Type) := Pair : T -> U -> pair T U.

Inductive triple (T U V : Type) := Triple : T -> U -> V -> triple T U V.

And so on (or even define it recursively as a "tuple : forall n, n_types n -> Type").

And then have a (x) notation for single T type, (x, y) for pair T U type and so on.

Then using and defining "f : single A -> B" instead of "f : A -> B" might do the trick, if you do not fear to box/unbox values.

Then use notations to get "A ⟶ B" for "single A -> B", "A×B ⟶ C" for "pair A B -> C" and so on.

And remember that some mathematic functions are often used without parentheses (the _+_ function, the cos function…), so that you can tell them that "f x y" could be added to these notations for the cases where type setting the right notations is not that easy.

​