[isabelle-dev] »real« considered harmful

[Larry Paulson]

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