8 ms·

> 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, actual

> 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 [1] Or prelude, or whatever it's called. https://github.com/idris-lang/Idris-dev/blob/master/libs/prelude/Prelude/Nat.idr#L772 https://github.com/idris-lang/Idris-dev/blob/master/libs/pre...

reikonomusha 7y ago
This is also using induction on naturals, which doesn’t “port” to the reals, as the post asks.
lmm 7y ago
That's doing induction its arguments, which relies on them being naturals - it's not an approach that would generalise to reals.
- JadeNB 7y ago
  I think that's necessary, since the order on the full set of reals isn't constructively decideable, so min isn't even a total function there.
  - lmm 7y ago
    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.
    - leni536 7y ago
      Unless when they happen to be equal. Then it never halts.
      - Skeime 7y ago
        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.
    - JadeNB 7y ago
      Yes, I'm wrong. I was thinking of the naïve implementation if ( a < b ) then { return b } else { return a } which requires being able to decide order, but, as child comments point out, that's not necessary.

reikonomusha 7y ago

This is also using induction on naturals, which doesn’t “port” to the reals, as the post asks.

lmm 7y ago

That's doing induction its arguments, which relies on them being naturals - it's not an approach that would generalise to reals.

JadeNB 7y ago
I think that's necessary, since the order on the full set of reals isn't constructively decideable, so min isn't even a total function there.
- lmm 7y ago
  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.
  - leni536 7y ago
    Unless when they happen to be equal. Then it never halts.
    - Skeime 7y ago
      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.
  - JadeNB 7y ago
    Yes, I'm wrong. I was thinking of the naïve implementation if ( a < b ) then { return b } else { return a } which requires being able to decide order, but, as child comments point out, that's not necessary.