is there possible to compare arbitrary set in total order?

Like the first step, I want to calculate `{1::nat} <= {2}`

holds on, because it's obviously held for numbers.

Concrete syntax for what?

trying to prove the comparison between two predicates.

Sorry, wrong thread.

I see, thank you

I am not aware of any total ordering on sets

Thanks, then I think I need to search another way

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.

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"

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.

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

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

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.

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.

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

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: Dec 07 2023 at 20:16 UTC