[isabelle-dev] »real« considered harmful

[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
>