## Stream: new members

### Topic: Get is_linear_order

#### Marcus Rossel (Mar 11 2021 at 15:39):

Is there an easy way of removing the following sorry: ?

import data.nat.basic

@[derive has_le, derive has_lt]
def mass := ℕ

@[ext]
structure object :=
(m : mass)
(n : ℕ)

instance object_le : has_le object := ⟨λ o o', o.m < o'.m ∨ (o.m = o'.m ∧ o.n ≤ o'.n)⟩

instance object_le_linear : is_linear_order object (≤) := sorry


The object structure is basically just an ℕ × ℕ and its ≤ is lexicographic.
I would like to avoid proving reflexivity, transitivity, antisymmetry and totality manually. Is that possible?

docs#lex

#### Marcus Rossel (Mar 11 2021 at 16:58):

Unfortunately I need to keep the structure, so I can't just def object := lex mass ℕ.

#### Mario Carneiro (Mar 11 2021 at 17:02):

docs#linear_order.lift

#### Marcus Rossel (Mar 11 2021 at 17:04):

Mario Carneiro said:

docs#linear_order.lift

I don't understand how to use this. Could you perhaps show an example? :)

#### Marcus Rossel (Mar 11 2021 at 17:10):

Is this the intended use?

def object.to_lex (o : object) : lex ℕ ℕ := (o.m, o.n)
instance : linear_order object := linear_order.lift object.to_lex sorry


#### Mario Carneiro (Mar 11 2021 at 17:12):

import data.nat.basic order.lexicographic

@[derive linear_order]
def mass := ℕ

@[ext]
structure object :=
(m : mass)
(n : ℕ)

instance : linear_order object :=
@linear_order.lift _ (lex mass ℕ) _
(λ o:object, (o.m, o.n)) (by rintro ⟨⟩ ⟨⟩ ⟨⟩; refl)


Last updated: Dec 20 2023 at 11:08 UTC