Better way to add well-founded instance

Stream: general

[AHan]

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]

how is your has_add being supplied to your monomial order?

[Kenny Lau]

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

[AHan]

Ah sorry actually those α should be α →₀ β as I am operating on finsupp
my bad...

[Kenny Lau]

and what instances are on \b?

[Kenny Lau]

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]

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]

I fail to see how \a \to\_0 \b can have a well order

[AHan]

or maybe just consider \b as nat would be better, sorry for confusing.
I'm just trying to prove something on monomials

[AHan]

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]

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

[Kenny Lau]

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

[AHan]

Why won't it satisfy the relation?
For example Lexicographic order on monomials

[Kenny Lau]

never mind, I was wrong

[Kenny Lau]

I suppose you can define a new structure well_order that extends linear_order

[Mario Carneiro]

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

[Mario Carneiro]

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

[AHan]

yes, so I am trying to prove it either with
"well-founded + linear order + monomial order" or with "well-order + monomial order"