News for hackers. Stuff that matters.
Re:What would Dijkstra do? Proving the associativity of min by im3w1l on Thursday March 12, 2020 @01:46AM (#22554123)
Here's the solution I thought of, which is pretty similar.

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.

Re:What would Dijkstra do? Proving the associativity of min by virtuous_signal on Thursday March 12, 2020 @02:38AM (#22554365)
Similar? In my opinion this is much faster, easier, and less burdened by notation.
Re:What would Dijkstra do? Proving the associativity of min by atq2119 on Thursday March 12, 2020 @03:59AM (#22554693)
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.
Re:What would Dijkstra do? Proving the associativity of min by thaumasiotes on Friday March 13, 2020 @07:01PM (#22571612)
> 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.

Re:What would Dijkstra do? Proving the associativity of min by Josh04 on Thursday March 12, 2020 @08:08AM (#22555913)
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.
Re:What would Dijkstra do? Proving the associativity of min by im3w1l on Thursday March 12, 2020 @02:30PM (#22560062)
I agree. It's more of a sketch than a proof which is why it's so short.
Re:What would Dijkstra do? Proving the associativity of min by raverbashing on Thursday March 12, 2020 @07:34AM (#22555705)
Hence mathematicians will "hate it" and replace it with something more complicated and less clear

This proof works for any totally ordered set (hence a <= operation is defined on it)