Re: [isabelle-dev] »real« considered harmful
Maybe we should resurrect the idea of using adhoc overloading for the real abbreviation. Florian, does your rework of the generic machinery for syntactic abbreviations include moving more of the adhoc overloading into HOL? Then we could setup real as an adhoc overloaded constant and the proof machinery only sees of_nat, of_int, while the user has still the ability to write real. - Johannes Am Mittwoch, den 03.06.2015, 11:20 +0200 schrieb 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 nip...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
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
Re: [isabelle-dev] Infix syntax for division?
Indeed, the warning sign attached to div can be very helpful. Hence b). Tobias On 02/06/2015 21:10, Jasmin Blanchette wrote: Hi Florian, a) The radical solution: there is only »_ / _« for both field division and euclidean division. How natural is notation like »a / b * b + a mod b = a« then? b) The conservative solution: partial division has »_ div _«, an (the more special) field division »_ / _«. This seems more sensible than the other way round since »_ div _« suggests some kind of »incompleteness«. Any opinions? I’d vote for (b). I also find that “div” suggests some incompleteness. It serves as a warning signal; when you try to prove sum_sq n = n * (n + 1) * (2 * n + 1) div 6 you think twice and rewrite it into 6 * sum_sq n = n * (n + 1) * (2 * n + 1) I believe Maude (another system named after a French female, presumably) even had a different minus operator on “nat” as opposed to the other types. In a formal context, such precision is surely helpful. Indeed, minus is a nasty case for Dmitriy’s coercions. Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
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 nip...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
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 nip...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev smime.p7s Description: S/MIME Cryptographic Signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
