368 add alldisjoint alldistinct 2

[wdcraft01]

A second initial attempt to augment the logic/sets/disjointness package with the new AllDisjoint() and AllDistinct() classes, which are intended to take a single argument consisting of a collection of sets or items (in contrast to the variadic classes Disjoint() and Distinct()). This will make some expression formulations simpler. This branch also makes an initial effort to establish some definitional axioms and new disjoint_singleton and distinct_singleton theorems. The AllDisjoint() and AllDistinct() classes are purely abstract right now with no methods for evaluation, unfolding, conclusion, etc. It is worth @wwitzel looking at the axioms/theorems with a skeptical eye.

[wwitzel]

There are a couple issues with your 'all_distinct_def' theorem. IndexedVar is intended for use within an ExprRange. I don't think you'll be able to sensibly instantiate 'all_distinct_def' in it's current form. Instead, you should treat 'x' as a function. Also, I believe you mean to use 'Disjoint' instead of 'NotEquals', right? You can do something like:

Forall(n, Forall(x,Equals(AllDistinct(Set(ExprRange(Function(x, k), one, n),
Forall((i, j), Disjoint(Function(x, i), Function(x, j)),
conditions=[NotEquals(i, j)], domain=Interval(one, n)))),
domain=Natural))

But a more straightforward definition would be:
Forall(S, Equals(AllDistinct(S),
Forall((A, B), Disjoint(A, B),
domain=S, condition=NotEquals(A, B))))

Do I have that right?

[wdcraft01]

Thanks @wwitzel. In response to your observations:

There are a couple issues with your 'all_distinct_def' theorem. IndexedVar is intended for use within an ExprRange. I don't think you'll be able to sensibly instantiate 'all_distinct_def' in it's current form. Instead, you should treat 'x' as a function. Also, I believe you mean to use 'Disjoint' instead of 'NotEquals', right? You can do something like:

Forall(n, Forall(x,Equals(AllDistinct(Set(ExprRange(Function(x, k), one, n), Forall((i, j), Disjoint(Function(x, i), Function(x, j)), conditions=[NotEquals(i, j)], domain=Interval(one, n)))), domain=Natural))

I am looking at this now and will switch the indexed var approach over to a functional approach. In answer to the question about 'Disjoint' instead of 'NotEquals', though, I think 'NotEquals' is what we need here — the 'all_distinct_def' is about distinctiveness, not disjointness. The items x(1), x(2), … x(n) are elements in a set and we are specifying that x(i) is distinct from x(j) (i.e. they are not equal) whenever i ≠ j. We could rewrite it to use the singleton set approach you've used in the distinct_def, in which case disjoint would then be appropriate and we could avoid the quantification over $i$ and $j$. I don't know which is better. Disjointness of the singleton sets feels elegant and clever; the NotEquals approach feels more direct.

The "more straightforward" definition you propose I think is off-track, perhaps confusing distinctiveness with disjointness. Translating your suggested text, I get:

$$\forall_{S}\big( \textrm{AllDistinct}(S) = \big[ \forall_{A,B \in S | A \ne B} (\textrm{disjoint}(A, B)) \big] \big)$$

I actually toyed with something similar when constructing the definition, but realized we can't "pick out" $A,B \in S | A \ne B$ since the $A \ne B$ is the definition of being distinct. And we can't use the following:

$$\forall_{S}\big( \textrm{AllDistinct}(S) = \big[ \forall_{A,B \in S} (A \ne B) \big] \big)$$

because $A,B\in S$ isn't sufficient to constrain $A$ and $B$ from being the same element. So I think we have to use some sort of ordered list (or functional list) expression to clarify that the two elements being compared are from different locations in the list.

Looking at this afresh now, I see we could also simply "punt" and use the approach I used for the AllDisjoint, defining AllDistinct simply in terms of Distinct by simpy removing the Set wrapper, something like this:

$$\forall_{n \in \mathbb{N}}\big[ \forall_{A_{1}, A_{2}, \ldots, A_{n}}\big( \textrm{AllDistinct}(\{A_{1}, A_{2}, \ldots, A_{n}\}) = \textrm{distinct}(A_{1}, A_{2}, \ldots, A_{n}) \big) \big] $$

[wwitzel]

But the elements of a set are always distinct. Remember?
{a, a, b, c} = {a, b, c}
They aren't multi-sets. I'm not seeing the purpose of AllDistinct.