Email Gateway (Aug 18 2022 at 13:14): Email Gateway (Aug 18 2022 at 13:14):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
I just played around a little with the Coq proof assistant and noted the
feature of Coercions
You can spare yourself some typing and improve readability of the input
code by telling the system how to resolve some "typing error" with some
explicit coercion function.
For example when working with locally nameless terms one can use
Coercion bvar : nat >-> exp.
The Coq interpreter then inserts the constructor bvar whenever it
expects an exp but finds a nat instead. So one can write (abs 0) instead
of (abs (bvar 0)). (with abs :: exp => exp)
Can a similar effect be achieved in Isabelle/HOL as well?
smime.p7s
Email Gateway (Aug 18 2022 at 13:14):From: Tobias Nipkow <nipkow@in.tum.de>
Yes, it would be nice to have coercions inserted automatically. But no
such luck in Isabelle.
Tobias
Christian Doczkal wrote:
Email Gateway (Aug 18 2022 at 13:14):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Yes, it would be nice to have coercions inserted automatically. But no
such luck in Isabelle.
Tanks for the reply. Just out of curiosity. Are there any theoretical or
deep technical reasons against having this feature or has this simply
never occurred on a top position on the priorities list?
smime.p7s
Email Gateway (Aug 18 2022 at 13:15):From: Tobias Nipkow <nipkow@in.tum.de>
Christian Doczkal wrote:
Yes, it would be nice to have coercions inserted automatically. But no
such luck in Isabelle.
Tanks for the reply. Just out of curiosity. Are there any theoretical or
deep technical reasons against having this feature or has this simply
never occurred on a top position on the priorities list?
No theoretical problem at all. Practically it is not hard either, and we
have thought about it from time to time.
From a user perspective it can be helpful, but it has it's snags as
well: writing "sin(m+n)", where m,n::int, the system may turn this into
"sin(real(n+m))" or "sin(real m + real n)". Depending on the context,
one may be preferable to the other...
Tobias
Email Gateway (Aug 18 2022 at 13:15):From: Tjark Weber <webertj@in.tum.de>
On Fri, 2009-03-27 at 09:43 +0100, Tobias Nipkow wrote:
Christian Doczkal wrote:
Yes, it would be nice to have coercions inserted automatically. But no
such luck in Isabelle.
"Trueprop" comes close, doesn't it? To me it looks like an invisible
coercion from bool to prop. But I'll admit that I have no idea how it
works internally, or why this can't be made to work for other coercions.
From a user perspective it can be helpful, but it has it's snags as
well: writing "sin(m+n)", where m,n::int, the system may turn this into
"sin(real(n+m))" or "sin(real m + real n)". Depending on the context,
one may be preferable to the other...
One might want to look at algorithms for overload resolution (in Ada/
C++/Java/...).
(Isn't "real (m+n)" equal to "real m + real n" anyway, so that it makes
no difference in the above example?)
Best,
Tjark
Email Gateway (Aug 18 2022 at 13:15):From: Steven Obua <obua@me.com>
If you don't have unification modulo "real (m+n) = real m + real n",
I guess then it can make a difference :-)
Steven
Last updated: May 03 2024 at 08:18 UTC