Zulip Chat Archive

Stream: Is there code for X?

Topic: manipulating multiset elements in proof


view this post on Zulip Bassem Safieldeen (Jul 26 2020 at 11:11):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:12):

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

view this post on Zulip Bassem Safieldeen (Jul 26 2020 at 11:16):

Mario Carneiro said:

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

Will give it a try now.

view this post on Zulip Kenny Lau (Jul 26 2020 at 11:17):

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 }

view this post on Zulip Bassem Safieldeen (Jul 26 2020 at 11:20):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:21):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:23):

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

view this post on Zulip Mario Carneiro (Jul 26 2020 at 11:23):

f $ x means f x but it has lower precedence

view this post on Zulip Kenny Lau (Jul 26 2020 at 12:26):

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

view this post on Zulip Eric Wieser (Jul 29 2020 at 18:20):

(deleted)


Last updated: May 16 2021 at 05:21 UTC