Ascending chain conditions

Stream: Is there code for X?

[Oliver Nash]

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

[Oliver Nash]

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

[Johan Commelin]

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

[Oliver Nash]

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

[Oliver Nash]

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

[Johan Commelin]

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

[Oliver Nash]

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?

[Kevin Buzzard]

What are the assumptions on the order?

[Oliver Nash]

In this case, complete_lattice.

[Kevin Buzzard]

Isn't subsets of a set a complete lattice?

[Oliver Nash]

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

[Oliver Nash]

Hmm, am I being dense?

[Kevin Buzzard]

I think finite_Sup_mem is false for subsets of a set

[Kevin Buzzard]

Union of two sets might not be either one

[Oliver Nash]

Oh sorry, I am being dense.

[Oliver Nash]

Thanks, no wonder this was such a useful lemma!

[Oliver Nash]

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

[Kevin Buzzard]

True for total orders

[Adam Topaz]

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:

[Aaron Anderson]

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

[Oliver Nash]

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).

[Oliver Nash]

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.

[Aaron Anderson]

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

[Oliver Nash]

You mean the file order_iso_nat.lean?

[Aaron Anderson]

Yes

[Aaron Anderson]

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

[Oliver Nash]

Yes, I actually used that.

[Oliver Nash]

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

[Aaron Anderson]

I see

[Oliver Nash]

Darn, gotta run. Visitors arrived. Apologies.

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Oliver Nash]

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.

[Oliver Nash]

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

[Johan Commelin]

Good luck! :happy:

[Oliver Nash]

Thanks :D

[Oliver Nash]

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.