a multiset of headaches

Stream: general

[Johan Commelin]

I've never really used multisets before, but how do I prove something like this?

example {σ : Type*} (l : list σ) :
  multiset.map (λ (i : fin l.length), l.nth_le i i.2) finset.univ.val = (l : multiset σ) :=
begin
  sorry
end

[Kenny Lau]

what is the use case?

[Kenny Lau]

I think a statement involving list and multiset and finset at the same time wouldn't be too idiomatic

[Johan Commelin]

Can you show that there exists a monomial in 5 variables, of the form $X^3 Y^2 Z W^4 U^3$?

[Johan Commelin]

The 5 variables are indexed by an arbitrary fintype.

[Johan Commelin]

In particular, 5 is actually n : nat, or rather fintype.card \sigma.

[Johan Commelin]

But it's easy to reduce to the case fin n, which is what you see upstairs.

[Johan Commelin]

And l is a list of nats that are the degrees of the variables that I want, so l = [3,2,1,4,3].

[Johan Commelin]

(But there is no prescribed order on the variables, so any monomial will do, up to symmetry.)

[Scott Morrison]

1. rename multiset.ext to multiset.ext_iff
2. define multiset.ext following the usual rule
3. mark it with @[ext]
4. prove the lemma alluded to the the doc-string for map, but apparently not actually proved ...?
5. hope the goal looks better?

[Scott Morrison]

(Yuck?)

[Scott Morrison]

(Both your goal, and what I found looking in multiset.lean...)

[Johan Commelin]

Hmmm, I see...

[Chris Hughes]

@[simp] lemma list.nth_le_cons_cast_succ {α : Type*} (a : α) (l : list α) (i : fin l.length) :
  (a :: l : list α).nth_le i.cast_succ i.cast_succ.2 = l.nth_le i i.2 :=
sorry

@[simp] lemma list.nth_le_cons_length {α : Type*} (a : α) (l : list α) (h):
  (a :: l : list α).nth_le l.length h = a :=
sorry

example {σ : Type*} (l : list σ) :
  multiset.map (λ (i : fin l.length), l.nth_le i i.2) finset.univ.val = (l : multiset σ) :=
begin
  induction l with a l ih,
  { refl },
  { have h₁ : (finset.image fin.cast_succ (@finset.univ (fin l.length) _)).1 =
        (@finset.univ (fin l.length) _).1.map fin.cast_succ,
      from finset.image_val_of_inj_on (by simp),
    have h₂ : fin.last l.length ∉ finset.image fin.cast_succ finset.univ,
    { rw [finset.mem_image], simp [fin.cast_succ_ne_last] },
    rw [fin.univ_cast_succ, finset.insert_val, multiset.ndinsert_of_not_mem h₂,
      multiset.map_cons, h₁, multiset.map_map],
    simp [function.comp, list.nth_le_cons_cast_succ, ih] }
end

[Scott Morrison]

list.nth_le_cons_length seems wrong, but you also didn't use it?

[Chris Hughes]

It's @[simp] so the simp used it.

[Scott Morrison]

But it's wrong, isn't it? a is the zeroth element, no that l.lengthth?

[Chris Hughes]

Yes, the list is in the wrong order. D'oh

[Chris Hughes]

So it should probably be proved with list.reverse_rec_on

[Scott Morrison]

While something like this will work (and Chris reached it much faster than I was going to), I feel like "having to resort to induction" is a bad sign here, and it might be better to improve the API.

[Scott Morrison]

though there's some irreducible gross-ness in any proof of this caused by the gross-ness of (λ (i : fin l.length), l.nth_le i i.2). :-)

[Johan Commelin]

Yup...

[Scott Morrison]

but I think with better API, you could hope that just ext and simp got you basically down to a statement about lists, after which dealing with gross-ness by induction feels less intimidating

[Johan Commelin]

Here's what I really want:

example {σ : Type} [fintype σ] (l : multiset ℕ) :
  ∃ f : σ →₀ ℕ, multiset.map f finset.univ.val = l :=
sorry

[Johan Commelin]

But from there to my first question is quite straightforward, and I think the obvious way to go.

[Johan Commelin]

(Modulo that I change l to a multiset here.)

[Scott Morrison]

Why bother with the finsupp, if you already have fintype?

[Kenny Lau]

I don't think that statement is true?

[Scott Morrison]

Yeah, it's not true... what if l takes on more values than \sigma has elements?

[Johan Commelin]

Ooh, shoot...

[Johan Commelin]

What I really really want, is that (l : list nat) (hl: l.length = fintype.card \sigma) (hl' : l.sorted), and I tag on a multiset.sort on top of the multiset.map.