Zulip Chat Archive

Stream: general

Topic: multiset min on with_top


view this post on Zulip Kevin Buzzard (Jul 12 2018 at 21:06):

Back in the days before with_top I rolled my own instance of decidable_linear_order (option nat) (with none = +infinity), and defined min on multiset (option nat) as lam s, multiset.fold (min) none s. It compiled and worked fine and I thought no more about it.

In a fit of tidying up today, I decided that rather than leaving those 60 lines of code in my repo I could just switch to with_top; however to my mild surprise (because I didn't remember doing anything clever)

import data.multiset

definition multiset.min (s : multiset (with_top )) : with_top  := multiset.fold min none s

fails -- for fold to work like this on a multiset we need a proof that min is commutative and associative on with_top nat, and type class inference fails to find these things. So I went back to my original work and found that in my home-grown linear order associativity seemed to come from lattice.inf_is_associative, because for me @lattice.has_inf.inf (option nat) _ = min was rfl but for with_top nat it's apparently not. I would just create an instance of is_commutative (with_top nat) min and of is_associative (with_top nat) min (or more generally a proof that if min is commutative on X then it's commutative on with_top X etc) but because I've seen with my own eyes this devious trick which I inadvertently pulled off using lattice infs I wonder whether there is a better approach; I decided that asking here was a better idea than creating noisy irrelevant PRs.

view this post on Zulip Mario Carneiro (Jul 18 2018 at 09:41):

I think this just needs to be copied from finset.min

view this post on Zulip Chris Hughes (Jul 18 2018 at 22:06):

On a related note, is there a case for making min and max return values in with_top and with_bot instead of option? I needed the theorem s ⊆ t -> max s ≤ max t for polynomials, but there's no order on option.

view this post on Zulip Patrick Massot (Jul 18 2018 at 22:36):

Kenny's work on valuations includes putting an order on option a from an order on a. But I'd prefer to see semantic names used instead of option

view this post on Zulip Kenny Lau (Jul 18 2018 at 22:36):

I think that's just what we now call with_bot

view this post on Zulip Mario Carneiro (Jul 19 2018 at 04:10):

You can use sup and inf instead of min and max for a more order-based definition


Last updated: May 14 2021 at 03:27 UTC