[isabelle-dev] »real« considered harmful

[Tobias Nipkow]

Thank you for reminding me of the "reading" part. My ability to read formulas 
decreases quadratically with their length. Trading in "real_of_int" for "real" 
makes things definitely worse.

I would want to see a concrete figures how much duplication is avoided in the 
current theories and how much additional annotation is needed. Note also that if 
some device helps to make the foundations elegant but complicates the 
applications it can be detrimental if the foundations remain fixed but the 
applications keep growing.

Tobias

On 03/06/2015 10:55, Fabian Immler wrote:
> I think I could live without "real": coercions save a lot of the writing.
> Moreover, the "real_of_foo" abbreviations help to avoid type annotations:
> I suppose that all of the current occurrences of "real" could be replaced with one particular "real_of_foo".
>
> For reading (subgoals etc), one could perhaps think about less obstructive abbreviations like e.g., "real_N" and "real_Z", or "real⇩N" and "real⇩Z".
> But I see that "real_of_foo" is much more uniform and you can immediately read off the type "foo".
>
> Fabian
>
>> Am 03.06.2015 um 10:11 schrieb Tobias Nipkow <nipkow at in.tum.de>:
>>
>> For me the main point of "real" is the ease of writing. If we get rid of some lemma duplications but trade that in for many type annotations, I am not in favour.
>>
>> Tobias
>>
>> On 02/06/2015 20:18, Florian Haftmann wrote:
>>> Dear all,
>>>
>>> recently, I stumbled (once again) over the matter of the »real« conversion.
>>>
>>> There is an inclusion hierarchy (⊆) of numerical types
>>>
>>> 	(num ⊆) nat ⊆ int ⊆ rat ⊆ real ⊆ complex
>>>
>>> We can embed »smaller« into »bigger« types using conversions
>>>
>>> 	(numeral ⊆) of_nat ⊆ of_int ⊆ of_rat ⊆ of_real
>>>
>>> These conversions have solid generic algebraic definitions!
>>>
>>> For historic reasons, there is also the conversion real :: 'a ⇒ real
>>> which is overloaded and can be instantiated to arbitrary types. This
>>> (co)conversion works in the other direction without any algebraic
>>> foundation!
>>>
>>> My impression is that having this conversion is a bad idea. For
>>> illustration have a look at
>>> http://isabelle.in.tum.de/repos/isabelle/file/3d696ccb7fa6/src/HOL/Archimedean_Field.thy#l312
>>> which gives a wonderful generic lemma relating fraction division and
>>> integer division:
>>>
>>> 	»floor (of_int k / of_int l) = k div l«
>>>
>>> Note that the result type of the of_int conversion is polymorphic and
>>> can be instantiated to rat and real likewise!
>>>
>>> In the presence of the »real« conversion, there is a second variant
>>>
>>> 	»floor (real k / real l) = k div l«
>>>
>>> which must be given separately!
>>>
>>> For uniformity it would be much better to have »real« disappear in the
>>> middle run. I see two potential inconveniences at the moment:
>>> * Writing »of_foo« might demand a type annotation on its result in many
>>> cases (n.b. operations of type foo ⇒ 'a are one of the rare cases where
>>> explicit type annotations must be given in terms rather than at »fixes«).
>>> * We have the existing abbreviations »real_of_foo« which have no type
>>> ambiguity, but might seem a little bit verbose.
>>> Anyway, the duplication seems more grivious to me than such syntax issues.
>>>
>>> Any comments?
>>> 	Florian
>>>
>>>
>>>
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150603/cd01a111/attachment.bin>