Zulip Chat Archive

Stream: general

Topic: how to call this lemma


view this post on Zulip Johan Commelin (Aug 07 2018 at 12:03):

lemma quux {A : Type*} [add_comm_group A] {n : } (f : fin (n+1)  A) : sum univ f = f n + sum univ (λ i : fin n, f i.raise) :=
begin
  sorry
end

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:06):

Ooh, and if you don't know a name, but you know a proof... that's fine too.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 12:23):

Johan, I think Kenny might have generated a proof of this once, when I was trying to figure out induction.

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 12:24):

https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 12:25):

check out def4 in https://github.com/kckennylau/Lean/blob/master/proofs_by_induction.lean

view this post on Zulip Kevin Buzzard (Aug 07 2018 at 12:25):

Apparently it uses a lemma called chris. I'm not sure if this is the official mathlib-sanctioned name.

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:30):

Ok, thanks. I'll take a look in a minute!

view this post on Zulip Chris Hughes (Aug 07 2018 at 12:56):

I proved a slightly weaker version

lemma quux {A : Type*} [add_comm_group A] {n : } (f : fin (n+1)  A) :
  sum univ f = f n, nat.lt_succ_self _⟩  + sum univ (λ i : fin n, f i.raise) :=
by rw [ insert_erase (mem_univ (n, nat.lt_succ_self _⟩ : fin (n + 1))),
    sum_insert (not_mem_erase _ _), add_left_inj]; exact
sum_bij (λ a ha, a, lt_of_le_of_ne (nat.le_of_lt_succ a.2)
  (fin.vne_of_ne (mem_erase.1 ha).1) ) (λ _ _, mem_univ _)
  (λ ⟨_, _⟩ _, rfl) (λ a, _⟩ b, _⟩ _ _ h, fin.eq_of_veq (fin.veq_of_eq h : _))
  (λ b hb, ⟨⟨b.1, nat.lt_succ_of_lt b.2, mem_erase.2 fin.ne_of_vne (ne_of_lt b.2), mem_univ _⟩,
    by cases b; refl)

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:57):

Why is it weaker?

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:57):

Also, apparently I ought to be using finset.range...

view this post on Zulip Chris Hughes (Aug 07 2018 at 12:57):

I used ⟨n, nat.lt_succ_self _⟩ instead of \u n

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:58):

Aaah, but that is better.

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:58):

Silly me didn't understand that \u n is difficult.

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:59):

I think you can use nat.le_refl _ for some golfing.

view this post on Zulip Johan Commelin (Aug 07 2018 at 12:59):

But I will first think about the finset.range version. Maybe it becomes a whole lot easier.

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:08):

lemma quux {A : Type*} [add_comm_group A] (n : ) (f :   A)
: (finset.range (n+1)).sum f = f n + (finset.range n).sum f := by simp

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:09):

So, that might not be even worth stating as a lemma.

view this post on Zulip Kenny Lau (Aug 07 2018 at 14:09):

what's the use of this lemma if you could just simp?

view this post on Zulip Johan Commelin (Aug 07 2018 at 14:10):

That's exactly my point.


Last updated: May 13 2021 at 22:15 UTC