Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] mathematical function notation

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] mathematical function notation


Chronological Thread 
  • From: Clément Pit--Claudel <clement.pit AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] mathematical function notation
  • Date: Tue, 3 Nov 2015 23:45:44 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
  • Ironport-phdr: 9a23:KU+9nhz91y0782bXCy+O+j09IxM/srCxBDY+r6Qd0e4TIJqq85mqBkHD//Il1AaPBtWGragVwLWM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStOU1ZX8iLr60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWZg8O43YaTlIukwYNRiPB5Qz2U5O55iD+u+9w3jXcJczqZb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf5qg==

Hi Mike,

This works for me in 8.4pl4 and trunk:

Notation "f ( x )" := (f x) (at level 1, format "f ( x )").

Definition Linear f := forall x y, f(x + y) = f(x) + f(y).
Print Linear.

(* Linear = fun f : nat -> nat => forall x y : nat, f(x + y) = f(x) +
f(y) *)
(* : (nat -> nat) -> Prop *)

(The format trick should also be useful to remove unwanted spaced in the
multi-arguments case)

Clément.

On 11/03/2015 11:17 PM, Michael Shulman wrote:
> 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
>

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page