Zulip Chat Archive

Stream: new members

Topic: orders on products


view this post on Zulip Alistair Tucker (Dec 08 2018 at 19:06):

I want definitions like

instance prod_has_le {α β : Type} [has_le α] [has_le β] : has_le (prod α β) :=
{ le            := λ a b, a.1  b.1  a.2  b.2 }

instance prod_preorder {α β : Type} [preorder α] [preorder β] : preorder (prod α β) :=
{ le_refl       := λ a, le_refl a.1, le_refl a.2,
  le_trans      := λ a b c h₁ h₂, le_trans h₁.1 h₂.1, le_trans h₁.2 h₂.2,
  .. prod_has_le }

instance prod_partial_order {α β : Type} [partial_order α] [partial_order β] : partial_order (prod α β) :=
{ le_antisymm   := λ a b h₁ h₂, prod.ext (le_antisymm h₁.1 h₂.1) (le_antisymm h₁.2 h₂.2),
  .. prod_preorder }

(At the moment just for ℕ × ℕ, Cauchy sequences and contraction mapping theorem, but probably for more later on.)

These don't seem already to be in mathlib, so should I assume there is some good reason to exclude them? And if so, can I use some namespace trick to define them 'locally'?

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 19:08):

I think attribute local instance works for something which is already defined.

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 19:09):

For example this is from TPIL:

open classical
local attribute [instance] prop_decidable

(after prop_decidable has been defined)

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 19:12):

"However, such commands can often be prefixed with the local modifier, which indicates that they only have effect until the current section or namespace is closed, or until the end of the current file."

view this post on Zulip Alistair Tucker (Dec 08 2018 at 19:14):

Thanks, I'll do that then.

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 19:19):

It would not surprise me if there were a trick to do it all in one go. Does local instance... not work?

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 19:19):

Oh! Do you need to import pi_instances or something? Maybe they're there?

view this post on Zulip Alistair Tucker (Dec 08 2018 at 20:52):

Hmm possibly. I didn't know about pi_instances.

import algebra.pi_instances

def a : bool   := λ i, if i then 1 else 2
def b : bool   := λ i, if i then 3 else 4

#check a  b

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 20:54):

import algebra.pi_instances

example {α β : Type} [partial_order α] [partial_order β] :
partial_order (α × β) := by apply_instance -- fails

I thought it might work out of the box. But no.

view this post on Zulip Kevin Buzzard (Dec 08 2018 at 20:55):

Maybe the reason it's not an instance is that some people might want to use lex order in some cases


Last updated: May 06 2021 at 22:13 UTC