## 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

#### 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