It's certainly a nice solution, but OP's solution has the nice property of working directly on a universality definition, which makes the argument more general. For example, the universality argument also works for the infimum and gcd operations.
> For example, the universality argument also works for the infimum and gcd operations.
I've been thinking about this and I don't see how the argument can possibly work for the infimum operation. The problem is that infimum is necessarily a unary operation -- it doesn't make any sense to consider it to have multiple arguments.
Consider the open interval (1,2). The infimum is 1. But 1 is not contained in the interval. And because 1 is not contained within the interval, _if_ infimum were a binary operation, we could not apply it to the interval and get 1. Binary infimum is the same operation as binary min, and while the infimum of (1,2) is 1, the minimum value of (1,2) does not exist.
We can actually use this to do a much more direct proof of the associativity of binary min: binary min is the same thing as unary min (min as applied to a single set of arguments rather than two scalar arguments), and unary min cannot fail to be associative because it has only one argument. Repeated binary mins do nothing more than apply unary min to the set of individual arguments.
With no offense intended to the poster, the inferences are a little sloppy by mathematical standards and most of the hard work is done by introducing ("noticing") the set notation to the definition of min.
The Dedekind cut formulation of the real numbers is that a real number is defined to be a nonempty "downwards closed" subset of rational numbers. Then the min operation corresponds to taking intersections, and taking intersections is associative.
It's cool they figured something like this out from first principles.
> The Dedekind cut formulation of the real numbers is that a real number is defined to be a nonempty "downwards closed" subset of rational numbers. Then the min operation corresponds to taking intersections
They didn't figure that out exactly. They figured out something much less significant: that a real number is defined by a nonempty upwards closed subset of real numbers:
>> My second epiphany was that equality of real numbers can also be characterized by having the same “downsets”, i.e. two real numbers are equal if and only if the sets of real numbers less than or equal to them are the same.
In other words, we choose to represent the real number r as the closed interval (-∞, r].
The point of Dedekind cuts is that you can define real numbers without using real numbers in the definition.
They do then set up min as set intersection as suggested by the interval definition.
Writing out the choice of real number representation makes it clear that we could also represent a real number as the interval [r, ∞), in which case minimum would be set union rather than set intersection. It doesn't really matter whether we use a closed or open interval.
The somewhat-standard definition of the naturals (0 = {}, 1 = {0}, 2 = {0, 1}, 3 = {0, 1, 2}, ...) also maps min to set intersection. GCD, which someone else mentions in another comment, is very straightforwardly a set intersection problem.
The intuition here is that an operation throws away information that isn't relevant while keeping the relevant information. If you can't lose relevant information, you can't fail to be associative. Probably all such operations can be straightforwardly mapped to set intersection or set union. (Under the definition of the naturals given above, note that set union gives you the max operator.)
Similarly you can show that gcd and lcm are associative, once you know their universal properties (for gcd, being the one common divisor that every common divisor divides; for lcm, the corresponding dual property). Similarly the associativity (up to unique diagram-fitting isomorphism) of products (or even fibered products) in any category (when they exist).
The really high horse here is called "Yoneda embedding", but there is not much gained from going that high.
You don't really need to bring the Yoneda embedding into it. They're all just partial orders (for the gcd and lcm use the order defined by divisability), which can easily be shown to be categories with at most a single function between objects. After that it's just expanding definitions.
I think a shorter way to write that is to first note the downset representation of reals. Then your definition of min is just the set intersection and there's nothing more to show.
To be fair, reals have nothing to do with this - the 'min' makes sense - and is associative - in any ordered set (even partially ordered, if you accept that it may be undefined for some pairs).
So you define max([-∞, a]) =a, and define min(a, b) as max([-∞, a] ∩ [-∞, b])? Isn't this just shifting the problem elsewhere? For instance now you need to prove that the intersection of sets is of the form [-∞, a] or [-∞, b], which is fairly intuitive, but not more intuitive than the usual definition of min.
This is the definition that leads to the ugly proof by cases.
Right there is the problem. There's nothing wrong with proof by cases. People suck at it, but machines do it just fine. I ran into this years ago in the early days of program proving. The kind of proofs that mathematicians like are not the kind you really want to use to get work done by machine.
"Programmers are not to be measured by their ingenuity and their logic but by the completeness of their case analysis." ~ Perlis
I personally pride myself on my ability to analyze situations by cases, and to grind through normally-opaque walls to find proofs, but we should always keep in mind that it is the hardest way. It's like fishing for algorithms.
Presumably, ingenuity and logic can lead one to a simplified case analysis (more cases covered by fewer separate conditions), which allows one to do a complete case analysis with less effort.
> The book expected them to do a proof by cases, with some sort of case split on the order of a , b , and c . What they turned in was mostly pretty good, actually, but while grading it I became disgusted with the whole thing and thought there has to be a better way.
This is how it's done in the Idris standard library[1]:
total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z c r = Refl
minimumAssociative (S k) Z r = Refl
minimumAssociative (S k) (S j) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
Almost all reals are not computable, but as far as I know min is total - given two reals (represented as e.g. lazy infinite decimal sequences), computing their min is trivial.
Actually, computing the minimum should work: If they are equal you can still lazily produce the digits of the decimal expansion. What you can’t do in this case is to tell whether this minimum is equal to the first or the second number.
One way of looking at it is training, you practise punching a bag and later you go box, you prove trivial results 5 ways then when you have a problem that isn't trivial you have 5 approaches in your locker.
It is a course exercise. The additional insight is that there are multiple ways to solve this exercise, one that most students would chose and another, explored in the article.
Start with the case definition of min.
Notice that min(a,b) <= a, min(a,b) <= b and min(a,b) in {a,b}
Let d = min(a,min(b,c)) and e = min(min(a,b),c)
Then d <= a, d <= b, d <= c and d in {a,b,c}
Same goes for e.
Since e is in {a,b,c} and d <= a, d <= b, d <= c, it must follow that d <= e. And by symmetry e <= d. So d=e.