Re: [isabelle-dev] »real« considered harmful
Currently we have definition of_real :: real ⇒ 'a::real_algebra_1 where of_real r = scaleR r 1 Maybe of_real could be done another way. And floats could be injected into the rationals. Larry On 29 Jul 2015, at 16:34, Johannes Hölzl hoe...@in.tum.de wrote: Ah, I forgot about real of float. I assume you meant: of_float :: float = 'a::field - Johannes Am Mittwoch, den 29.07.2015, 16:07 +0100 schrieb 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 hoe...@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 l...@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 imm...@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
Re: [isabelle-dev] »real« considered harmful
Ah, I forgot about real of float. I assume you meant: of_float :: float = 'a::field - Johannes Am Mittwoch, den 29.07.2015, 16:07 +0100 schrieb 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 hoe...@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 l...@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 imm...@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
Re: [isabelle-dev] »real« considered harmful
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 hoe...@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 l...@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 imm...@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 ___
Re: [isabelle-dev] »real« considered harmful
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 l...@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 imm...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
