manipulating multiset elements in proof

Stream: Is there code for X?

[Bassem Safieldeen]

Hi everyone,

I am learning how to do stuff with multisets and I am stuck. I have a multiset X : multiset ℝ and a function myFunc : multiset ℝ → multiset ℝ that doubles elements of a multiset. I am trying to prove that if the multiset has 10 elements and each element of the multiset is 5, then applying myFunc and summing gives us 100.

Here is my code:

import algebra.big_operators
import data.real.basic

/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc : multiset ℝ → multiset ℝ :=
begin
intro X,
exact multiset.map (λ x:ℝ, 2*x) X,
end

/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100  :=
begin
    intro hX'',
    unfold myFunc,
    --  ⊢ (multiset.map (λ (x : ℝ), 2 * x) X).sum = 100
    sorry
end

[Mario Carneiro]

The first step might be to prove X = list.repeat 5 10

[Bassem Safieldeen]

Mario Carneiro said:

The first step might be to prove X = list.repeat 5 10

Will give it a try now.

[Kenny Lau]

import algebra.big_operators
import data.real.basic

/-
A function that doubles every element in a given multiset of ℝ.
-/
def myFunc (X : multiset ℝ) : multiset ℝ :=
X.map $ λ x, 2 * x

theorem multiset.map_repeat {α β : Sort*} (f : α → β) (x : α) (n : ℕ) :
  (multiset.repeat x n).map f = multiset.repeat (f x) n :=
nat.rec_on n rfl $ λ n ih, by simp_rw [multiset.repeat_succ, multiset.map_cons, ih]

/-
For a multiset of 10 elements, all of which are 5, doubling
each element and summing gives 100.
-/
example (X : multiset ℝ) (hX1 : X.card = 10) (hX2 : ∀ x ∈ X, (x : ℝ) = 5) : (myFunc X).sum = 100 :=
by { rw [multiset.eq_repeat_of_mem hX2, hX1, myFunc, multiset.map_repeat, multiset.sum_repeat], norm_num }

[Bassem Safieldeen]

This is a good chance to ask about $ :)
I see it occasionally but don't know what it means.

[Mario Carneiro]

example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100  :=
begin
  intro hX'',
  have : X = list.repeat (5:ℝ) 10,
  { obtain ⟨l⟩ := X,
    change (l : multiset ℝ) = _, congr,
    exact list.eq_repeat.2 ⟨hX', hX''⟩ },
  subst X,
  rw show (100:ℝ) = (10:ℕ) * (2 * 5), by norm_num,
  generalize_hyp : 10 = a at *,
  simp [myFunc],
end

You can do the last bit without the generalize_hyp but simp does a really stupid proof in that case

[Mario Carneiro]

example (X : multiset ℝ) (hX' : X.card = 10) :
(∀(x:ℝ), x ∈ X → x = 5) → (myFunc X).sum = 100  :=
begin
  intro hX'',
  have := multiset.eq_repeat.2 ⟨hX', hX''⟩,
  subst X,
  rw show (100:ℝ) = (10:ℕ) * (2 * 5), by norm_num,
  generalize_hyp : 10 = a at *,
  simp [myFunc, multiset.repeat],
end

[Mario Carneiro]

f $ x means f x but it has lower precedence

[Kenny Lau]

That means f $ x y = f (x y) (as opposed to f x y = (f x) y)

[Eric Wieser]

(deleted)