Zulip Chat Archive

Stream: Is there code for X?

Topic: Ascending chain conditions


view this post on Zulip Oliver Nash (Dec 18 2020 at 22:45):

I need to use an "ascending chain condition". Poking around, I see we have a large body of excellent stuff on orders so I'm a bit surprised that we seem to have everything except how I usually think about this. Do we have anything like wf_iff_satisfies_acc somewhere:

import order.well_founded
import order.preorder_hom
import order.order_iso_nat

/-- I see we have `rel_embedding.well_founded_iff_no_descending_seq` but can we have this too?
Can we at least have a comment including the phrase "ascending chain" somewhere? -/
def satisfies_acc (α : Type*) [partial_order α] :=  (a :  →ₘ α),  n,  m, n  m  a n = a m

/-- So that we could then add this. Or does this already exists and I can't find it? -/
lemma wf_iff_satisfies_acc (α : Type*) [partial_order α] :
  well_founded ((>) : α  α  Prop)  satisfies_acc α := sorry

view this post on Zulip Oliver Nash (Dec 18 2020 at 22:47):

In addition, do we have anything along the lines of these (which I need):

/-- Do we already have this? Is it sufficiently more useful than `inv_image.wf` to introduce? -/
lemma well_founded_of_embedding {α β : Type*} [partial_order α] [partial_order β]
  (f : α →ₘ β) (hf : function.injective f) (h : well_founded ((>) : β  β  Prop)) :
  well_founded ((>) : α  α  Prop) := sorry

/-- Surely this property has an "official" name; what is it? -/
def is_sup_compact (α : Type*) [complete_lattice α] :=
   (s : set α) (h : s.nonempty), ( a b, a  s  b  s  a  b  s)  (Sup s)  s

/-- Do we already have this? -/
lemma is_sup_compact_of_wf {α : Type*} [complete_lattice α] (h : well_founded ((>) : α  α  Prop)) :
  is_sup_compact α := sorry

view this post on Zulip Johan Commelin (Dec 19 2020 at 06:06):

I think @Aaron Anderson did some things in this direction a while ago

view this post on Zulip Oliver Nash (Dec 19 2020 at 11:37):

Thanks, maybe I'll see if I can turn some of this into a PR and ping him on that.

view this post on Zulip Oliver Nash (Dec 19 2020 at 13:57):

PR 1 of 2 https://github.com/leanprover-community/mathlib/pull/5434

view this post on Zulip Johan Commelin (Dec 19 2020 at 14:23):

@Aaron Anderson @Mario Carneiro could you mind taking a look at :up: ?

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:38):

I now have (disgusting) proofs of the above modulo the following two results:

variables {α}

lemma Sup_sup_Sup_eq_Sup_union
  {s t : set α} (hs : s.finite) (ht : t.finite) : Sup s  Sup t = Sup (s  t) := sorry

lemma finite_Sup_mem {s : set α} (h : s.finite) : Sup s  s := sorry

I don't suppose we have these somewhere?

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 17:42):

What are the assumptions on the order?

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:42):

In this case, complete_lattice.

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 17:42):

Isn't subsets of a set a complete lattice?

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:42):

My code snippets are supposed to flow into each other but it's possible I've screwed up.

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:43):

Hmm, am I being dense?

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 17:43):

I think finite_Sup_mem is false for subsets of a set

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 17:43):

Union of two sets might not be either one

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:44):

Oh sorry, I am being dense.

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:44):

Thanks, no wonder this was such a useful lemma!

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:44):

Right, I'm done for the day but I'll pick this up tomorrow. Apologies for the nonsense.

view this post on Zulip Kevin Buzzard (Dec 19 2020 at 17:44):

True for total orders

view this post on Zulip Adam Topaz (Dec 19 2020 at 17:53):

I think is_sup_compact needs some additional assumptions too, e.g. it's false for the set of finite subsets of a type. Edit: ignore this --- just saw it was a def :rofl:

view this post on Zulip Aaron Anderson (Dec 19 2020 at 17:54):

Looking at the PR, it looks like there is quite a bit of work to do in uniting preorder_hom and rel_hom.

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:57):

I'm confident the only outright error is the one Kevin identified since I have sorry-free proofs of everything except is_sup_compact_iff (which I actually don't even need).

view this post on Zulip Oliver Nash (Dec 19 2020 at 17:58):

Aaron Anderson said:

Looking at the PR, it looks like there is quite a bit of work to do in uniting preorder_hom and rel_hom.

Yes, there seem to be basically no bridges between these two except the tiny scraps I have introduced.

view this post on Zulip Aaron Anderson (Dec 19 2020 at 17:59):

There's also work that you should look at in order_iso_nat

view this post on Zulip Oliver Nash (Dec 19 2020 at 18:00):

You mean the file order_iso_nat.lean?

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:00):

Yes

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:00):

which proves well-founded iff no strictly-ascending-chains

view this post on Zulip Oliver Nash (Dec 19 2020 at 18:01):

Yes, I actually used that.

view this post on Zulip Oliver Nash (Dec 19 2020 at 18:01):

https://github.com/leanprover-community/mathlib/pull/5434/files#diff-99300ada126e52bba4dacab69467bb0ec9c644b4334bd73fcb07d32e5d8d9535R66

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:01):

I see

view this post on Zulip Oliver Nash (Dec 19 2020 at 18:02):

Darn, gotta run. Visitors arrived. Apologies.

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:04):

We should fill out the connections between preorder_hom and rel_hom, or else refactor preorder_hom to use rel_hom and porting the preorder_hom API to that new definition, but I'm ok with getting a PR or two on ACC and DCC first.

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:09):

I would probably guess that ACC and DCC should be instances you can place on a partial_order rather than just props

view this post on Zulip Aaron Anderson (Dec 19 2020 at 18:10):

and you can define DCC either through using a different kind of rel_homin the definition, or just ACC of the order dual.

view this post on Zulip Oliver Nash (Dec 20 2020 at 17:11):

I now have a second PR here with some of the other results I'd like to use: https://github.com/leanprover-community/mathlib/pull/5446

The proofs are a total mess and so should be ignored (though this time they have the advantage of not requiring any false lemmas). However I would be grateful for feedback on whether it looks like I'm taking things in a useful direction in terms of what I'm defining and proving.

Unfortunately as usual I'm in a hurry and must now run off but I will have some time tomorrow and will pay careful attention to any remarks others may have to offer.

view this post on Zulip Oliver Nash (Apr 06 2021 at 20:06):

Since I now want to use the result, I've decided to revive this previously-abandoned PR: https://github.com/leanprover-community/mathlib/pull/5434

view this post on Zulip Johan Commelin (Apr 06 2021 at 20:07):

Good luck! :happy:

view this post on Zulip Oliver Nash (Apr 06 2021 at 20:07):

Thanks :D

view this post on Zulip Oliver Nash (Apr 06 2021 at 20:07):

I'm afraid I rebased rather than merged master to resolve a merge conflict so I've blown away the branch history but what I understood to be the most contentious issue was the new typeclass which I have removed.


Last updated: May 17 2021 at 15:13 UTC