Zulip Chat Archive

Stream: new members

Topic: minimum and maximum of 4 rats


view this post on Zulip 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)?

view this post on Zulip Mario Carneiro (May 30 2020 at 16:43):

You can use finset.min or finset.inf

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 30 2020 at 16:51):

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

view this post on Zulip Anas Himmi (May 30 2020 at 16:51):

I didn't

view this post on Zulip Johan Commelin (May 30 2020 at 16:55):

Neither did I :wink:

view this post on Zulip Johan Commelin (May 30 2020 at 16:55):

But I think Isabelle has a good implementation

view this post on Zulip Johan Commelin (May 30 2020 at 16:55):

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

view this post on Zulip Anas Himmi (May 30 2020 at 17:04):

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

view this post on Zulip 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

view this post on Zulip Anas Himmi (May 30 2020 at 17:08):

okay, thank you !

view this post on Zulip 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