orders on products

Stream: new members

[Alistair Tucker]

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'?

[Kevin Buzzard]

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

[Kevin Buzzard]

For example this is from TPIL:

open classical
local attribute [instance] prop_decidable

(after prop_decidable has been defined)

[Kevin Buzzard]

"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."

[Alistair Tucker]

Thanks, I'll do that then.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Alistair Tucker]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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