Re: [isabelle] Ordering of the complex numbers

Dear all,

in developing the JNF library, we respected and utilized the "a >= 0 <--> a is real nonnegative" convention indeed. I'd say there's no other natural way to extend this to a >= b.

Nevertheless, I agree this should be separate from Complex_Main, as I don't know there's enough merit in this ordering alone to convince others. In JNF, the merit is observed only after having conjugate as a class operation and introducing a class assuming "a * conjugate a >= 0" (e.g. the almost preordered field Dominique mentions).

Best regards,

On 2021/08/31 21:57, Manuel Eberl wrote:
I am a bit sceptical about such orphan instances. If two AFP authors
decide to import incompatible instances of such an order, that means
that no future entry can ever import both of these at the same time, and
there is no workaround for this.

I am generally not a big fan of this particular order instance of the
complex numbers for similar reasons as were already discussed, although
I think my opposition is more of a vague "philosophical" nature than
anything practical.

And yes, indeed, I recently had to use a very different ordering on them
(the lexicographic one) in my proof of the Lindemann–Weierstraß theorem.
I decided against introducing an orphan instance there and instead
simply interpreted the "order" locale.

The locale approach gives you almost everything that a class instance
does, except that the notation is not quite as convenient and that you
don't get the "order" sort, of course, so you cannot use constants that
require it.

So, in summary:
– "Pick-and-choose" orphan instances are, in my opinion, a ticking time
bomb and a bad idea.

– Non-canonical instances such as the one suggested in this thread are,
in my opinion, not a great idea, but I am not *absolutely* opposed to
it. However, if one goes down that path, one should at least have one
(and only one) official one. It can be made optional (i.e. an optional
import); we have some other similar "optional" instances, but that has
the disadvantage that it may lead to people rolling their own
"unofficial" instantiations after all.



On 31/08/2021 12:28, Lawrence Paulson wrote:
It should be separate, so that users have the choice whether to use this
ordering, no ordering or possibly some other ordering. We already do
this for lists (Library/List_Lenlexorder.thy vs Library/List_Lexorder.thy).

On 30 Aug 2021, 18:53 +0100, Wenda Li <wl302 at>, wrote:

The only question I have is whether we should include this ordering in
Complex_Main or as a separate theory file (say in HOL-Library) so that
the user can have the freedom to exclude this ordering (assuming most
of complex number users start with Complex_Main).

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.