Zulip Chat Archive

Stream: general

Topic: Better way to add well-founded instance


view this post on Zulip 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)]

view this post on Zulip Kenny Lau (Feb 24 2019 at 09:52):

how is your has_add being supplied to your monomial order?

view this post on Zulip 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?

view this post on Zulip AHan (Feb 24 2019 at 09:53):

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

view this post on Zulip Kenny Lau (Feb 24 2019 at 09:54):

and what instances are on \b?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 24 2019 at 09:56):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Feb 24 2019 at 10:03):

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

view this post on Zulip Kenny Lau (Feb 24 2019 at 10:03):

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

view this post on Zulip AHan (Feb 24 2019 at 10:06):

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

view this post on Zulip Kenny Lau (Feb 24 2019 at 10:07):

never mind, I was wrong

view this post on Zulip Kenny Lau (Feb 24 2019 at 10:08):

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

view this post on Zulip Mario Carneiro (Feb 24 2019 at 10:10):

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

view this post on Zulip Mario Carneiro (Feb 24 2019 at 10:11):

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

view this post on Zulip 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