# Zulip Chat Archive

## Stream: general

### Topic: Better way to add well-founded instance

#### AHan (Feb 24 2019 at 09:49):

Is there any better way to add a well-founded instance ?

I wanted to prove some lemmas by `linear order`

, `monomial order`

(defined as below) and `<`

is well-founded

(```
lean class is_monomial_order (α : Type*) [has_add α] (r : α → α → Prop) :=
(monomial_order : ∀ a b : α, r a b → ∀ c : α, r (c + a) (c + b))
```

)

So something like :

variables {α : Type*} [linear_order α] [is_monomial_order α (≤)] (wf : well_founded ((<) : α → α → Prop))

It's a bit annoying that every time I wanted to use those lemmas I have to explicitly add the well-founded proof

I've tried instance `is_well_order`

:

variables {α : Type*} [linear_order α] [is_monomial_order α (≤)] [is_well_order α ((<) : α → α → Prop) ]

And after realizing `is_well_order`

implies `linear_order`

, I tried the following two ways, but neither of them looks good...

variables {α : Type*} (r : α → α → Prop ) [is_well_order α r] instance : linear_order α := linear_order_of_STO' r variables [mo : is_monomial_order α (≤)]

variables {α : Type*} (r : α → α → Prop ) [is_well_order α r] [mo : is_monomial_order (α →₀ β) (λ x y, x = y ∨ r x y)]

#### Kenny Lau (Feb 24 2019 at 09:52):

how is your `has_add`

being supplied to your monomial order?

#### Kenny Lau (Feb 24 2019 at 09:53):

as in, how does `variables {α : Type*} [linear_order α] [is_monomial_order α (≤)] [is_well_order α ((<) : α → α → Prop) ]`

even type check?

#### AHan (Feb 24 2019 at 09:53):

Ah sorry actually those `α`

should be `α →₀ β`

as I am operating on `finsupp`

my bad...

#### Kenny Lau (Feb 24 2019 at 09:54):

and what instances are on `\b`

?

#### Kenny Lau (Feb 24 2019 at 09:56):

I mean, the only canonically ordered monoids that are well-founded seem to be the limit ordinals, which we don't really care about other than the first one (i.e. `nat`

), so I don't know what you're trying to achieve

#### AHan (Feb 24 2019 at 09:56):

I defined a class

`lean class decidable_canonically_ordered_monoid (α : Type*) extends canonically_ordered_monoid α, decidable_linear_ordered_cancel_comm_monoid α `

`\b`

is of the instance `decidable_canonically_ordered_monoid `

#### Kenny Lau (Feb 24 2019 at 09:56):

I fail to see how `\a \to\_0 \b`

can have a well order

#### AHan (Feb 24 2019 at 10:00):

or maybe just consider `\b`

as `nat`

would be better, sorry for confusing.

I'm just trying to prove something on monomials

#### AHan (Feb 24 2019 at 10:02):

according to wikipedia

"In the case of finitely many variables, well-ordering of a monomial order is equivalent to the conjunction of the following two conditions:

The order is a total order. If u is any monomial then 1 ≤ u ."

And I'm trying to prove this, so the well order of `α →₀ β`

is actually the well order of monomials

#### Kenny Lau (Feb 24 2019 at 10:03):

but it will not satisfy `∀ a b : α, r a b → ∀ c : α, r (c + a) (c + b)`

#### Kenny Lau (Feb 24 2019 at 10:03):

what is "the" well order of `\a \to\_o \b`

?

#### AHan (Feb 24 2019 at 10:06):

Why won't it satisfy the relation?

For example Lexicographic order on monomials

#### Kenny Lau (Feb 24 2019 at 10:07):

never mind, I was wrong

#### Kenny Lau (Feb 24 2019 at 10:08):

I suppose you can define a new structure `well_order`

that extends `linear_order`

#### Mario Carneiro (Feb 24 2019 at 10:10):

monomials are well founded, but they are not well ordered because the order is not total

#### Mario Carneiro (Feb 24 2019 at 10:11):

it's basically the same as asserting that the < order on multiset is well founded

#### AHan (Feb 24 2019 at 10:13):

yes, so I am trying to prove it either with

"well-founded + linear order + monomial order" or with "well-order + monomial order"

Last updated: May 10 2021 at 00:31 UTC