Zulip Chat Archive

Stream: general

Topic: finset


Floris van Doorn (Nov 20 2018 at 22:12):

Is the following result somewhere in mathlib? If not, are there results which make it less painful than proving it from scratch using lists?

def exists_of_subset_image {α : Type u} {β : Type v} {f : α → β} {s : finset β} {t : set α}
  (h : ↑s ⊆ f '' t) : ∃s' : finset α, ↑s' ⊆ t ∧ s'.image f = s

Kenny Lau (Nov 20 2018 at 22:51):

import data.finset

universes u v

theorem exists_of_subset_image {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β]
  {f : α  β} {s : finset β} {t : set α} (h : s  f '' t) :
  s' : finset α, s'  t  s'.image f = s :=
begin
  induction s using finset.induction with a s has ih h,
  { exact , set.empty_subset _, finset.image_empty _⟩ },
  rw [finset.coe_insert, set.insert_subset] at h,
  rcases ih h.2 with s', hst, hsi,
  rcases h.1 with x, hxt, rfl,
  refine insert x s', _, _⟩,
  { rw [finset.coe_insert, set.insert_subset], exact hxt, hst },
  rw [finset.image_insert, hsi]
end

Kenny Lau (Nov 20 2018 at 22:51):

a simple induction

Floris van Doorn (Nov 20 2018 at 22:56):

Thanks! finset.induction makes this indeed quite easy to prove.

Kenny Lau (Nov 20 2018 at 22:57):

can we call this finite_choice... >?<

Floris van Doorn (Nov 21 2018 at 00:02):

Different question: should finset.singleton be protected? There are two singletons if you open finset.

import data.finset
open finset
#print singleton

Kenny Lau (Nov 21 2018 at 01:26):

so... don't open finset? /s

Mario Carneiro (Nov 21 2018 at 01:50):

or use finset.singleton anyway

Mario Carneiro (Nov 21 2018 at 01:50):

maybe it should be renamed to single or something, it's already far longer than it should be, namely {x}

Mario Carneiro (Nov 21 2018 at 01:51):

in finset it has a prefix notation ι, you could use that

Scott Morrison (Nov 22 2018 at 22:47):

Hi, possibly a range of finset questions coming up... :-)

Scott Morrison (Nov 22 2018 at 22:47):

Why is theorem insert.comm (a b : α) (s : finset α) : insert a (insert b s) = insert b (insert a s) := ... marked as @[simp]?

Scott Morrison (Nov 22 2018 at 22:48):

This seems like a terrible idea, and is responsible for bad simplifications like:
range (n + 1 + 1) simplifying to insert n (insert (n + 1) (range n)).

Reid Barton (Nov 22 2018 at 22:49):

how does that not loop?

Scott Morrison (Nov 22 2018 at 22:49):

That too. :-)

Scott Morrison (Nov 22 2018 at 22:55):

Does mathlib have something to the effect of finset.iota n m, giving the finset of natural numbers n, n+1, ..., m-1?

Scott Morrison (Nov 22 2018 at 23:01):

Oops, iota is the wrong name. I guess finset.interval n m?

Scott Morrison (Nov 22 2018 at 23:04):

Hmm.. data.list.basic has a peculiarly named range' s n, giving the list [s, s+1, ..., s+n-1].

Scott Morrison (Nov 22 2018 at 23:08):

Okay, removing @[simp] on finset.insert.comm doesn't break anything, so if there are no complaints I'll PR it later.

Kevin Buzzard (Nov 22 2018 at 23:12):

IIRC Chris and Mario had a long discussion about the best way to do the bounds, when Chris was proving things about finite sums a while back

Scott Morrison (Nov 22 2018 at 23:12):

So what happened to Chris's work on finite sums?

Scott Morrison (Nov 22 2018 at 23:13):

Faced with talking to students again, I really want to make finset.sum more fun. :-)

Scott Morrison (Nov 23 2018 at 00:07):

I'm wondering how people would feel about removing the @[simp] from

theorem range_succ : range (succ n) = insert n (range n) := ...

I feel like this is often unhelpful. (In fact, in quadratic_reciprocity.lean Chris has to write - range_succ many times to avoid it firing. Similarly in order_of_element.lean.)

This would require either explicitly adding range_succ to the simp set in a few places, but not too many. (Three places across mathlib, and it saves many simp [-range_succ]s in quadratic_reciprocity.lean.)

Scott Morrison (Nov 23 2018 at 00:08):

But in particular as soon as you have a sum of range (n+1), this simp lemma may unhelpfully fire, which is confusing.

Kenny Lau (Nov 23 2018 at 00:08):

Is Scott Morrison talking about simp? :P

Scott Morrison (Nov 23 2018 at 00:08):

I love simp. I want to use it as much as possible.

Scott Morrison (Nov 23 2018 at 00:08):

Hence I want to remove bad @[simp] lemmas that get the maths wrong.

Kenny Lau (Nov 23 2018 at 00:09):

I see

Chris Hughes (Nov 23 2018 at 00:15):

I don't recall that conversation. I think it was Mario and Patrick. There's definitely a need to make finest.sum nicer, particularly with natural numbers. Also a need for a nice non commutative sum interface.

Scott Morrison (Nov 23 2018 at 00:39):

@Chris Hughes , if we were going to introduce an interval n m : finset nat, and try to make doing sums over natural numbers work nicely with it, would you prefer interval n m includes m, or not?

Scott Morrison (Nov 23 2018 at 01:00):

Does anyone know if

lemma finset_sum_split [add_comm_monoid β] (s : finset α) (f : α → β) (P : α → Prop) [decidable_pred P] :
s.sum f = (s.filter P).sum f + (s.filter (λ a, ¬ P a)).sum f := sorry

exists in mathlib?

Kenny Lau (Nov 23 2018 at 01:00):

yes

Kenny Lau (Nov 23 2018 at 01:01):

import data.finsupp

#check @finsupp.filter_pos_add_filter_neg

/-
finsupp.filter_pos_add_filter_neg :
  ∀ {α : Type u_1} {β : Type u_2} [_inst_1 : decidable_eq α] [_inst_2 : decidable_eq β] [_inst_3 : add_monoid β]
  (f : α →₀ β) (p : α → Prop) [_inst_4 : decidable_pred p] [_inst_5 : decidable_pred (λ (a : α), ¬p a)],
    finsupp.filter p f + finsupp.filter (λ (a : α), ¬p a) f = f
-/

Kenny Lau (Nov 23 2018 at 01:01):

oh wait

Kenny Lau (Nov 23 2018 at 01:01):

they are not exactly the same

Scott Morrison (Nov 23 2018 at 01:02):

I see. They're clearly related, but it's not obvious you could even prove mine from this, because of the decidable_eq hypotheses.

Scott Morrison (Nov 23 2018 at 01:05):

While on the subject, the [_inst_5 : decidable_pred (λ (a : α), ¬p a)] argument of finsupp.filter_pos_add_filter_neg is unnecessary.

Kenny Lau (Nov 23 2018 at 01:09):

import data.finsupp

lemma finset_sum_split {α β : Type*} [add_comm_monoid β] (s : finset α) (f : α  β) (P : α  Prop) [decidable_pred P] :
s.sum f = (s.filter P).sum f + (s.filter (λ a, ¬ P a)).sum f :=
by haveI := classical.dec_eq α; rw [ finset.sum_union (finset.filter_inter_filter_neg_eq s), finset.filter_union_filter_neg_eq]

Scott Morrison (Nov 23 2018 at 01:10):

awesome, thank you!

Reid Barton (Nov 23 2018 at 01:10):

in principle, it could be relevant at the use site... because decidability arguments are relevant

Scott Morrison (Nov 23 2018 at 01:11):

oh, I see, you might want to give separate arguments that P and not P are decidable??

Reid Barton (Nov 23 2018 at 01:11):

in principle...

Reid Barton (Nov 23 2018 at 01:12):

though it's not very likely especially when the arguments are provided by type class inference and not looking at the expected type

Reid Barton (Nov 23 2018 at 01:17):

actually it might not be that unlikely, if both instances come from prop_decidable

Sebastien Gouezel (Nov 23 2018 at 07:13):

@Chris Hughes , if we were going to introduce an interval n m : finset nat, and try to make doing sums over natural numbers work nicely with it, would you prefer interval n m includes m, or not?

The notation for real intervals is Icc a b for intervals which are closed on both ends, and Ico for closed-open ones, and so on. All this is in /data/set/intervals. Ideally, you would use the same syntax prefixed with finset., or something like that. And by the way, the only good convention to do sums is closed on the left and open on the right, i.e., $S_n f = \sum_{i=0}^{n-1} f(i)$.

Sebastien Gouezel (Nov 23 2018 at 07:20):

Fancy Isabelle notation for these (I don't think this has been ported to Lean, or if there could be a parsing problem): {a..b} for the closed interval with endpoints a and b. And {a<..b} for the open/closed version. And {..<b} for the semiinfinite open one. And so on.

Scott Morrison (Nov 23 2018 at 07:43):

I wonder if we could do the actual maths notations for these... [a,b), etc.

Patrick Massot (Nov 23 2018 at 07:49):

Or the actual maths notations for these... [a, b[, etc.

Mario Carneiro (Nov 23 2018 at 07:49):

nonono

Mario Carneiro (Nov 23 2018 at 07:49):

that will kill your editor

Mario Carneiro (Nov 23 2018 at 07:50):

trust me it's not worth it

Patrick Massot (Nov 23 2018 at 07:50):

see also https://github.com/PatrickMassot/bigop/blob/master/src/tests.lean

Patrick Massot (Nov 23 2018 at 07:50):

Although Cyril convinced me that Sébastien is right and I should exclude the upper bound from the sum

Mario Carneiro (Nov 23 2018 at 07:51):

I'm okay with {a..<b} and friends. In metamath we used (a ..^ b) which is slightly less mnemonic

Mario Carneiro (Nov 23 2018 at 07:52):

there could be a parsing problem with {a}, but it might work as long as ... doesn't mean anything else... oh

Johan Commelin (Nov 23 2018 at 07:52):

There is also unicode

Scott Morrison (Nov 23 2018 at 07:55):

In any case, it sounds like everyone is on board with the "default" being to not include the upper point.

Kevin Buzzard (Nov 23 2018 at 07:56):

One million python users can't be wrong

Patrick Massot (Nov 23 2018 at 07:56):

What convinced be is that is avoids some nat substractions. That is a killing argument

Scott Morrison (Nov 23 2018 at 07:56):

I will try to fill in interval n m as a list/multiset/finset, and provide a good API for splitting these, into disjoint intervals or endpoint + other interval, for reindexing, etc.

Johan Commelin (Nov 23 2018 at 07:59):

@Scott Morrison How does this tie in to "I'll stop working on maths in Lean for a while, to work a bit on infrastructure..." (just curious)

Scott Morrison (Nov 23 2018 at 23:03):

:-)

Scott Morrison (Nov 28 2018 at 04:51):

Is there any reason why we don't have sUnion on finset? This seems like an obvious omission.

Kenny Lau (Nov 28 2018 at 04:52):

finset.bind _ id?

Scott Morrison (Nov 28 2018 at 04:53):

Great, thank you!

Scott Morrison (Nov 28 2018 at 05:14):

Is there no preimage for finset?

Kenny Lau (Nov 28 2018 at 05:16):

you could use finset.filter


Last updated: Dec 20 2023 at 11:08 UTC