minimum and maximum of 4 rats

Stream: new members

[Anas Himmi]

what's the best (constructive) way to get the minimum and maximum of four rationals say a,b,c and d from a proving standpoint?
should i use min (min a b) (min c d)?

[Mario Carneiro]

You can use finset.min or finset.inf

[Mario Carneiro]

but it's hard to say from just this what the best way to do what you want is. What are you trying to do?

[Anas Himmi]

I am implementing multiplication of interval arithmetic. i think i can't use finsets because in general, they could be equal, but i don't know much about finsets yet.

[Anas Himmi]

i tried going with `min (min a b) (min c d), bu then i end up with A LOT of cases to handle.

[Johan Commelin]

Have you looked at what other systems do for interval arithmetic?

[Anas Himmi]

I didn't

[Johan Commelin]

Neither did I :wink:

[Johan Commelin]

But I think Isabelle has a good implementation

[Johan Commelin]

They can do lots of stuff in analysis that we can't.

[Anas Himmi]

it seems they did the same thing as my first guess :/

[Yury G. Kudryashov]

You can add def min4 a b c d := min (min a b) (min c d) and prove (mostly by simp) lemmas like le_min4_iff

[Anas Himmi]

okay, thank you !

[Jalex Stark]

a finset is a multiset with a nodup proof, right? you could try working with multisets directly if you don't like the "hardcoded" version