prove {1::nat} <= {2} · Beginner Questions

Well, there might be a way to define a total order on sets for element types that are totally ordered. You probably want the element type to be totally ordered anyhow when thinking about a total order on sets, but the total order on the element type allows you to turn sets into lists if the sets are finite. You can then use the lexicographic order to compare the resulting lists, which in effect gives you a total order on finite sets. It might be possible to extend this to infinite sets.

Mathias Fleury (Aug 01 2023 at 19:58):

Just to mention something I tried on the theories you sent me: changing the definition of the ordering to have "le_rexp (Sym _) (Sym _) = True"

Wolfgang Jeltsch (Aug 01 2023 at 19:58):

Let’s think how to extend this to infinite sets. If you just compare lists lexicographically, you start with their respective first elements and compare them. With sets you don’t necessarily have a good notion of first element. However, it’s immediately clear that one list is smaller than the other if its first element is smaller than the first element of the other. You could equivalently say that one list is smaller than the other if it contains an element that is smaller than any element of the other list. This is something you can generalize to sets.

Mathias Fleury (Aug 01 2023 at 19:58):

but there were more changes to do (you also have some "if r=r' then _ else _ " in the definition which is not executable

Wolfgang Jeltsch (Aug 01 2023 at 20:02):

Going on with my idea, we can see that the only case left is when neither set has elements that are smaller than all elements of the other set. But then we can just look for a maximal part “at the bottom” of both sets and cut it off. What’s left are two sets where either one set has an element smaller than all the elements in the other set with some elements actually being there, or one two sets where at least one is empty. It’s then sort of clear which one should be considered the smaller one.

I’m not sure whether I’ve overlooked something. It might be fun to try defining this order in Isabelle and prove that it’s total.

Wolfgang Jeltsch (Aug 01 2023 at 21:10):

Wolfgang Jeltsch said:

I’m not sure whether I’ve overlooked something. It might be fun to try defining this order in Isabelle and prove that it’s total.

I tried to come up with such a definition and proof and finally had to conclude that I’ve overlooked something. :sweat_smile: Consider the set of even integers and the set of odd integers. These don’t have a common part at the bottom, so there’s nothing to cut off. Still, it’s not the case that one of these sets has an element smaller than all elements of the other set.

Wolfgang Jeltsch (Aug 01 2023 at 21:11):

So totally ordering infinite sets seems problematic. Finite sets are a different matter, though: you should be able to apply the approach sketched above, where you first convert the sets to lists and then order the resulting lists lexicographically.

Wolfgang Jeltsch (Aug 01 2023 at 21:13):

Another thing is coming up with a partial order. Here you can just define that one set is smaller than the other exactly if all elements in the former are smaller than all elements in the latter. This should give you a partial order even if the elements are only partially ordered.

Hongjian Jiang (Aug 01 2023 at 21:46):

I could have a try on finite set in this way, thanks

Hongjian Jiang (Aug 01 2023 at 21:50):

in this way, lemma le_rexp_antisym"⟦le_rexp r s; le_rexp s r⟧ ⟹ r = s" will fail.

with the conterexample of r = Sym {} and s = Sym UNIV

Last updated: Apr 28 2024 at 01:11 UTC