Sum over characteristic function

Stream: Is there code for X?

[Michael Stoll]

How can I prove a statement like the following without having to contort myself too much?

example (n : ℕ) : ∑ (j : fin n.succ), ite (j = 0) 0 1 = n :=
begin
  change ∑ (j : fin n.succ), id (ite (j = 0) 0 1) = n,
  rw [finset.sum_apply_ite],
  simp [finset.filter_ne'],
end

By "contort", I mean introducing the explicit identity function in the first step, which appears to be necessary for the rewrite.

[Damiano Testa]

Would using something like refine (finset.sum_ite_apply _ _).trans _ work?

You may need to give some arguments to finset..., or a different number of underscores... (I'm on mobile)

[Damiano Testa]

The point being that refine would match via defeq, while rewrite via syntactic equivalence. If you manage to apply/refine the right shape, you can get away with looser matching.

[Michael Stoll]

refine (finset.sum_apply_ite 0 1 id).trans _, can indeed replace the first two lines of the proof.
Whether one considers it to be less of a contortion, is perhaps a matter of taste :smile:

[Michael Stoll]

(And without specifying id, it does not work, so the problem persists.)

[Damiano Testa]

You probably can also replace the underscore with (by simp [...]), remove begin, end and refine, make it a one-liner and be happy with it! :upside_down:

[Damiano Testa]

Also, replacing the rw by the refine will probably create a shorter proof term.

[Michael Stoll]

In my application, I actually have ... < n + 1 instead of ... = n, so that .trans does not work.

[Damiano Testa]

Would (...).le.trans_lt work instead? This is getting worse and worse, I realize...

[Damiano Testa]

I'm probably convincing you that the show ... id ... was not so bad, after all, given how the proof could have looked.

[Damiano Testa]

At some point, a calc proof would be better. One advantage of calc is that it allows you to lock in the proper defeq you are aiming for and then you can simply provide the correct lemma to fill it in.

[Michael Stoll]

OK, I have found a simpler version of docs#finset.sum_apply_ite that works directly (docs#finset.sum_ite).

[Michael Stoll]

Which solves the problem (and tells me I should go to bed...).

[Michael Stoll]

Right now, I'm stuck on the trivial-looking example (n : ℕ) : 1 - n = 1 → n = 0...
What I have is

example (n : ℕ) (h : 1 - n = 1) : n = 0 :=
begin
  rcases @eq_zero_or_pos _ _ n with (rfl | hp),
  { refl, },
  { rw [nat.sub_eq_zero_of_le (nat.one_le_of_lt hp)] at h,
    exfalso, exact zero_ne_one h, }
end

which looks unnecessarily complicated.

[Damiano Testa]

Does docs#nat.lt_of_sub_eq_succ help?

[Damiano Testa]

(beginning with a lemma that converts the = 0 to < 1?)

[Damiano Testa]

docs#nat.lt_one_iff

[Michael Stoll]

:= nat.lt_one_iff.mp (nat.lt_of_sub_eq_succ h). Thanks.

[Michael Stoll]

I just tend not to think of succ when looking for lemmas....

[Damiano Testa]

I find navigating nat lemmas very tricky.

[Damiano Testa]

One guiding principle that I find useful, is that strict inequality is much stronger than ≤, due to truncated subtraction. So, if I can, I try to get < to do most of the work.

[Kevin Buzzard]

lemma nat.sub_eq_self (a b : ℕ) : a - b = a ↔ a = 0 ∨ b = 0 := ...

would be a nice addition to mathlib.

[Damiano Testa]

Indeed, I found the lemma above hoping that nat.sub_eq_ would autocomplete to self!

[Kevin Buzzard]

import tactic

lemma nat.sub_eq_self (a b : ℕ) : a - b = a ↔ a = 0 ∨ b = 0 := by omega

[Kevin Buzzard]

omega is a really cool tactic for all this stuff, it's such a shame that it's banned

[Eric Rodriguez]

does docs#finset.sum_ite not work?

[Yakov Pechersky]

import algebra.big_operators.basic
open_locale big_operators

example (n : ℕ) : ∑ (j : fin n.succ), ite (j = 0) 0 1 = n :=
by simp [finset.sum_ite, finset.filter_ne']

[Yakov Pechersky]

n here is a red herring:

example {α : Type*} [decidable_eq α] (x : α) (s : finset α) (hx : x ∈ s) :
  ∑ j in s, ite (j = x) 0 1 = s.card - 1 :=
by { simp [finset.sum_ite, finset.filter_ne', hx] }

[Michael Stoll]

Eric Rodriguez said:

does docs#finset.sum_ite not work?

See above.

[Eric Rodriguez]

seems I need some rest too :)

[Yakov Pechersky]

example (n : ℕ) (h : 1 - n = 1) : n = 0 :=
by cases n; simp [*] at *

[Yaël Dillies]

You should use docs#finset.sum_boole

[Michael Stoll]

True, but one has to find it first...

[Michael Stoll]

...and the name does not exactly help here. The statement does not involve booleans. Something involving ite and perhaps zero and one would be much more helpful in finding it.

[Yaël Dillies]

Agreed, but I could not come up with a better name.

[Yakov Pechersky]

indicator or single maybe? fun i, ite (i = x) 1 0 = fun i, ite (i != x) 0 1 = pi.single x 1

[Andrew Yang]

By the way, why does it require a non_assoc_semiring? Is add_monoid not enough?

[Damiano Testa]

I guess it is the presence of 0 and 1.

[Eric Rodriguez]

add_monoid_with_one is probably enough, now that that exists

[Kevin Buzzard]

You should also have its multiplicative counterpart, monoid_with_e