one liner for quotient_induction

Stream: new members

[Antoine Chambert-Loir]

I wrote the following lemmas to prove a basic property for sum of members of list/multiset :

mport tactic.basic

import data.multiset.basic

lemma list.sum_le_sup_mul_length {s : list ℕ} (a : ℕ) (h : ∀ (n : ℕ), n ∈ s → n ≤ a) :
  s.sum ≤ a * s.length :=
begin
  induction s with hd tl ih,
  { simp , },
  rw [list.sum_cons, add_comm],
  rw [list.length_cons, mul_add, mul_one],
  refine nat.add_le_add (ih _) (h _ _),
  { intros n hn, refine h n _,  --
    apply list.mem_cons_of_mem, exact hn, } ,
  { apply list.mem_cons_self, }
end

lemma multiset.sum_le_sup_mul_card {m : multiset ℕ} (a : ℕ) (h : ∀ (n : ℕ), n ∈ m → n ≤ a) :
  m.sum ≤ a * m.card :=
begin
  revert a,
  apply quotient.induction_on m,
  intros l a h,
  simpa using list.sum_le_sup_mul_length a h,
end

Is there a way to write a one-line proof of the lemma for multisets ?
(The problem is the necessity to revert a.)

(By the way : Is it the proper way to prove such a lemma ?)

[Kevin Buzzard]

This is your proof again, but in one line:

lemma multiset.sum_le_sup_mul_card {m : multiset ℕ} : ∀ (a : ℕ) (h : ∀ (n : ℕ), n ∈ m → n ≤ a),
  m.sum ≤ a * m.card :=
quotient.induction_on m (λ l a h, by simpa using list.sum_le_sup_mul_length a h)

[Kevin Buzzard]

I just move the a to after the colon. Usually this is not what is done, because ∀s after colons usually means more unnecessary intros. But moving stuff before or after the colon doesn't change the type of multiset.sum_le_sup_mul_card; indeed #check @multiset.sum_le_sup_mul_card shows you that actually everything gets moved after the colon in the end :-)

[Eric Wieser]

Another approach is to write induction m using quotient.induction_on instead of apply quotient.induction_on m,, which avoids the need for revert