[isabelle-dev] »real« considered harmful

[Larry Paulson]

This is an unusual case, because this function is not even injective. I would prefer to reserve of_XXX for generic functions, like the existing ones.

I now see that there is another case:

	real :: float => real

This one is injective, and a properly generic function

	of_float :: "real ⇒ 'a::real_algebra_1”

looks easy to define.

Larry

> On 29 Jul 2015, at 15:24, Johannes Hölzl <hoelzl at in.tum.de> wrote:
> 
> I'm fine with it. The only problem maight be that
>  real :: "ereal => real"
> is overloaded in Extended_Real, which is quite often used in Probability
> theory. I can rename it to "of_ereal".
> 
>  - Johannes
> 
> Am Mittwoch, den 29.07.2015, 15:02 +0100 schrieb Larry Paulson:
>> In recent work, I’ve seen again how tricky things are with coercions.
>> We need “real” because it is already used in thousands of places and
>> in many basic lemmas, but it can only do nat=>real and int=>real. If
>> we are working more abstractly, only of_nat and of_int are general
>> enough. It isn’t unusual to find both types of coercions in a single
>> formula, and to make matters worse, their behaviour under
>> simplification isn’t identical. But how can we fix this without
>> breaking thousands of proofs?
>> 
>> I have a suggestion based on the assumption that real :: int=>real is
>> almost never used. (I have previously removed overloading from other
>> functions, and found essentially no uses of the integer version.) If
>> this assumption is correct, we should be able to define real ::
>> nat=>real as an abbreviation for of_nat, so that the two functions are
>> synonymous. Then we could eliminate the existing abbreviation
>> real_of_nat. This should win all around: we keep the name “real”,
>> which is more readable than “of_nat”, and get rid of the overloading.
>> The effect on existing proofs should be modest, especially if we
>> change things to ensure that of_nat is simplified exactly as real is
>> now.
>> 
>> Obviously, the biggest obstacle is likely to be occurrences of real ::
>> int=>real. Any explicit occurrences will immediately be flagged, and
>> can be replaced by of_int.
>> 
>> Views?
>> 
>> Larry
>> 
>>> On 3 Jun 2015, at 12:23, Larry Paulson <lp15 at cam.ac.uk> wrote:
>>> 
>>> The situation regarding coercions has become extremely untidy, and I think it should be cleared up. We have four generic functions:
>>> 
>>> 	of_nat :: nat \<Rightarrow> ‘a::semiring_1
>>> 	of_int :: int \<Rightarrow> ‘a::ring_1
>>> 	of_rat :: rat \<Rightarrow> ‘a:: field_char_0
>>> 	of_real :: real \<Rightarrow> 'a::real_algebra_1
>>> 
>>> With these functions, we can express practically all numeric conversions, and they are based on algebraic principles. There is no need to introduce quadratically many other functions for each possible combination of source and target type. And yet we seem to done that. Why do we need abbreviations such as these?
>>> 
>>> abbreviation real_of_nat :: "nat \<Rightarrow> real”
>>> where "real_of_nat \<equiv> of_nat"
>>> 
>>> abbreviation real_of_int :: "int \<Rightarrow> real”
>>> where "real_of_int \<equiv> of_int"
>>> 
>>> abbreviation real_of_rat :: "rat \<Rightarrow> real”
>>> where "real_of_rat \<equiv> of_rat"
>>> 
>>> abbreviation complex_of_real :: "real \<Rightarrow> complex"
>>> where "complex_of_real \<equiv> of_real"
>>> 
>>> And then why use overloading so that “real” redirects to one of those, which in turn abbreviates one of the original four functions?  Note that "real x = of_nat x” is not an instance of reflexivity, but must be proved using the definition real_of_nat_def. This definition is used 88 times in our HOL development, and it’s also my direct experience of having two different but equivalent coercions complicates proofs.
>>> 
>>> We currently set up automatic coercions in Real.thy as follows:
>>> 
>>> declare [[coercion "of_nat :: nat \<Rightarrow> int"]]
>>> declare [[coercion "real   :: nat \<Rightarrow> real"]]
>>> declare [[coercion "real   :: int \<Rightarrow> real”]
>>> 
>>> And then in Complex.thy as follows:
>>> 
>>> declare [[coercion "of_real :: real \<Rightarrow> complex"]]
>>> declare [[coercion "of_rat :: rat \<Rightarrow> complex"]]
>>> declare [[coercion "of_int :: int \<Rightarrow> complex"]]
>>> declare [[coercion "of_nat :: nat \<Rightarrow> complex”]]
>>> 
>>> This latter version is the correct one, using just the primitive coercions.
>>> 
>>> I think that we should phase out all the derivative coercions in favour of the primitive ones. I know that our complicated system arose by accident, but it would not be that difficult to fix things.
>>> 
>>> Larry
>>> 
>>>> On 3 Jun 2015, at 09:55, Fabian Immler <immler at in.tum.de> 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
>>> 
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 
>