fold

Stream: general

[Johan Commelin]

@Simon Hudon I think you had a very general framework for doing folds. Is there an easy way to prove

lemma finset.fold_sup_bot_singleton {X : Type*} (s : finset X) :
  finset.fold has_sup.sup \bot singleton s = s :=
sorry

I feel like this should follow from some abstract nonsense. singleton = pure etc...

[Mario Carneiro]

I would suggest relating it to finset.bind, and then abstract nonsense will let you use the monad laws

[Mario Carneiro]

i.e. finset.fold has_sup.sup \bot f s = finset.bind s f

[Johan Commelin]

Aah, I should be using bind from the get go (-;

[Simon Hudon]

did bind do the trick? The foldable framework won't work without extending it because it doesn't use commutative monoids to do the aggregation. I considered doing that extension but I wasn't sure it would be useful because the only instances that I could think of are finset and multiset. Now that I think of it, unordered trees could probably use it as well.

[Johan Commelin]

Yes, bind works great.

[Johan Commelin]

However, there doesn't seem to be a lemma relating the two

[Johan Commelin]

Mario Carneiro said:

i.e. finset.fold has_sup.sup \bot f s = finset.bind s f

:up: is missing from the library, I think. Also for multiset.

[Bryan Gin-ge Chen]

It'd be nice if the finset module doc had a few examples of using finset.bind since it seems to be a common but nonobvious technique.

[Mario Carneiro]

Would it help to rename it to bUnion?

[Mario Carneiro]

We don't use "monadic" naming for anything else in finset so it's a bit hard to find

[Reid Barton]

relatedly, I was wondering why there is no algebra.big_operators for sup and inf (as far as I know)

[Reid Barton]

A semilattice_sup_bot is equivalent to a special kind of commutative monoid (namely an idempotent one) so one could imagine obtaining much of the API automatically

[Mario Carneiro]

we don't have that type alias yet

[Mario Carneiro]

is that tropical?

[Reid Barton]

I think tropical usually suggests you're also turning * into +

[Reid Barton]

whereas in order theory it's probably more commonly useful to turn it into inf (in a distributive lattice)

[Mario Carneiro]

I was thinking more about the second part, turning + into max

[Reid Barton]

Right, but I think tropical usually suggests the two as a package. But I'm not really an expert on that.
Maybe to_lattice? to_boolean? to_sup, to_inf?

[Reid Barton]

I suspect naming won't turn out to be the hardest problem to solve here

[Mario Carneiro]

Sure, but as long as the two are compatible we could equip a single type alias with both the add_group structure and the ring structure, depending on what underlying instances are available

[Mario Carneiro]

Although, I think the map actually goes in the other direction, so it would be e.g. add_comm_group (of_inf L) where L is some kind of lattice

[Mario Carneiro]

you could precompose with order_dual to get the other one