## Stream: new members

### Topic: minimum and maximum of 4 rats

#### Anas Himmi (May 30 2020 at 16:34):

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 (May 30 2020 at 16:43):

You can use finset.min or finset.inf

#### Mario Carneiro (May 30 2020 at 16:45):

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 (May 30 2020 at 16:49):

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 (May 30 2020 at 16:50):

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 (May 30 2020 at 16:51):

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

I didn't

#### Johan Commelin (May 30 2020 at 16:55):

Neither did I :wink:

#### Johan Commelin (May 30 2020 at 16:55):

But I think Isabelle has a good implementation

#### Johan Commelin (May 30 2020 at 16:55):

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

#### Anas Himmi (May 30 2020 at 17:04):

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

#### Yury G. Kudryashov (May 30 2020 at 17:06):

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 (May 30 2020 at 17:08):

okay, thank you !

#### Jalex Stark (May 30 2020 at 22:53):

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

Last updated: May 16 2021 at 05:21 UTC